Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information

• URL: http://arxiv.org/abs/2607.21533v1
• Date: Thu, 23 Jul 2026 17:19:21 GMT
• Title: Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
• Abstract summary: 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.<n>We evaluate four models-GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3-within a common theorem-proving framework under two settings.<n>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.
• Score: 13.46344583931603
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• QuantumMind: Constraint-Grounded Agentic Reasoning for Speedup Analysis in Quantum Computing [30.648434508009988]
  We present QuantumMind, an auditable agentic workflow for generating and conservatively screening quantum-acceleration hypotheses.<n>A fixed sequence of typed, role-specialized actions formalizes the public task, analyzes structure and classical bottlenecks, and constructs a scoped candidate scheme.<n>We evaluate QuantumMind against seven task-adapted prompting and agentic controls on 582 identical open-discovery tasks.
  arXiv  Detail & Related papers  (2026-08-07T20:21:13Z)
• Qiskit QuantumKatas: Adapting Microsoft's Quantum Computing exercises for LLM evaluation [1.2891210250935148]
  We package Microsoft's QuantumKatas quantum computing curriculum with an evaluation framework for systematic LLM assessment.<n>The resulting benchmark comprises 350 tasks across 26 categories, spanning fundamental gates through advanced algorithms.<n>Each task includes a natural language prompt, canonical solution, and deterministic test verification via classical circuit simulation.
  arXiv  Detail & Related papers  (2026-05-26T16:02:08Z)
• QuanBench+: A Unified Multi-Framework Benchmark for LLM-Based Quantum Code Generation [39.32132630606808]
  We introduce QuanBench+, a unified benchmark spanning Qiskit, PennyLane, and Cirq.<n>We evaluate models with executable functional tests, report Pass@1 and Pass@5, and use KL-divergence-based acceptance for probabilistic outputs.<n>Across frameworks, the strongest one-shot scores reach 59.5% in Qiskit, 54.8% in Cirq, and 42.9% in PennyLane.
  arXiv  Detail & Related papers  (2026-03-25T20:51:21Z)
• AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
  We develop AQER, a scalable AQL method that constructs the loading circuit by systematically reducing entanglement in target states.<n>We conduct systematic experiments to evaluate the effectiveness of AQER, using synthetic datasets, classical image and language datasets, and a quantum many-body state datasets with up to 50 qubits.
  arXiv  Detail & Related papers  (2026-02-02T14:39:42Z)
• On-Chip Verified Quantum Computation with an Ion-Trap Quantum Processing Unit [0.5497663232622965]
  We present and experimentally demonstrate a novel approach to verification and benchmarking of quantum computing.<n>Unlike previous information-theoretically secure verification protocols, our approach is implemented entirely on-chip.<n>Our results pave the way for more accessible and efficient verification and benchmarking strategies in near-term quantum devices.
  arXiv  Detail & Related papers  (2024-10-31T16:54:41Z)
• QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
  Quantum computing is recognized for the significant speedup it offers over classical computing through quantum algorithms.<n>QCircuitBench is the first benchmark dataset designed to evaluate AI's capability in designing and implementing quantum algorithms.
  arXiv  Detail & Related papers  (2024-10-10T14:24:30Z)
• QKSAN: A Quantum Kernel Self-Attention Network [53.96779043113156]
  A Quantum Kernel Self-Attention Mechanism (QKSAM) is introduced to combine the data representation merit of Quantum Kernel Methods (QKM) with the efficient information extraction capability of SAM. A Quantum Kernel Self-Attention Network (QKSAN) framework is proposed based on QKSAM, which ingeniously incorporates the Deferred Measurement Principle (DMP) and conditional measurement techniques. Four QKSAN sub-models are deployed on PennyLane and IBM Qiskit platforms to perform binary classification on MNIST and Fashion MNIST.
  arXiv  Detail & Related papers  (2023-08-25T15:08:19Z)
• Quantum circuit architecture search on a superconducting processor [56.04169357427682]
  Variational quantum algorithms (VQAs) have shown strong evidences to gain provable computational advantages for diverse fields such as finance, machine learning, and chemistry. However, the ansatz exploited in modern VQAs is incapable of balancing the tradeoff between expressivity and trainability. We demonstrate the first proof-of-principle experiment of applying an efficient automatic ansatz design technique to enhance VQAs on an 8-qubit superconducting quantum processor.
  arXiv  Detail & Related papers  (2022-01-04T01:53:42Z)
• On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
  We devise three effective QAE-based learning protocols to address three classically computational hard learning problems. Our work sheds new light on developing advanced quantum learning algorithms to accomplish hard quantum physics and quantum information processing tasks.
  arXiv  Detail & Related papers  (2021-06-29T14:01:40Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.