arXiv cs.AI· Hanchao Zhou, Jialei Li·· 10 天前AI 评分38
SCOPE：以语言模型为策略规划器的可验证定理证明
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
AI 导读
SCOPE 让语言模型在算子词表上做规划、符号引擎执行数值计算、编译器渲染证明，在 218 题测试集上用 135M 主干模型通过 191/218（87.6%）。
正文 · AI 翻译
摘要：在 Lean 等证明助手中，生成的证明必须通过机器编译检查，因此评估无需人工评分。直接生成在多步数值命题上会失败：只有当每个内容整数都正确时，证明才有效，因此通过率受限于每个整数准确率的 k 次方。对 2,617 个参考证明进行受控破坏，证实了这一幂律。SCOPE（状态条件算子规划与执行）强制实行自然的分工：模型在算子词汇表上进行规划，符号引擎执行数值计算，编译器渲染证明。在一个 218 个问题的测试套件上，它以 135M 主干网络认证了 191/218（87.6%）；7B 的 DeepSeek-Prover-V1.5-RL 认证了 18/218，但消耗了 27.5 倍的 token 和 37.5 倍的墙钟时间，而 DeepSeek-Prover-V2-7B 在双向对偶套件上认证为零。多步思考每个问题需要 6.12 个离散决策动作，且不产生自然语言思考文本。将决策框架中的滞后引擎状态替换为当前状态，可将通过率从 117/218 提升至 191/218，而提高链末端损失的权重则会产生负面影响。在公开的 Lean-Workbook 库中，3,536 个可评分且可接受的问题中有 2,132 个获得认证（60.29%），且在主套件上零退化。所有读数均来自版本冻结的审查，并经过独立复核和反向验证。限制自由生成并保持决策时信息可见，是比扩大模型更直接的途径。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.08319 [cs.AI] |
| （或 arXiv:2610.08319v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.08319 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Hanchao Zhou [查看电子邮件]
[v1]
2026年10月6日星期二 13:22:24 UTC（4,931 KB）
来源：arXiv cs.AI · arxiv.org