SCOPE 框架用 135M 模型在 Lean 定理证明上超越 DeepSeek-Prover
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
一个 135M 的小模型在 Lean 证明上干翻了 7B 的 DeepSeek-Prover，靠的是让符号引擎算数、模型只做规划，思路挺反直觉的。
SCOPE（State-Conditioned Operator Planning and Execution）让语言模型只负责规划操作符，数值计算交给符号引擎，证明由编译器在 Lean 中验证。在 218 题测试集上，135M 主干模型证明 191/218（87.6%），而 7B 的 DeepSeek-Prover-V1.5-RL 只证明 18/218，消耗的 token 是前者的 27.5 倍、时间是 37.5 倍。论文在 2,617 条参考证明上验证了逐整数准确率与通过率之间的幂律关系。在公开的 Lean-Workbook 库上，3,536 道可评定题目中 2,132 道通过验证（60.29%）。消融实验显示，把决策帧中的滞后引擎状态换成当前状态可将通过率从 117/218 提升到 191/218。
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.