QEDIA: Quantum Program Verification in Lean

AI summary

Overview

Research area: Quantum programming languages and formal verification — specifically mechanized quantum Hoare logic in the Lean 4 proof assistant, with LLM agents used as proof engineers.

Technical level: Advanced. The paper assumes familiarity with Hoare logic, density operators, and proof assistants, though its motivation and contributions are stated in largely accessible terms.

Scope (one sentence): QEDIA is a Lean 4 library that formalizes the quantum Hoare logic QHL⁺ — including its mathematics, program semantics, specification language, and proof rules with proved soundness — and uses an LLM-based agent to build both the library and eleven verified quantum programs.

What This Paper Is About

Quantum programs mix classical and quantum computation in both directions: classical variables decide which gates run, on which qubits, with which parameters, while measurement outcomes feed back into classical control flow. Verifying such programs in a proof assistant means mechanizing that interplay consistently from the underlying linear algebra up through the proof rules. QEDIA does this by formalizing QHL⁺ in Lean 4 on top of Mathlib and proving the logic sound for both partial and total correctness, with an LLM-based prover agent assisting in writing the library and the example proofs.

Key Contributions

1. A formalized quantum Hoare logic with proved soundness. QEDIA formalizes QHL⁺ for quantum while-programs with classical variables, quantum arrays, and parameterized gates, and proves the proof system sound in Lean for both partial and total correctness. The formalization covers the classical–quantum interplay at every level, from quantum mechanics up to the proof system.

2. An agent-based proof-writing framework. A general-purpose core agent coordinates LLM agents that construct and review formal proofs, combining Lean's kernel checks with review of the intended mathematics. Its quantum extension supports applying QHL⁺ rules and adds quantum-specific checks.

3. Eleven verified program examples. Bell state preparation, a 1D cluster state, parallel Hadamard, the quantum Fourier transform and its inverse, quantum phase estimation, a repeat-until-success circuit, Hamiltonian simulation of the transverse-field Ising model via a Trotter product formula, and the Bravyi–Kitaev encoding, block encoding, and quantum signal processing for the Fermi–Hubbard model.

4. A first-of-its-kind claim. The authors state that, to their knowledge, this is the first mechanized quantum program logic built by LLM agents, and that some of the verified examples cannot be directly handled by existing quantum program verifiers because they involve classical–quantum interplay at both the program and specification levels.

Main Findings

• Three levels of classical–quantum interplay must be handled together. The paper identifies (L0) mathematics and quantum mechanics — Hilbert spaces, states, tensor products, Kraus operators, measurements; (L1) program syntax and semantics — guards, array indices, gate parameters, measurement outcomes written into classical state; and (L2) specification and proof system — quantum predicates that depend on classical variables. The authors argue existing verifiers do not directly support the interplay at both L1 and L2.

• Specifications need "formal quantum states." To write predicates such as |χ(n, x)⟩⟨χ(n, x)|, which depend on a classical array x, QEDIA introduces formal quantum states with a recursively defined signature recording which quantum variables they involve, interpreted relative to a classical state.

• Quantum predicate formulas are a small, expressive language. The syntax includes atomic predicates K(t̄)[q̄], formal-state atoms [s], negation, tensor product, and a family F(t̄)q̄ of Kraus operators. The Kraus family uniformly expresses reset, unitary evolution, measurement, and masking.

• A distinctness side condition governs well-formedness. Operations on a sequence of quantum variables require σ ⊧ Dist(q̄), meaning the qubit indices denoted by the classical state are pairwise distinct — for example, CNOT[q[i], q[j]] requires σ(i) ≠ σ(j).

• The logic captures approximation guarantees, not just exact behaviour. The Trotter example is specified with a precondition requiring ε ≥ (θ²/2N)‖[H_X, H_ZZ]‖ and a postcondition giving fidelity at least 1 − ε with the target state. The authors emphasize that proving the product formula exact would not establish this guarantee; the classical variable ε parameterizes the quantum predicates.

• Probabilistic correctness is expressible. The repeat-until-success example is proved with two Hoare triples: one for termination with either success (m = 0) or exhaustion of N attempts, and one bounding the overall success probability by 1 − 4^{−N}, given per-iteration success probability 3/4 for the gate V_RUS = (I + i√2 X)/√3.

