Discovering formally verified quantum programs with AI
Sergey Shirobokov, Ben Jaderberg and colleagues at Google DeepMind and Google Quantum AI, with Pushmeet Kohli as senior author, build a Lean library of quantum programs in which teams of LLM agents write new programs against formal specifications and prove their correctness and cost.
Ask this paper
Problem. Classical computers can only test quantum algorithms on small or restricted instances, so discovery loops scored by simulation cannot reach the regimes where quantum algorithms matter.
Method. Researchers write a specification theorem and a cost target in Lean. Agent teams propose programs, the Lean kernel checks correctness and cost, and an independent comparator re-verifies each accepted solution.
Collaboration. Teams publish verified solutions, partial results and dead ends to a shared wiki and exchange ideas and critiques at scheduled conferences.
Results. Verified programs improve on prior baselines by up to 1.4x for parallel search, 290x for quantum arithmetic (arcsin), and 11x, 8x and 2.5x for simulations relevant to fusion, photochemistry and drug metabolism.
Significance. Formal proof replaces simulation as the check, so agents can produce algorithms that neither classical computers nor current quantum hardware can test.
Abstract
The timeline by which quantum computers can solve breakthrough problems in science depends on improved quantum algorithms as much as on better hardware. Such algorithmic advances are typically achieved through many years of expert human collaboration. In mathematics and computer science, large language models have accelerated progress through automated discovery loops. However, quantum algorithms can only be evaluated by classical computers on restricted or small instances. Here we demonstrate automated discovery of quantum programs beyond these regimes including order-of-magnitude improvements on scientific applications. To achieve this, we build a quantum program library in the Lean theorem prover in which large language model agents synthesize novel programs against formal problem specifications and verify their correctness and cost. Agent teams collaborate, sharing results and knowledge through wikis and discussing ideas at organized conferences. Our results improve on prior baselines for parallel search (up to 1.4x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug-metabolism by 11x, 8x and 2.5x respectively. Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.