An AI-assisted proof puts a limit on quantum speedups for random inputs

A PSI research system used an unreleased Anthropic model to produce a proof of the Aaronson-Ambainis conjecture, formalized in Lean.

A quantum computer can query multiple positions in a bit string in superposition. Scott Aaronson and Andris Ambainis asked how many bits a classical computer would need to read to reproduce its behavior on random inputs. On November 6, the research lab Physical Superintelligence (PSI) published a proof of their conjecture alongside a formalization in Lean. What the gap between the two computers measures

In the setting studied, the computation returns a yes-or-no answer. For most uniformly sampled bit strings, a classical computer can estimate the probability that the quantum computer answers yes. For a fixed accuracy and a fixed fraction of exceptions, the number of classical reads is bounded by a polynomial in the number of quantum queries. The bound counts accesses to the input. Total runtime also includes the work performed between queries and is a separate question.

In August, Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan established this consequence in a special case. Their result applied to quantum procedures that query their input in a fixed number of parallel rounds. According to PSI, the four researchers have examined the new proof, shared feedback, and are preparing a shorter exposition. The bit worth reading

The link to polynomials comes from the probability of answering yes. After (T) quantum queries, that probability can be expressed as a polynomial of degree at most (2T) in the input bits. In their original paper, Aaronson and Ambainis showed that a bound on the influence of those bits would give the classical computer a way to decide which ones to read.

To measure a bit’s influence, flip it, square the resulting change in the polynomial’s value, and average over all possible inputs. The proof guarantees that if the polynomial varies and stays between 0 and 1, at least one bit meets an influence threshold determined by the degree and variance. For a fixed variance, the threshold decreases as an inverse power of the degree and is independent of the total number of bits. The proof follows an approach proposed by Shachar Lovett and Jiapeng Zhang and builds on a result by David Reimer to pair up bit configurations. From AI-assisted research to verification in Lean

According to PSI, its system produced a first complete proof on the third day of a run on its own infrastructure, using an unreleased Anthropic model. David Turturean designed the system, scoped the problem, launched the run, and reviewed the manuscript prepared from the results.

The formalization in the Lean 4 repository covers the influence bound at the heart of the conjecture. Two independent implementations of the proof checker accepted the formal proofs, according to PSI’s logs. The implications for quantum computing are developed in the manuscript and fall outside the scope of that verification.