★ 2
新方法用 Lean 4 编译器报错修复定理证明，解出率提升 32%
论文提出有界在线步骤级修复模块：每步采样 K 个策略，失败时把 Lean 4 编译器错误信息喂给预训练修复模型就地修正，而非丢弃重采样。在 LeanDojo 1990 条定理子集上最多取得 32% 相对提升、多解出 82 条定理，收益主要来自浅层策略执行错误。该方法在 Lean Workbook …
arXiv cs.AI12 天前
共 1 篇相关资讯，按重要度与时间排序，每 3 小时更新。
论文提出有界在线步骤级修复模块：每步采样 K 个策略，失败时把 Lean 4 编译器错误信息喂给预训练修复模型就地修正，而非丢弃重采样。在 LeanDojo 1990 条定理子集上最多取得 32% 相对提升、多解出 82 条定理，收益主要来自浅层策略执行错误。该方法在 Lean Workbook …