⚛️ quantum physics

Discovering formally verified quantum programs with AI

This paper demonstrates how large language model agents, operating within a formal verification framework in the Lean theorem prover, can autonomously discover and mathematically prove the correctness of novel quantum programs that achieve significant performance improvements over existing baselines in scientific applications like quantum arithmetic and fusion simulation.

Original author: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M.

Published 2026-11-09

📖 4 min read🧠 Deep dive

CC BY 4.0

Original author: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M. Zhang, James Watson, Tanuj Khattar, Aws Albarghouthi, Stavan Jain, Harun Khan, Leopoldo Sarra, Andrew W. Senior, Michael Broughton, Hussain Masoom, Sergio Boixo, Ryan Babbush, Swarat Chaudhuri, Pushmeet Kohli

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the author. For technical accuracy, refer to the original paper. Read full disclaimer

Quantum computers promise to solve problems that are currently impossible for the machines we use every day, from designing new medicines to modeling the behavior of stars. However, building a machine that can actually do these tasks is incredibly difficult. The hardware is still in its infancy, prone to errors, and far too small to handle the massive calculations required for real-world science. To bridge this gap, scientists need better algorithms—step-by-step instructions that tell the quantum computer how to solve a problem using the fewest possible resources. For decades, finding these instructions has been a slow, manual process, relying on the intuition and hard work of human experts who spend years refining a single idea.

The challenge is that these algorithms are so complex that even the most powerful classical computers cannot test them to see if they work correctly before the quantum hardware is ready. This creates a catch-22: we need better algorithms to make the hardware useful, but we cannot verify the algorithms without the hardware. A team of researchers at Google has now broken this cycle by combining artificial intelligence with rigorous mathematical proof. They have created a system where AI agents act as researchers, writing and testing quantum programs in a language that a computer can check for absolute correctness. This approach allows them to discover new, highly efficient algorithms for scientific problems that are far too large to be simulated on any existing computer.

The researchers built a digital laboratory where teams of AI agents collaborate to solve specific scientific puzzles. Instead of just guessing and checking, these agents work within a strict framework called a theorem prover. Think of this framework as a rulebook that demands every single step of a proposed solution be mathematically proven to be correct before it is accepted. The agents are tasked with writing quantum programs that simulate physical systems, such as how particles interact in a fusion reactor or how a drug molecule breaks down in the body. If an agent proposes a program that saves time or uses fewer resources, the system immediately checks the math. If the proof holds, the solution is saved; if it fails, the agent learns from the error and tries again. This process happens in a shared workspace where different teams of agents can see each other's progress, share ideas, and build upon one another's discoveries, much like human scientists at a conference.

Using this method, the team tackled five major scientific challenges. In one case, they improved a fundamental mathematical operation used in many quantum algorithms, making it nearly three hundred times more efficient than the best previous method. In another, they optimized a search algorithm, finding solutions that were up to 1.4 times faster than the strongest known alternatives. The most significant achievements came in simulating complex physical phenomena. For a simulation relevant to nuclear fusion, which involves tracking the energy loss of particles moving through hydrogen, the AI discovered a program that reduced the required resources by nearly eleven times. For a simulation of a chemical reaction involved in photochemistry, the improvement was eight times better. Finally, for a model of a key enzyme that helps the human body process medicines, the AI found a solution that was nearly 2.5 times more efficient.

These results are not just theoretical improvements; they represent a shift in how scientific discovery can happen. The programs discovered by the AI are so complex that they involve thousands of logical components, far beyond what current quantum computers can run. Because the AI's work is backed by formal mathematical proofs, researchers can trust that these programs will work correctly once the hardware catches up. The system effectively allows scientists to design algorithms for machines that do not yet exist, shortening the path to practical quantum computing. By automating the search for these solutions and verifying them with mathematical certainty, the researchers have shown that artificial intelligence can accelerate the development of quantum technology, turning what was once a slow, manual struggle into a rapid, collaborative discovery process.

Technical Summary: Discovering Formally Verified Quantum Programs with AI

Problem Statement

The realization of practical quantum advantage in science depends as much on improved algorithms as on hardware advancements. Historically, developing these algorithms has required years of expert human collaboration. While large language models (LLMs) have accelerated discovery in mathematics and classical algorithms, their application to quantum computing has been limited. The primary bottleneck is the inability to verify general quantum algorithms without fault-tolerant hardware; classical simulation is restricted to small or restricted gate sets, limiting the design space for discovery. Consequently, there is a need for a framework that can discover, verify, and optimize quantum programs for large-scale, asymptotic applications beyond the reach of classical simulation.

Methodology

The authors introduce a multi-agent discovery workflow centered on a formal verification library built in the Lean theorem prover. This system pairs large language model agents with rigorous mathematical proofs to synthesize and verify quantum programs.

1. Formal Verification Library

The core of the system is a library based on Quantum Hoare Logic (QHL). It formalizes:

