Technical Summary: AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

1. Problem Statement

Quantum programs extend quantum circuits by incorporating classical control flow constructs such as branches and loops. While quantum circuits (the domain of AutoQ 1.0) suffice for defining static sequences of gates, advanced quantum algorithms—such as Repeat-Until-Success (RUS) algorithms and weak-measurement-based versions of Grover's search—require dynamic control based on classical values obtained from qubit measurements.

Verifying these programs presents significant challenges not present in circuit-only verification:

• Measurement and Normalization: Measurement collapses quantum states and yields classical values (0 or 1) that drive control flow. This process often requires normalization of probability amplitudes, which complicates formal reasoning.
• Control Flow Reasoning: Verifying loops and branches requires handling state spaces that evolve based on measurement outcomes, a task difficult for existing automated tools.
• Lack of Automated Tools: While deductive verification tools exist for classical programs (e.g., Dafny, KeY) and some quantum tools exist (e.g., CoqQ, Qbricks), they either lack full automation or require substantial manual effort (e.g., providing complex Hermitian operators or extensive proof search). Existing automated tools often focus on circuit equivalence or specific parameterized programs, lacking general support for control flow in quantum programs.

2. Methodology

AutoQ 2.0 addresses these challenges by extending the previous circuit verification framework to support full quantum programs. The core methodology relies on Level-Synchronized Tree Automata (LSTAs) and a novel entailment testing approach.

2.1 Formal Model: Level-Synchronized Tree Automata (LSTAs)

The tool represents sets of quantum states (pre-conditions, post-conditions, and loop invariants) using LSTAs.

• Structure: LSTAs are symbolic tree automata designed to encode quantum states as perfect binary trees, where branches represent computational basis states and leaves represent complex probability amplitudes.
• Synchronization: A key feature of LSTAs is the "choice" mechanism. Transitions at the same tree level must share a common choice set. This allows LSTAs to compactly represent entangled states and superpositions that standard tree automata cannot, by ensuring that only valid combinations of branches (those sharing a choice) are generated.
• Input Format: Users specify pre-conditions, post-conditions, and loop invariants as .lsta files, which define the automata recognizing the sets of valid quantum states.

2.2 Verification Framework

The verification process is automated and follows a deductive style:

1. Program Execution: The tool executes quantum gates (e.g., $H$, $CX$, $T$) on the LSTA representing the pre-condition.
2. Handling Measurement and Branches:
   • When a measurement $M_i = b$ occurs, the LSTA is split into two copies corresponding to outcomes $b=0$ and $b=1$.
   • The algorithm updates the tree by zeroing out the probability amplitudes of the non-matching branches (e.g., if $M_1=0$, the amplitudes of the $1$-subtree under $x_1$ are set to 0).
   • Crucially, the tool does not normalize the amplitudes during this step. It preserves the raw amplitudes to avoid complex arithmetic during execution, deferring normalization checks to the final entailment test.
   • Branch statements are handled by computing the resulting LSTAs for both the true and false paths and taking their union.
3. Handling Loops:
   • For while loops, the user must provide a loop invariant as an LSTA.
   • The tool verifies that the invariant is inductive: it must cover all states reachable before the loop, and executing the loop body on the invariant (conditioned on the loop continuation) must result in states still covered by the invariant.
   • The states at the loop exit are over-approximated by the invariant conditioned on the loop termination.
4. Entailment Testing (Up to Scaling):
   • The final step checks if the set of reachable states (represented by an LSTA $R$) is included in the post-condition (LSTA $Q$).
   • Because normalization factors were ignored during execution, the tool uses a specialized entailment up to scaling ($|=_{uts}$) relation.
   • $A |=_{uts} B$ holds if every tree in $A$ is a linearly scaled version of a tree in $B$ (i.e., $T_A = r \cdot T_B$ for some non-zero scalar $r$).
   • This check is performed using a graph search algorithm that traverses the LSTAs level-by-level, mapping states and terms, and finally invoking an SMT solver (Z3) to verify the existence of a scaling factor $r$ that satisfies the global constraints.

3. Key Contributions

• Extension to Quantum Programs: AutoQ 2.0 is the first tool to provide automated deductive verification for quantum programs containing loops and branches, moving beyond the circuit-only scope of AutoQ 1.0.
• Automated Handling of Measurement: The tool introduces algorithms to split LSTAs based on measurement outcomes and manage the resulting state spaces without manual intervention.
• Normalization-Free Verification: By designing an entailment test that works with non-normalized states (up to scaling), the tool avoids the computational complexity of normalizing amplitudes during the execution phase, significantly improving efficiency.
• LSTA-Based Invariants: The framework utilizes LSTAs to represent loop invariants, allowing for the compact representation of complex quantum states required for iterative algorithms.
• Scalability: The approach supports verification of programs with a large number of qubits (up to 100 qubits in the reported benchmarks) by leveraging the compactness of LSTAs and efficient SMT solving.

4. Experimental Results

The authors evaluated AutoQ 2.0 on two classes of advanced quantum programs:

1. Repeat-Until-Success (RUS) Algorithms: Used for generating non-standard quantum gates (e.g., specific unitaries like $(2X + \sqrt{2}Y + Z)/\sqrt{7}$).
   • Result: All RUS benchmarks were verified instantly (0.0s).
2. Weak-Measurement-Based Grover's Search: A version of Grover's algorithm that does not require prior knowledge of the number of solutions.
   • Result: The tool successfully verified instances with up to 100 qubits (specifically, 101 qubits in the table) in approximately 11 seconds (for the 101-qubit case) to 20 minutes (as stated in the abstract for the 100-qubit case, though the table shows 11s for 101 qubits; the abstract likely refers to a specific configuration or includes setup time). The verification time scales reasonably with the number of qubits and gates.

The experiments were conducted on a server with an AMD EPYC 7742 processor and 1,152 GiB of RAM.

5. Significance and Claims

The paper claims that AutoQ 2.0 is currently the only tool capable of verifying quantum programs with such a high degree of automation. Unlike existing tools that rely on proof assistants (requiring significant human effort) or focus solely on circuit equivalence, AutoQ 2.0 bridges the gap between formal verification theory and practical quantum programming by handling control flow and measurement automatically.

The authors position the tool as a significant step toward the formal verification of complex quantum algorithms, demonstrating that automated deductive verification is feasible for programs that cannot be expressed as simple quantum circuits. They note modestly that while the current implementation handles non-nested control flow and pure states, future work aims to automate invariant generation and extend support to mixed states arising from more complex loops.