arXiv cs.AI· Christian Clason, Tapio Helin, Medet Nursultanov, Lauri Oksanen·· 11 小时前AI 评分31
AutoIP：用 AI 智能体自动形式化线性正则化理论的 Lean 库
Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
AI 导读
研究者发布 Lean 库 AutoIP，由 AI 智能体将经典线性正则化理论及其依赖的泛函分析自动形式化。由于机器校验的证明只保证形式陈述本身成立，人工任务转为核对形式陈述是否符合原意，审阅者无需阅读证明。作者称风险主要在陈述而非证明，简单的陈述自动化测试甚至能暴露既有文献中的问题，并邀请逆问题社区扩展该库。
正文 · AI 翻译
摘要：Lean 等证明助手可将数学证明一直检验到公理层面，而 AI 智能体最近已使撰写此类证明变得成本低廉。我们介绍 AutoIP，这是一个 Lean 库，其中经典线性正则化理论及其所依赖的泛函分析已由 AI 智能体自动形式化。机器检验的证明只能保证它所证明的形式陈述成立，因此剩下的人工任务是确认每个形式陈述所表达的内容符合原意。我们围绕这一任务来组织该库：审阅者只需将形式陈述与其自然语言对应表述进行比较，无需阅读证明。我们的经验是，风险在于陈述而非证明，而且对陈述进行简单的自动化测试甚至能揭示已有文献中的问题。我们用一个教科书定理来说明这一点，该定理的假设比其所声称的更为严格。我们邀请反问题领域的研究者扩展并基于该库继续构建。
| 主题： | 人工智能（cs.AI） |
| MSC 分类号： | 68V20, 47A52 |
| 引用为： | arXiv:2611.06962 [cs.AI] |
| （或 arXiv:2611.06962v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.06962 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Lauri Oksanen [查看邮箱]
[v1]
2026年11月4日星期三 08:30:31 UTC（21 KB）
来源：arXiv cs.AI · arxiv.org