Classical-Quantum States: Combining classical control flow with quantum states.
Correctness: Expressed as Hoare triples (precondition, program, postcondition), verified via weakest precondition calculus.
Resource Counting: Formal bounds on expected and worst-case resource costs, specifically targeting the spacetime cost ( $Q \cdot T$ ), defined as the number of logical qubits ( $Q$ ) multiplied by the number of $T$ gates ( $T$ ). This metric is critical for fault-tolerant architectures where $T$ -gate distillation is the dominant overhead.

2. Multi-Agent Discovery Architecture

Researchers define a problem specification in Lean, stating the target correctness theorem and cost bounds with placeholders (sorry) for the solution.

Agent Teams: Independent teams of LLM agents are launched to explore candidate algorithms. Teams can range from single agents to hierarchical structures handling subroutines.
Collaboration: Teams share progress via a shared wiki (storing verified solutions, reusable lemmas, and notes on dead ends) and scheduled conferences (for discussing unverified conjectures and critiques).
Independent Verification: An external verifier, using the Lean Comparator, checks every submission against a frozen specification. This prevents agents from exploiting loopholes (e.g., weakening theorems or altering definitions) and ensures that only valid, machine-checked proofs are accepted.

Key Contributions

Formal Verification Framework for Quantum Algorithms: The paper presents a comprehensive Lean library that supports the formal verification of correctness and resource costs for dynamic quantum circuits, including mid-circuit measurements and classical control flow.
Multi-Agent Discovery Workflow: A novel research paradigm where human researchers define specifications, and autonomous agent teams collaborate to discover, optimize, and formally prove quantum algorithms.
Machine-Checked Solutions: The system produces quantum programs with machine-checked proofs of correctness and cost, eliminating the need for manual code review and enabling safe, large-scale collaboration.

Results

The workflow was applied to five distinct problems, yielding significant resource reductions compared to the strongest published baselines:

Problem	Application Domain	Baseline Cost ( $Q \cdot T$ )	This Work Cost ( $Q \cdot T$ )	Improvement
Parallel Grover Search	Unstructured Search	Strongest published protocols	Verified circuits	Up to 1.41× reduction in expected oracle rounds
Fixed-Point arcsin	State Preparation	$> 1.08 \times 10^8$	$3.70 \times 10^5$	290× reduction
$\alpha$ -particle Stopping Power	Inertial Confinement Fusion	$5.42 \times 10^{15}$	$4.98 \times 10^{14}$	10.9× reduction
Non-Born–Oppenheimer Dynamics	Photochemistry ( $C_{23}H_{20}N_3O$ )	$4.98 \times 10^{15}$	$6.16 \times 10^{14}$	8.08× reduction
Cytochrome P450 Compound I	Drug Metabolism	$1.09 \times 10^{12}$	$4.37 \times 10^{11}$	2.49× reduction

Specific Algorithmic Improvements

arcsin: Agents first optimized using a restricted "kickmix" gate set (verifiable via classical fuzzing) and then lifted the solution to the full Clifford+ $T$ set using formal verification, discovering a coefficient lookup mechanism that reduced $T$ -gate counts by 33%.
Stopping Power: The solution utilized a real-space grid representation to exploit Pauli exclusion, reducing the linear combination of unitaries (LCU) $\lambda$ norm. It also introduced a technique to reuse the total electron momentum register between walk steps, cutting $T$ -gate counts per step by 10%.
Non-Born–Oppenheimer Dynamics: Improvements included measurement-based uncomputation for coordinate loading, approximating $1/r$ potentials via Bernstein polynomials (avoiding expensive multiplication), and using reversible logic for nuclear charges instead of alias sampling.
Cytochrome P450: The solution replaced binary angle lookups with a one-hot register for orbital vectors, significantly reducing the $T$ -gate cost of state preparation and rotation application.

Significance and Claims

The paper claims that combining formal verification with LLM agents shifts the frontier of quantum algorithm development. By moving the human effort from manual circuit design and optimization to problem specification and scientific interpretation, the workflow enables the discovery of algorithms that are:

Beyond Classical Simulation: Capable of addressing problems requiring thousands of qubits and $10^9$ to $10^{15}$ logical operations, regimes where classical numerical testing is impossible.
Rigorously Verified: Every solution comes with a machine-checked proof of correctness and cost, ensuring reliability without the need for fault-tolerant hardware to test the algorithms.
Collaborative: The multi-agent system demonstrates that cross-team collaboration (via wikis and conferences) is essential, with the best solutions often emerging from the synthesis of ideas across multiple teams.

The authors emphasize that while these improvements are substantial, end-to-end simulations still demand resources beyond current early fault-tolerant hardware projections. However, the work establishes a path for cumulative resource reductions, narrowing the gap to practical quantum computation from the algorithmic side while hardware scales from the physical side. The paper concludes that this approach lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.