arXiv cs.AI· Hanchao Zhou, Jialei Li·2026-10-07 12:00· 9 小时前AI 评分31

SCOPE：以语言模型为策略规划器的可验证定理证明框架

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

AI 导读

SCOPE 用语言模型规划算子、符号引擎执行数值、编译器渲染证明，在 218 题测试集上以 135M 主干模型通过 191/218（87.6%）。相比之下，7B 的 DeepSeek-Prover-V1.5-RL 仅通过 18/218，且消耗 27.5 倍 token 与 37.5 倍耗时；DeepSeek-Prover-V2-7B 在双向对偶测试集上通过为零。

来源：arXiv cs.AI · arxiv.org

DeepSeek 推理能力数据与训练论文研究 #论文/研究 #推理 #数据/训练 #DeepSeek