Google AI Agents Cut Quantum Algorithm Resource Costs by Up to 290x

Google researchers used teams of AI agents to cut the resources some quantum algorithms need by up to 290 times, and every result arrived with a machine-checked proof that the program works and costs what it claims. The work comes from Google DeepMind and Google Quantum AI. The preprint, "Discovering formally verified quantum programs with AI," was posted to arXiv on Nov. 6 and revised on Nov. 9. It lists 25 authors, led by Sergey Shirobokov, Ben Jaderberg and Katerina Hristova.

Why verification was the bottleneck

The paper attacks a problem that has constrained automated quantum program search for years. Quantum programs for useful chemistry or physics are too large to test on today's hardware or to simulate on classical machines. Earlier automated searches were therefore limited to small instances a classical computer could check.

The Google team built a quantum programming library inside the Lean theorem prover. Each task in the library states the required calculation, the target accuracy, and how resources are counted. Agents must then produce programs that satisfy the specification and prove both correctness and cost. When a proof fails, the agents use Lean's error messages to revise their work. A separate checker confirms the final solution still matches the original specification, which prevents an agent from quietly weakening the task to pass.

What did the agents achieve?

The team measured cost mainly as logical qubits multiplied by T gates, the operations that are most expensive on error-corrected hardware. Against prior baselines the paper reports:

• A 290-fold resource reduction for a quantum arithmetic routine, an arcsine calculation
• Up to 2.55 times better performance for parallel search
• Roughly 11-fold reduction for a fusion simulation
• About 8-fold reduction for a photochemistry simulation
• About 2.5-fold reduction for a drug-metabolism simulation

The fusion task models how an alpha particle slows in inertial-confinement fuel containing 218 electrons and 216 fixed protons. Logical qubits fell from 5,650 to 4,374. Combined cost fell by a factor of 10.9.

The photochemistry gain of 8.08 times came against a baseline that already included earlier improvements. The largest single step, 34%, came when one agent team's idea was refined and proved by another team. The drug-metabolism task modeled a 63-electron representation of the cytochrome P450 enzyme's Compound I and improved 2.49 times.

How the agent teams worked

The agents did not work in isolation. Teams shared programs, partial proofs and failed attempts through a common wiki. They also held scheduled virtual "conferences" to exchange ideas. Humans chose the problems, wrote the specifications and interpreted the results. The collaboration between agent teams proved productive: the biggest photochemistry improvement came directly from one team building on another's approach.

What are the limits?

The researchers state the limits plainly. The scientific programs remain beyond what early fault-tolerant machines are projected to run, and improvements of several orders of magnitude are still needed before the code fits on such hardware. Results also depend on how specifications are written. The photochemistry program, for example, had to be correct for every input state, including physically invalid ones. The P450 molecular representation was fixed in advance.

The team plans to open-source the Lean library, the problem specifications and the verified solutions. The work joins other recent cases of AI systems producing checkable mathematics, including an unreleased Anthropic model's proof of the Aaronson-Ambainis conjecture.

If agent-driven optimization continues at this pace, formally verified quantum programs could shrink faster than fault-tolerant hardware roadmaps expand, tightening the target that future quantum machines must hit.