Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information

AI summary

Overview

Research area: AI for formal theorem proving (Lean 4) applied to quantum algorithms and quantum information theory.

Technical level: Advanced. The paper assumes familiarity with dependent type theory, Lean 4 proof engineering, and graduate-level quantum information concepts, though its headline results are readable without that background.

Scope (one sentence): The paper introduces two Lean 4 theorem-completion benchmarks (36 tasks for quantum algorithms and 40 for quantum information theory) and reports a descriptive, single-run evaluation of four AI models under a task-only baseline and a library-augmented setting.

What This Paper Is About

Formal verification of quantum results in proof assistants such as Lean is becoming practical, but no benchmark has measured whether AI agents can actually construct machine-checkable proofs of quantum theorems. The authors build two coordinated Lean 4 benchmark suites covering quantum algorithms and quantum information theory, and use them to measure how well four current models complete proofs, at what monetary and wall-clock cost, and which subfields remain hard. The goal is a reproducible baseline that later proof agents and "self-evolving AI scientists" can be measured against.

Key Contributions

1. Two coordinated benchmarks. Lean-QuantumAlg-Bench (QAlg-Bench) contains 36 theorem-completion tasks and Lean-QIT-Bench (QIT-Bench) contains 40, giving 76 tasks in total, built on Lean 4 and on the authors' Lean-QuantumAlg and Lean-QIT libraries. Both suites share a common theorem-completion contract and the same deterministic proof checks.

2. A six-field taxonomy with pre-assigned difficulty weights. Each suite is partitioned into three fields with fixed difficulty denominators: QAlg-Bench into state and operator methods (SOM, denominator 67), circuit and algebraic algorithms (CAA, 105), and simulation, signal processing and learning (SSL, 93); QIT-Bench into quantum channels and representations (QCR, 80), operator and state geometry, symmetry and distinguishability (GSD, 138), and quantum information measures and entanglement (IME, 109). Per-task difficulties $d_i \in {1,\dots,10}$ were fixed before any model execution, and the score is $100 \sum_i d_i v_i / \sum_i d_i$, where $v_i \in {0,1}$ is the verified acceptance indicator.

3. A two-condition evaluation protocol. Every model runs under a task-only baseline and under library-augmented deduction (LAD), which additionally grants consultation access to a verified domain library. Sixteen suite–model–condition combinations are recorded (4 models × 2 suites × 2 conditions), each with a fixed suite version, budget, retry policy and execution environment.

4. Capability–efficiency accounting. Beyond score and completion rate, the paper reports cost per score point in USD and in seconds, exposing trade-offs that performance rankings alone hide.

Main Findings

• Top scores stay near 60 out of 100. The highest difficulty-weighted scores reported are 60.4 on QAlg-Bench and 59.6 on QIT-Bench. GPT-5.5 had the highest observed score in every suite–condition combination.

• LAD helps in all eight within-model comparisons. Every historical baseline-to-LAD pair shows higher score and higher completion under LAD, with gains of up to 15.9 score points. The largest absolute increases named are 15.9 points for GPT-5.5 on QIT-Bench and 11.7 points for DeepSeek V4-Pro on QAlg-Bench.

• Relative gains can be misleading. MiniMax M3 doubles its QAlg-Bench score from 6.4 to 12.8 (+100.0% score, +200.0% completion) from a very low baseline, whereas other models post smaller percentages with larger absolute movement.

• Field-level profiles are uneven. SSL on QAlg-Bench and IME on QIT-Bench stay comparatively weak across models; GPT-5.5's QIT-Bench scores are much higher on QCR and GSD than on IME. GPT-5.5's largest single field change is a 30.4-point rise in GSD.

• Local regressions can hide inside aggregate gains. DeepSeek V4-Pro rises 13.3 and 18.3 points in CAA and SSL on QAlg-Bench but declines 7.5 points in QCR on QIT-Bench; its QIT-Bench suite-wide score moves only from 16.8 to 17.1 because other fields offset the decline. MiniMax M3 remains at 0.0 in SSL and in IME under both conditions. Kimi K3 shows a +6.7 net change in CAA on QAlg-Bench (two tasks verified only under LAD, one only under baseline) and +8.8 in QCR on QIT-Bench from one additional verified task with no regression, with its other fields unchanged.

• Cost rankings differ from capability rankings. DeepSeek V4-Pro has the lowest reported economic cost per score point, and GPT-5.5 the lowest observed time cost per score point, despite GPT-5.5 leading on score. Economic-cost comparisons for MiniMax M3 are reported as N/A.

• Direction of cost change under LAD varies. Table 1 shows score and completion always up, but economic cost per score point rises for Kimi K3 on QAlg-Bench (+19.9%) and falls elsewhere where measurable (for example −40.4% for DeepSeek V4-Pro on QIT-Bench, −17.0% for GPT-5.5 on QAlg-Bench). Time cost per score point falls in all eight comparisons, from −4.0% to −33.1%.

• Timeouts are not automatic failures. A model-call timeout does not set $v_i=0$; an independent Lean check runs on the final submission. Four tasks in the snapshot timed out yet still passed final verification.

• Caveats the authors state explicitly. Each suite–model–condition combination is one recorded run; historical baseline and LAD pairs are not fully matched on execution details; GPT-5.5 uses a different agent tool from the other three models, so cross-model orderings compare joint model-plus-tool settings; and no confidence intervals or significance tests are reported. The LAD differences are therefore described as properties of the recorded runs, not as estimates of an access-condition effect.

Methodology in Plain English

