Lean-QuantumAlg-Bench 和 Lean-QIT-Bench 评估 AI 定理证明

研究者发布两个 Lean 4 基准：Lean-QuantumAlg-Bench（36 个任务）和 Lean-QIT-Bench（40 个任务），用于评估 AI 在量子算法和量子信息理论上的定理证明能力。在四个模型（GPT-5.5、Kimi K3、DeepSeek V4-Pro、MiniMax M3）中，最高难度加权得分分别为 60.4/100 和 59.6/100。库增强推理（LAD）在所有八个模型-基准对比中均提升得分和完成率，最高提升 15.9 分。模型在量子模拟、量子学习、量子信息度量等领域的证明能力存在薄弱环节。