arXiv · cs.AI· Hanchao Zhou, Jialei Li·· 6 小时前精选
SCOPE：以语言模型规划操作符实现可认证定理证明
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
arXiv:2610.08319v2阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Hanchao Zhou, Jialei Li
研究任务与主要进展
SCOPE 让语言模型负责操作符规划、符号引擎执行数值计算并由编译器检查证明，在218题套件中用135M模型认证191题（87.6%）。
阶段、条件与复现 · 深读核对
- 新能力对应什么具体任务与最小输入输出？
- 代码、模型、数据、许可与可用入口是否明确？
- 效果、总成本、失效条件与实际工作流如何验证？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
本站判断
SCOPE 将语言模型的规划、符号引擎的数值执行与编译器证明检查分工，并用当前引擎状态进行决策，针对多步数值命题中逐步正确性导致的快速失败问题。基于论文摘要，135M 模型在218题套件中认证191题，且与更大模型、更高 token 和更长墙钟时间相比具有明显效率；但当前材料仅为摘要，尚不能核验具体证明和基准细节。本站设想：可在相同模型规模、token与墙钟预算下，进一步比较状态更新策略对多步数值命题通过率和证明成本的影响。
来源：arXiv · cs.AI · arxiv.org