• Quantitative proof-engineering statistics are not reported in the provided content. The truncated text does not give line counts, proof-automation rates, agent success rates, or timing measurements for the eleven examples.

Methodology in Plain English

The authors take an existing program logic, QHL⁺, and rebuild it inside Lean 4, a proof assistant that checks every step of a mathematical argument mechanically. The work proceeds bottom-up. First, they set up the mathematical substrate for quantum mechanics — states, operators, tensor products, measurements — reusing Mathlib where possible and adding what the classical–quantum interplay demands. Second, they encode the syntax of a small quantum while-language with classical variables and quantum arrays. Third, they define the operational semantics as transitions between configurations consisting of a remaining program, a classical state, and a partial density operator. Fourth, they define the specification language — pairs of a classical formula and a quantum predicate formula — and the proof rules, and they prove those rules sound for both partial and total correctness.

The proofs themselves are written with an LLM agent under human supervision. The agent is general-purpose at its core, extended with quantum-specific capabilities: it can apply QHL⁺ rules and run quantum-specific checks. Its outputs are accepted only if Lean's kernel accepts them, and a review step checks that the formal statement matches the intended mathematics.

Finally, the framework is exercised on a set of programs chosen to stress the classical–quantum interplay: circuits with mid-circuit measurement and feedback, circuits whose gate indices and phases are computed from classical variables, and a circuit whose correctness is an approximation bound.

Why This Matters

Impact on research. Mechanized verification of quantum programs has, to date, required large manual formalization efforts — the paper points to CoqQ, Qbricks, and the certified end-to-end verification of Shor's algorithm as evidence. QEDIA contributes a mechanized logic that handles classical variables, quantum arrays, and parameterized gates in one framework, and it demonstrates that LLM agents can carry a substantial share of that formalization work. If the approach generalizes, it changes the cost structure of building verified quantum software.

Real-world applications:

• Fault-tolerant compilation. Repeat-until-success circuits exist to reduce the count of expensive T gates; verifying their success probability and termination bound is directly relevant to compiled non-Clifford gates.
• Quantum algorithms for cryptography and number theory. The quantum Fourier transform, its inverse, and quantum phase estimation are the readout machinery of Shor's factoring algorithm and of eigenvalue estimation generally.
• Quantum simulation for chemistry and materials. Hamiltonian simulation of the transverse-field Ising model and the Bravyi–Kitaev, block-encoding, and quantum signal processing components for the Fermi–Hubbard model are the primitives of electronic-structure simulation.
• State preparation and benchmarking circuits. Bell state and 1D cluster state preparation and parallel Hadamard are the building blocks of measurement-based quantum computing and hardware characterization.

Industry relevance. Quantum hardware and software companies need correctness arguments for compilers, control stacks, and error-correction primitives that cannot be established by testing alone, since measurement disturbs the state and the no-cloning theorem forbids copying it for offline analysis. The work is also relevant to the formal-methods and AI-for-code industries, since the agent architecture described is presented as a general-purpose core extended to a specific domain.

Future Directions

• Scaling beyond the current example set. The eleven programs are substantial but still modest relative to full applications; whether the library and agent workflow extend to larger circuits and richer classical data structures is an open question.
• Reducing human supervision. The authors describe the agents as working under human supervision; how much of the review step can be automated while preserving trust in the formalized statements is unresolved.
• Broadening the mechanized logic. The paper's comparison section is truncated in the provided content, so the precise scope of what QHL⁺ features remain unformalized is not reported here; extensions such as richer classical theories or additional proof rules are natural next steps.
• Transfer to other program logics and other proof assistants. The general-purpose core agent is presented as domain-agnostic, which raises the question of whether the same pattern transfers to other quantum or classical logics beyond Lean 4.

Target Audience

Researchers in quantum programming languages and formal verification; proof engineers and developers of mechanized semantics in Lean, Coq, or Isabelle; quantum software and compiler teams seeking correctness guarantees for hybrid classical–quantum code; and researchers in AI-assisted theorem proving interested in a domain-specific case study of LLM agents building a substantial verified library. Readers without background in Hoare logic or quantum mechanics will find the motivation accessible but the technical development demanding.

Authors’ abstract

Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.