Lean证明修复最高提32%求解率，多解82个定理！
Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4
📖 AI 总结
该论文针对自动定理证明中语言模型采样丢弃编译器错误信息的问题，提出一种有界的在线步骤级修复模块：每步采样K个候选策略，对失败策略最多修复R次，将Lean 4编译器返回的错误信息输入预训练修复模型，就地修正被拒绝的单个步骤，而非简单重新采样。在LeanDojo基准的1990个定理子集上，该方法在所有候选预算（K为1、3、5、8）下均优于纯采样基线，相对提升最高达32%，多解出82个定理。研究进一步刻画了修复的代价与收益特征：修复以额外运行时间换取可达证明，采样受限时收益最大，且收益前置，首次修复尝试即贡献总增益的84%至96%；增益几乎全部来自浅层策略执行失败，而非类型不匹配等结构性错误。该方法在Lean Workbook基准上成功复现，求解率接近翻倍且无性能回退。
🔑 关键词速览
| Lean 4 | 一种交互式定理证明器，同时是编程语言，用于形式化数学和验证软件。 |
| 策略（tactic） | 在定理证明中用于逐步构造证明的命令或指令。 |
| 步骤级修复（step-level repair） | 在证明搜索过程中，针对单个失败步骤利用错误信息进行就地修正的技术。 |
| LeanDojo | 一个用于Lean定理证明的基准数据集和工具包，包含大量形式化数学定理。 |
| 求解率（solve rate） | 在给定基准上成功证明的定理数量占总定理数量的比例。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