AI is designing quantum programs for machines that cannot run them yet
Google researchers report lower-cost algorithms checked with a proof assistant. The advance concerns what future machines would need to do, with important assumptions still in human hands.
Reading tools for text size, copying, printing and your reading list
Google researchers have reported a way to improve quantum programs without waiting for a quantum computer powerful enough to run them. Their AI systems propose algorithms and mathematical proofs; a separate checking process assesses whether the programs satisfy the researchers’ requirements.[1]
The attraction is practical. Useful quantum computing depends on the work a machine must perform as well as the machine’s capabilities. Reducing that workload could bring demanding calculations closer to reach. The new preprint reports progress on that software side, rather than a faster processor or a laboratory demonstration of a new medicine.[1]
Submitted to arXiv on November 6, the study is by researchers from Google DeepMind and Google Quantum AI, with research consultants. The preprint has not yet been peer reviewed. It has not established that today’s quantum hardware can perform the proposed large scientific calculations.[1]
Checking an answer without running the experiment
Ordinary software testing tries inputs and checks outputs. That becomes difficult when the proposed program describes a quantum calculation too large to simulate on available classical machines, while suitable quantum hardware does not yet exist.[1]
Formal verification offers a different kind of evidence. A program is described mathematically, alongside a precise statement of what it must accomplish. A proof then connects the program to that statement. Lean, the open-source language and proof assistant, checks the formal reasoning rather than relying on the AI’s explanation of why its answer looks correct.[2]
A simple bookkeeping example illustrates the distinction. Testing a calculator on a thousand purchases checks those examples. A valid proof of the specified arithmetic could cover every permitted input. Neither exercise tells you whether the shop’s price list was correct. That question belongs to the assumptions supplied to the calculation.
For quantum science, those assumptions include the physical model, the allowed inputs, the acceptable error and the cost being minimized. A rigorous answer to the wrong scientific question would still be the wrong answer for the scientist.
The AI must not move the goalposts
The paper describes teams proposing programs and proofs, sharing useful results and recording failed ideas. An external verifier checks submissions against fixed specifications. This separation matters because an agent could otherwise make a difficult task easier by quietly changing what it had been asked to prove.[1]
The underlying Lean Comparator documentation makes the distinction concrete: checking a submitted proof includes checking that it proves the original statement and uses only permitted assumptions. Those guarantees themselves depend on a trusted checking environment. Formal verification is a carefully defined chain of reasoning, not an unrestricted certificate that everything associated with a result is true.[3]
This leaves humans with consequential work. They choose the problem and review whether its formal version captures the intended science. They must also decide whether a cheaper solution is useful enough to pursue.
Cheaper on paper has a precise meaning
One scientific example concerns a calculation relevant to fusion research. The authors report about a 10.9-fold reduction in a cost measure that multiplies by T gates, a type of operation expensive in error-corrected quantum computing. Logical qubits are protected units of quantum information, not a count of bare physical components. In this example the logical-qubit count falls from 5,650 to 4,374, about 23%. The larger improvement in the combined measure also reflects fewer counted operations.[1]
That combined measure should not be read as 10.9 times faster on an existing machine. Consider an invented example: a design requiring half as many logical qubits and half as many counted operations improves their product fourfold. It does not automatically finish four times sooner. Hardware layout, operation rates and the resources used to supply those operations still matter.
The paper discusses such architectural qualifications and says its scientific calculations still require substantially more resources than the first fault-tolerant machines are projected to provide. The improvement narrows a software requirement; it does not remove the hardware problem.[1]
The next test is public scrutiny
The manuscript says the researchers intend to release their Lean library, problem specifications and verified solutions. That promise is an important next milestone. This article reports the authors’ verification results; it does not claim an independent reproduction of their proofs.[1]
The most useful outcome would be a reusable collection of precisely stated programs that other researchers can inspect, challenge and improve. A smaller resource count becomes more persuasive when readers can examine both the program and the question it answers.
The broader lesson is encouraging: the path to useful quantum computing can improve before the hardware arrives. Keeping the specification, proof and physical machine separate is what lets that progress be measured honestly. This is a different result from the AI-assisted proof about quantum query limits that QubitWire reported earlier: here the subject is discovering and checking programs against specified tasks.