Agentic Autoresearch with Formal Verification for Quantum Algorithms

Here we present a scheme of autoresearch leveraging AI agents for quantum algorithms, using as an example the implementation of recursive Toom-Cook multiplication circuits due to Kahanamoku-Meyer & Yao (2024) inside the order finding circuit for Shor's algorithm. The recursive scheme allows for asymptotically more efficient circuits than schoolbook multiplication, but the design landscape for detailed implementations of the recursive circuitry is complex. Here we expose this landscape for AI agents to explore, while constraining such exploration within the confines of formal verification. We report that the agentic exploration so far has yielded a meaningful reduction in arithmetic operation count with respect to the previously published constructions (26.7%-34.5% reduction in arithmetic operations across different circuit families). The formally verified harness that we publish is open to receive further contribution from any agents that one may deploy towards this problem.