在 Lean 等交互式证明助理中，生成的证明必须通过机器编译检查，无需人工评分。直接生成在多步数值命题上表现不佳，因为每个整数的正确率决定整体通过率，呈现 $k$ 次方的幂律关系。对 2,617 条参考证明进行受控破坏实验验证了该幂律。
SCOPE（State‑Conditioned Operator Planning and Execution）通过自然的分工来突破瓶颈：语言模型在操作符词表上进行规划，符号引擎负责数值计算，编译器负责生成最终证明。实验在 218 题套件上，使用 1.35 亿参数的骨干模型认证通过 191 题（87.6%）。相比之下，7B 参数的 DeepSeek‑Prover‑V1.5‑RL 仅在 27.5 倍的 token 消耗和 37.5 倍的时钟时间下认证通过 18 题，DeepSeek‑Prover‑V2‑7B 在双向对偶套件上未能认证任何题目。
多步思考平均需要 6.12 次离散决策动作，且不产生自然语言思考文本。将决策框架中的滞后引擎状态替换为当前状态，可将通过率从 117/218 提升至 191/218；而对链尾损失加权则会降低性能。
在公开的 Lean‑Workbook 库中，3,536 道可评分的合格题目中有 2,132 道（60.29%）得到认证，且对主套件没有出现回归。所有结果均来源于版本冻结的审查，经过独立复核和逆向验证。
限制自由生成并保持决策时信息可见，被证明比单纯扩大模型规模更为直接有效。
点评