这篇题为《基准测试智能体在量子算法与量子信息理论中的定理证明能力》的论文，旨在通过创建一个严格的测试来回答这个问题。研究人员为 AI 智能体构建了两个巨大的“考场”：一个名为 Lean-QuantumAlg-Bench，包含 36 个关于量子算法（如著名的破解密码的 Shor 算法）的棘手问题；另一个名为 Lean-QIT-Bench，包含 40 个关于量子信息理论（涉及信息如何在量子系统中存储和移动）的问题。他们不仅仅是让 AI 去猜测，而是将问题交给四种不同的顶级 AI 模型，观察这些模型是否能写出计算机认可的正确证明。结果是希望与现实的碰撞。AI 模型成功解决了一些问题，表现最好的得分在算法测试中达到了约 60/100，在信息理论测试中达到了 59.6/100。然而，论文发现 AI 在模拟量子系统和理解纠缠（entanglement）等特定领域表现得非常吃力。一个关键的发现是，给 AI 一个“已验证库（verified library）”——即一份已证实的既有事实“小抄”供其查阅——显著提升了其性能，在某些情况下将分数提高了多达 15.9 分。这表明，虽然 AI 尚未准备好成为一名完全独立的量子科学家，但如果它能获得经过信任、预先检查过的知识来引导其推理，它的能力会大大增强。该研究还强调，不同的 AI 模型具有截然不同的“成本”，有些比其他模型更便宜或更快，这表明不存在唯一的“最佳”机器人，而是在速度、成本和智能之间存在权衡。
技术摘要：用于证明量子算法与量子信息定理的智能体基准测试
问题陈述 尽管形式化验证在量子计算领域正变得日益实用，但 AI 智能体在该领域构建机器可检查证明的能力尚未得到量化。量子形式化呈现出独特的挑战：量子态与算符具有有限维度的类型级结构；电路计算需要将句法变换与线性代数语义相联系；此外，信息论不等式依赖于特定的定义域、支撑集条件以及正定性假设。此外，教科书式的符号表示往往忽略了强制类型转换（coercions）、基底选择以及张量因子顺序，而这些在 Lean 等定理证明器中必须是显式的。现有的基准测试（如 miniF2F、PutnamBench）侧重于通用数学或竞赛问题，而特定领域的评估则往往缺乏受控的库访问或针对其预期数学主张的严格语义验证。因此，需要一个可复现的基准，以评估 AI 智能体在处理量子算法与量子信息理论所需的特定接口和类型化结构时的表现。
意义与主张 本文声称这些基准测试为开发更强大、更可靠的证明智能体建立了可复现的基准。通过隔离库访问的影响并提供受控的评估环境，这项工作使得衡量量子科学领域内智能体证明能力的进展成为可能。结果表明，经过验证的库是强化特定领域证明智能体的关键组件，特别是在量子模拟和纠缠理论等复杂领域。作者将这项工作定位为迈向能够推进量子信息科学的“自我进化 AI 科学家”的一步，尽管他们也指出，当前的智能体在特定子领域仍存在反复出现的弱点。本文的主旨并非声称已解决所有量子问题的形式化验证，而是提供了测量并改进该领域智能体性能所需的必要基础设施。