Bounds for Quantum Circuits using Logic-Based Analysis

TL;DR

This work addresses the challenge of scaling verification for quantum circuits to ensure they remain within a target sub-space, such as preserving a low Hamming distance or entanglement. It proposes a logic-based, SMT-driven approach that combines compositional verification with linear over-approximation of gate effects to derive bounds without full quantum simulation, incorporating weakest-precondition reasoning to automate local assumptions. The authors demonstrate two key ideas—decomposition into sub-circuits and abstraction of gate effects—through two examples (H-CNOT and an $H(2^6)$ gate fabric) and report that these strategies substantially reduce variable counts and solver runtimes. The approach holds promise for scalable verification of quantum software and complex circuits, including those modeling MB L-DTCs, by enabling bound proofs on properties like the Hamming weight $HW( abla)$ and subspace preservation while avoiding exhaustive state-space exploration.

Abstract

We explore ideas for scaling verification methods for quantum circuits using SMT (Satisfiability Modulo Theories) solvers. We propose two primary strategies: (1) decomposing proof obligations via compositional verification and (2) leveraging linear over-approximation techniques for gate effects. We present two examples and demonstrate the application of these ideas to proof Hamming weight preservation.

Figures (6)

• Figure 1: (a) Quantum circuit for the kicked Ising MBL-DTC. (b) A time crystals spontaneously breaks the time translational invariance of the drive.
• Figure 2: Left: two-qubit curcuit $C$ with pre-condition $P$ and post-condition $Q$. Right: Matrix representations of Hadamard gate (1) and CNOT gate (2).
• Figure 3: Logic encoding of the quantum circuit C in Figure \ref{['fig:example1']} along with pre-condition P and post-condition Q, expressed as first-order formulas over the complex coefficients of the basis states. This representation is translated to formulas over reals to decide $P\land C \models Q$ with an SMT solver.
• Figure 4: Decomposition of the proof from Figure \ref{['fig:constraints']}.
• Figure 5: H(4) gate matrix for parameter $\lambda$.