Ai teams discover verified quantum algorithms that outperform previous methods
Discovering formally verified quantum programs with AI
Artificial IntelligenceProgramming Languages
Summary
Quantum computers could solve important problems if they had better algorithms, but designing those algorithms is very hard. The authors show how teams of AI agents using a special math tool can create new, proven-correct quantum programs that improve on existing ones by big margins. These AI teams also discuss and share ideas to work together, speeding up discoveries beyond what people have done before. Their approach helps build quantum algorithms that classical computers cannot fully check yet, moving closer to practical quantum computing.
What this means in practice
- •For quantum software engineers: Create formally verified quantum programs with improved performance using AI agent collaboration within proof systems.
- •For pharmaceutical computation teams: Accelerate simulation of drug metabolism processes via improved quantum algorithms discovered and verified by AI agents.
Authors
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
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.