AI 中文总结
研究人工智能智能体在量子算法和信息定理证明的能力，引入两个Lean 4基准测试，在通用框架下评估四个模型，发现LAD可提升性能，揭示智能体证明弱点及模型成本差异，为开发更优证明智能体提供基线。
AI 中文摘要
形式验证在量子计算中日益实用，但人工智能智能体在此领域构建机器可检查证明的能力仍未得到衡量。我们引入了Lean-QuantumAlg-Bench和Lean-QIT-Bench这两个Lean 4基准测试，分别包含36个和40个量子算法与量子信息理论的定理完成任务。每个任务在固定环境中编译，并通过确定性证明检查和有针对性的语义审查进行评估，在模型执行前分配难度权重。我们在通用定理证明框架下，在两种设置下评估了四个模型：仅任务基线和库增强演绎（LAD）。结果显示LAD提高了分数和完成率，揭示了智能体证明在某些领域的反复出现的弱点，各模型每得分点的成本也有很大差异。我们期望这些基准测试为开发更有能力和可靠的证明智能体建立可重复的基线，并为推进量子信息科学的自我进化人工智能科学家铺平道路。
英文摘要
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.
Comments22 pages, including appendix; 4 figures
