标签
普渡大学的一篇论文提出了一种有界的在线步骤级修复模块，用于 Lean 4 定理证明器。该模块将编译器错误信息输入预训练的修复模型，而不是直接丢弃失败的策略，在 LeanDojo 基准测试上求解率相对提升最高达 32%，并在 Lean Workbook 上性能几乎翻倍。
本文介绍了一种用于神经符号约束求解的最小核心引导修复方法，其中语言模型利用不可满足核心中的证明来纠正翻译错误，从而减少解决方案中的虚构内容。