About AutoQ 2.0
Fully automatic verification of quantum programs using tree automata. C++ standalone tool. Can verify 100-qubit circuits in ~20 minutes without human proof effort.
Verification Paradigm
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Approach | Automata-based automatic verification | Foundational interactive theorem proving (ITP) |
| Style | Deductive: precondition/postcondition/invariant -> automatic checking | Denotational semantics + Hoare logic (planned) |
| User interaction | Provide program, pre/postconditions, loop invariants; tool does the rest | Write proofs interactively, aided by tactics |
| Paradigm analogy | Comparable to Dafny/KeY for classical programs | Comparable to Coq/Isabelle for classical programs |
State Representation
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Core model | Level-Synchronized Tree Automata (LSTAs) | Matrix denotational semantics (via Mathlib) |
| State encoding | Binary trees: branches = qubit values, leaves = complex amplitudes | Explicit matrices / state vectors over Hilbert spaces |
| Symbolic variables | LSTA leaf terms with symbolic complex variables constrained by global formula | Lean meta-variables; Dirac AST supports embedded Lean terms |
| Parametric states | Naturally supported: LSTAs represent infinite families via symbolic leaves | Supported via universally quantified Lean terms |
| Mixed states | Pure states only (no decoherence, no noise) | Can express mixed states via density matrices |
Automation
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Degree | Fully automatic (given specs + invariants) | Semi-automatic with certified tactics |
| Gate application | Algorithmic LSTA transformation | Symbolic evaluation via denotational semantics |
| Entailment checking | Dedicated 'entailment up to scaling' algorithm + Z3 | dirac_eq / ldirac_eq tactics |
| Loop handling | Automatic invariant checking via inductiveness test | Planned: Hoare logic rules with manual proof |
| Measurement | Algorithmic LSTA splitting (measured-0 / measured-1 copies) | Planned: denotational semantics of measurement |
Expressiveness
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Program language | U | P;P | while (M_i=b) do {P} | if (M_i=b) then {P} else {P} | Classical-quantum language with CExpr, labels, Dirac (program syntax planned) |
| Gate set | Fixed standard gates (H, S, CX, T, Z, SWAP, Toffoli) + special CK | Any operator expressible in Dirac notation / matrix form |
| Classical control | Measurement-based branching and loops only | Native classical expressions (arithmetic, booleans, arrays) |
| Nested control flow | Not supported (non-nested only) | No restriction in principle |
| Properties verifiable | Sets of reachable pure states (LSTA languages) | Any property expressible in Lean's type theory |
Scalability
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Demonstrated scale | Up to 100 qubits (weakly measured Grover's) in ~20 min | Small examples; scalability depends on proof strategy |
| Bottleneck | LSTA state-space explosion; entailment test complexity | Proof term size; matrix computation; tactic performance |
| Parametric verification | Handles parametric qubit count natively via symbolic LSTAs | Handles parametric proofs via universal quantification |
| WMGrover(50) | 101 qubits, 849 gates, 11 seconds, 44MB | Not yet benchmarked at comparable scale |
Trust Base
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Implementation | Standalone C++ tool (~thousands of lines) | Lean 4 library built on Mathlib |
| Trusted components | Entire C++ codebase + Z3 solver | Lean 4 kernel only (~10K lines of C++) |
| Soundness argument | Paper proofs (Theorems 1-2); implementation unverified | Machine-checked proofs; Lean kernel verifies every step |
| Bug risk | Implementation bugs in C++, Z3 bugs, paper-to-code gap | Bugs only possible in Lean 4 kernel (extremely small TCB) |
Proof Certificates
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Certificate output | None; binary Verified/Failed answer | Full Lean proof terms checked by kernel |
| Reproducibility | Requires re-running the tool | Proof terms are persistent artifacts |
| Independent verification | Not possible without re-implementation | Any Lean 4 installation can check proofs |
| Auditability | Must trust the tool | Proof structure is inspectable |
Case Studies
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Repeat-Until-Success circuits | All verified instantly (0.0s, 6-7MB) | Not yet |
| Weakly Measured Grover (3-50 qubits) | Verified: 0.0s to 11s, 42-44MB | Not yet |
| Dirac notation reasoning | Not in scope | Certified rewriting for plain and labelled Dirac |
| Shor's algorithm | Not demonstrated | Final verification goal |
Summary: Key Differences
| Aspect | AutoQ 2.0 | Fanal |
|---|---|---|
| Approach | Fully automatic (tree automata) | Interactive theorem proving |
| Trust Base | Unverified C++ implementation | Lean 4 kernel (fully verified) |
| Scalability | 100-qubit circuits in ~20 min | Depends on proof complexity |
| Expressiveness | Bounded quantum circuits only | General classical-quantum programs with loops |
| User Effort | Zero (fully automatic) | Medium (tactic-assisted proofs) |