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

SCOPE 提出用语言模型做策略规划、符号引擎执行数值计算、编译器校验证明的定理证明方案，以解决直接生成在多步数值命题上因逐整数正确率连乘而失败的问题。研究在 2,617 条参考证明上做受控破坏实验，验证了通过率随逐整数准确率呈幂律下降。