Analyzing quantum programs using the power of interaction
summary
Proposes two concrete verification routes: embed execution into a circuit-to-Hamiltonian embedding so the correct run is the ground-state witness and avoid intermediate measurements, and use interaction plus cryptography to let a classical verifier check a quantum run (a Mahadev classical verification under the LWE assumption). Targets making the lowest-energy eigenstate certify correctness by adding assertion terms to the Hamiltonian. Work is ongoing: no full implementation yet, main challenges are encoding unknown eigen-subspaces and relaxing cryptographic or practicality constraints.
AI-written summary · about
chapters (4)
related talks
22mEfficient Formal Verification of Quantum Error Correcting Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
40mDemocratizing quantum formal verification: the path-sum way
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
42mQuantum program analysis: Verification and Testing
45mClassical Verification of Quantum Computational Advantage
32mBeating Classical Impossibility of Position Verification
27mParameterized Verification of Quantum Circuits