The authors first selected source problems from standard quantum information and quantum algorithms literature, keeping only claims that are scientifically relevant, theorem-sized, and expressible in a fixed Lean task format. Researchers fixed the mathematical scope, assumptions and conclusion; AI agents assisted with translating statements into Lean. Every admitted task was compiled in a fixed Lean environment before inclusion, and every task ships with no hints.

Quality was handled on two levels. Compilation and automated screening are universal mechanical guarantees applied to all 76 tasks. Because the Lean kernel certifies only that a proof inhabits the stated type, not that the statement means what the source meant, the authors additionally performed a manual comparison of formal signature, supporting definitions and mathematical specification for selected high-risk statements, checking objects and quantifiers, explicit and implicit assumptions, dimensional constraints, index and tensor ordering, and the direction and strength of the conclusion. They state this targeted review is not a benchmark-wide semantic validity rate.

Evaluation used a fixed theorem-completion contract: the agent receives the theorem signature plus supporting definitions (and, under LAD, a verified reference library for consultation), and success means the submitted proof compiles, introduces no new axioms, contains no sorry, and leaves files outside the theorem body unchanged. Acceptance is checked by an independent final verification after the agent invocation ends. Performance is aggregated two ways: a difficulty-weighted score using weights fixed before execution, and an unweighted completion rate. Costs are converted into two ratios, USD per score point (mean list-price-equivalent API cost over tasks with reconstructable prices, divided by the corresponding score) and seconds per score point (mean model invocation time per task over the full suite, divided by the overall score), with pricing fixed on 2026-07-20 and Kimi K3 prices fixed on 2026-07-22.

Why This Matters

Research impact. The paper separates two questions that are often conflated in formal-proving evaluation: whether a proof is mechanically accepted, and whether the benchmark statement faithfully represents the intended mathematics. Its 76-task, six-field structure with pre-registered difficulty weights gives the quantum formalization community a baseline that also reveals where the hard interfaces are (index bookkeeping, tensor ordering, coercions, asymptotic LOCC reasoning) rather than producing a single aggregate number.

Real-world applications.

• Verifying quantum algorithm implementations: the benchmark tasks include Walsh–Hadamard decoding, eigenvectors of modular multiplication in Shor-style order finding, and LCU block encoding from PREPARE and SELECT, all of which underlie circuit-level correctness claims.
• Certified quantum information theory: channel representations, trace-norm and fidelity bounds, entropy and entanglement measures, Holevo/Fano-type bounds, and entanglement concentration are the mathematical substrate of quantum communication security arguments.
• Tooling for proof-assistant libraries: field-level weak spots such as quantum simulation, quantum learning, information measures and entanglement theory indicate where library interfaces and lemmas should be extended.
• Cost-aware deployment of AI proof assistants: reporting USD and seconds per score point lets teams pick a model by budget and latency constraints rather than by score alone.

Industry relevance. The results give a concrete picture of the current capability ceiling (top scores around 60 on a 100-point difficulty-weighted scale) and of the capability–efficiency trade-off, which matters to groups building AI-assisted formal verification pipelines in quantum hardware, quantum-safe cryptography, and proof-assistant tooling.

Future Directions

• Matched reruns to isolate the LAD effect. The authors state that matched reruns are required to separate library access from execution-detail differences, since the historical baseline and LAD pairs are not fully matched.
• Closing the weak fields. SSL on QAlg-Bench and IME on QIT-Bench remain weak across models, and GPT-5.5 shows a large QCR/GSD versus IME gap on QIT-Bench; targeted library development and agent strategies for these areas are the natural next step.
• Benchmark-wide semantic validation. The manual comparison is currently applied only to selected high-risk statements; extending it, or automating fidelity checks, would let scores be interpreted against meaning as well as kernel acceptance.
• Reducing the model–tool confound. Because GPT-5.5 ran with a different agent tool from the other three models, rerunning all models under an identical agent harness is needed before cross-model orderings can be attributed to the models themselves.

Target Audience

Researchers in AI-for-mathematics and automated theorem proving who need domain-specific Lean benchmarks; quantum information and quantum algorithms researchers interested in formal verification; developers of Lean libraries such as Lean-QuantumAlg and Lean-QIT; and engineering teams evaluating AI proof agents under real cost and latency constraints. Readers seeking a gentle introduction to Lean or to quantum information will find the paper demanding, since it presumes familiarity with both.

Authors’ abstract

Formal verification is becoming increasingly practical for quantum computing, yet the ability of AI agents to construct machine-checkable proofs in this domain remains unmeasured. We introduce Lean-QuantumAlg-Bench and Lean-QIT-Bench, two Lean 4 benchmarks containing 36 and 40 theorem-completion tasks for quantum algorithms and quantum information theory, respectively. Every task compiles in a fixed environment and is evaluated by deterministic proof checking and targeted semantic review, with difficulty weights assigned before model execution. We evaluate four models-GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3-within a common theorem-proving framework under two settings: a task-only baseline and library-augmented deduction (LAD), which additionally provides access to a verified domain library. The highest difficulty-weighted scores are 60.4 out of 100 on the quantum-algorithm benchmark and 59.6 out of 100 on the quantum-information benchmark. LAD improves both score and completion rate in all eight model-benchmark comparisons, with gains of up to 15.9 points, providing evidence that verified libraries can strengthen domain-specific proof agents. The results reveal recurring weaknesses of agentic proving in areas such as quantum simulation, quantum learning, quantum information measures, and entanglement theory. Monetary and wall-clock costs per score point also vary substantially across models, highlighting important capability-efficiency trade-offs. We expect these benchmarks to establish a reproducible baseline for developing more capable and reliable proof agents, and to pave the way toward self-evolving AI scientists for advancing quantum information science.