Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information

Research Overview

Formal verification is increasingly vital for quantum computing, where complex mathematical chains require rigorous, machine-checkable proofs. This paper introduces two new benchmarks, Lean-QuantumAlg-Bench and Lean-QIT-Bench, designed to evaluate the ability of AI agents to construct proofs in Lean 4 for quantum algorithms and quantum information theory. The benchmarks consist of 76 tasks across six specialized fields, ranging from quantum simulation to entanglement theory.

The researchers evaluated four models (GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3) under two conditions: a task-only baseline and library-augmented deduction (LAD). In the LAD setting, agents were provided access to a verified domain library to assist in proof construction. Each task was evaluated using deterministic proof checking within the Lean environment, with difficulty weights assigned to tasks prior to execution to provide a nuanced view of model capabilities.

The study demonstrates that providing agents with access to verified libraries significantly enhances their performance. In all eight model-benchmark comparisons, LAD resulted in higher completion rates and difficulty-weighted scores, with improvements reaching up to 15.9 points. Despite these gains, the results highlight persistent weaknesses in areas such as quantum learning and entanglement theory. Furthermore, the analysis reveals significant trade-offs between model performance, monetary cost, and wall-clock time, suggesting that efficiency varies substantially across different agentic architectures.

These benchmarks provide a reproducible, standardized framework for assessing AI agents in the domain of quantum information science. By establishing a baseline for formal verification, the work helps identify the current limitations of automated theorem proving and offers a pathway toward developing more reliable, self-evolving AI scientists capable of advancing complex quantum research.