研究人员开发了 Lean Refactor，这是一个旨在优化 Lean 数学证明助手（Lean mathematical proof assistant）中大型语言模型（LLMs）生成的证明的新框架。该系统解决了证明长度、编译成本和版本兼容性等关键挑战，这些挑战之间常常存在权衡。通过使用具有精选重构策略数据库的检索增强型代理方法，Lean Refactor 实现了显著的压缩率并减少了编译时间，其性能优于以往的方法，并展示了改进的版本迁移能力。 AI
影响 引入了一种提高 LLM 生成的数学证明的效率和鲁棒性的新方法，有可能加速形式化验证的努力。
排序理由 发表了一篇学术论文，详细介绍了优化 LLM 生成证明的新框架。
在 Hugging Face Daily Papers 阅读 →
AI 生成摘要 · Google Gemini · 来自 2 个来源。 我们如何撰写摘要 →
arXiv:2605.20244v1 Announce Type: cross Abstract: We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle…
Lean Refactor presents a retrieval-augmented agentic framework that improves Lean proof refactoring by addressing multi-objective optimization, version compatibility, and scalability challenges through curated strategy databases and version-filtered retrieval.