Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying \emph{spatial} and \emph{size-dependent} properties of physical many-body states, where the key parameter is the system size. This paper takes a step toward bridging the gap. We propose \emph{Linear Chain Logic} (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and large-size asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analysed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given size and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.
Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying \emph{spatial} and \emph{size-dependent} properties of physical many-body states, where the key parameter is the system size. This paper takes a step toward bridging the gap. We propose \emph{Linear Chain Logic} (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and large-size asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analysed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given size and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.
Abstract Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying spatial and size-dependent properties of physical many-body states, where the key parameter is the system size. This paper takes a step toward bridging the gap. We propose Linear Chain Logic (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and large-size asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analysed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given size and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.
The term Tensor Network States (TNS) refers to a number of families of states that represent different ansätze for the efficient description of the state of a quantum many-body system.Matrix Product States (MPS) are one particular case of TNS, and have become the most precise tool for the numerical study of one dimensional quantum many-body systems, as the basis of the Density Matrix Renormalization Group method.Lattice Gauge Theories (LGT), in their Hamiltonian version, offer a challenging scenario for these techniques.While the dimensions and sizes of the systems amenable to TNS studies are still far from those achievable by 4-dimensional LGT tools, Tensor Networks can be readily used for problems which more standard techniques, such as Markov chain Monte Carlo simulations, cannot easily tackle.Examples of such problems are the presence of a chemical potential or out-of-equilibrium dynamics.We have explored the performance of Matrix Product States in the case of the Schwinger model, as a widely used testbench for lattice techniques.Using finite-size, open boundary MPS, we are able to determine the low energy states of the model in a fully non-perturbative manner.The precision achieved by the method allows for accurate finite size and continuum limit extrapolations of the ground state energy, but also of the chiral condensate and the mass gaps, thus showing the feasibility of these techniques for gauge theory problems.
The Thesis explores the application of Matrix Product States (MPS) in the domain of quantum many-body systems and quantum computing, show casing the versatility and effectiveness of MPS for addressing complex com putational challenges. The opening chapter introduces essential tools for Tensor Networks, addressing the curse of dimensionality and elucidating the main characteristics of Matrix Product States and Matrix Product Op erators. The discussion encompasses also important numerical techniques, including Density Matrix Renormalization Group and Time Evolving Block Decimation. Furthermore, the relation between MPS and quantum circuits is discussed. The subsequent Chapters delve into specific applications of MPS. In the second Chapter, we introduce a Tensor Network ansatz inspired by the backflow transformation for correlated systems. This extension of the MPS representation ensures an area law for entanglement in dimensions one or greater. We employ an optimization scheme combining DMRG and variational Monte Carlo algorithms for efficient ground-state search. Bench marking against spin models demonstrates high accuracy. The third Chapter explores quantum annealing for optimizing complex classical spin Hamil tonians, as the Hopfield model and the binary perceptron. We introduce an efficient Tensor Network representation for the adiabatic time evolution of quantum annealing, enabling scalable classical simulations. The use of MPS in mitigating Trotter errors and mapping to quantum circuits is also explored. In the fourth Chapter we present a novel method for evaluating the amount of nonstabilizerness (also known as quantum magic) contained in an MPS. We overcome the exponentially hard evaluation of this quan tity by employing a simple perfect sampling technique of Pauli string. Our innovative MPS approach enables efficient computation. Benchmarked on magic states and the quantum Ising chain ground state, this method offers easy access to the non-equilibrium dynamics of nonstabilizerness following a quantum quench. The Appendices provide additional insights, including: an introduction to variational Monte Carlo, technical details on MPS simula tions for the quantum annealing and a comprehensive overview on stabilizer formalism and nonstabilizerness.
Simulating quantum many-body systems (QMBS) is one of the long-standing, highly non-trivial challenges in condensed matter physics and quantum information due to the exponentially growing size of the system's Hilbert space. To date, tensor networks have been an essential tool for studying such quantum systems, owing to their ability to efficiently capture the entanglement properties of the systems they represent. One of the well-known tensor network architectures, namely matrix product states (MPS), is the standard method for simulating one-dimensional QMBS. Here, we propose a simple, yet efficient, method to augment the already available MPS algorithms to simulate the dynamics of time-dependent Hamiltonians with better accuracy and a faster convergence rate, giving a second-order convergence compared to the first-order convergence of the standard method. We apply our proposed method to simulate the dynamics of a chain of single spins associated with nitrogen-vacancy color centers in diamonds, which has potential applications for practical and scalable quantum technologies, and find that our method improves the average error for a system of few NV centers by a factor of about 1000 for moderate step sizes. Our work paves the way for efficient simulation of QMBS under the influence of time-dependent Hamiltonians.
A generic method to investigate many-body continuous-variable systems is pedagogically presented. It is based on the notion of matrix product states (so-called MPS's) and the algorithms thereof. The method is quite versatile and can be applied to a wide variety of situations. As a first test, we show how it provides reliable results in the computation of fundamental properties of a chain of quantum harmonic oscillators achieving off-critical and critical relative errors of the order of ${10}^{\ensuremath{-}8}$ and ${10}^{\ensuremath{-}4}$, respectively. Next, we use it to study the ground-state properties of the quantum rotor model in one spatial dimension, a model that can be mapped to the Mott insulator limit of the one-dimensional Bose-Hubbard model. At the quantum critical point, the central charge associated with the underlying conformal field theory can be computed with good accuracy by measuring the finite-size corrections of the ground-state energy. Examples of MPS computations both in the finite-size regime and in the thermodynamic limit are given. The precision of our results is found to be comparable to that previously encountered in the MPS studies of, for instance, quantum spin chains. Finally, we present a spin-off application: an iterative technique to efficiently get numerical solutions of partial differential equations of many variables. We illustrate this technique by solving Poisson-like equations with precisions of the order of ${10}^{\ensuremath{-}7}$.
Numerical methods based on matrix product states (MPSs) are currently the standard for calculating the ground-state properties of (quasi-)one-dimensional quantum many-body systems. While the properties of the low-lying excitations in such systems are often studied in this MPS framework through by means of time-evolution simulations, we can also look at their by directly calculating eigenstates corresponding to these excitations. The so-called MPS excitation ansatz is a powerful method for finding such eigenstates with a single-particle character in the thermodynamic limit. Although this excitation ansatz has been used quite extensively, a general method for calculating expectation values for these states is lacking in the literature: We aim to fill this gap by presenting a recursive algorithm to calculate arbitrary observables expressed as matrix product operators. This method concisely encapsulates existing methods for—as well as extensions to—the excitation ansatz, such as excitations with a larger spatial support and multiparticle excitations, and is robust enough to handle further innovations. We demonstrate the versatility of our method by studying the low-lying excitations in the spin-1 Heisenberg chain and the one-dimensional Hubbard model, looking at how the excitations converge in the former, while in the latter, we present a refined method of targeting single-particle excitations inside a continuum by minimizing the energy rather than the energy itself. We hope that this technique will foster further advancements with the excitation ansatz.