SCOPE 让 135M LLM 只规划证明算子、由符号引擎执行数值，在 Lean 中认证 87.6% 多步数值命题

Zhou 与 Li 提出 SCOPE（State-Conditioned Operator Planning and Execution）：语言模型不直接生成完整 Lean proof，而只在受限 operator vocabulary 上做 state-conditioned 规划，符号引擎执行数值计算、编译器生成最终证明，从架构上规避多步数值证明中“任一整数出错即整体失败”的误差累积。论文在 218 题 suite 上使用 135M backbone 认证 191 题（87.6%）；7B DeepSeek-Prover-V1.5-RL 认证 18 题且消耗 27.5 倍 tokens、37.5 倍 wall-clock。SCOPE 还在 Lean-Workbook 的 3,536 个可评分 admissible problems 中认证 2,132 个（60.29%），并报告 version-frozen review、independent rechecks 与 reverse verification。