arXiv cs.AI· Christian Clason, Tapio Helin, Medet Nursultanov, Lauri Oksanen·· 12 小时前AI 评分31
AutoIP：用 AI 智能体自动形式化线性正则化理论的 Lean 库
Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
AI 导读
研究者发布 Lean 库 AutoIP，由 AI 智能体将经典线性正则化理论及其依赖的泛函分析自动形式化。由于机器校验的证明只保证形式陈述本身成立，人工任务转为核对形式陈述是否符合原意，审阅者无需阅读证明。作者称风险主要在陈述而非证明，简单的陈述自动化测试甚至能暴露既有文献中的问题，并邀请逆问题社区扩展该库。
正文 · 原文
Abstract:Proof assistants such as Lean check mathematical proofs down to the axioms, and AI agents have recently made writing such proofs cheap. We describe AutoIP, a Lean library in which classical linear regularization theory, together with the functional analysis it rests on, has been autoformalized by AI agents. A machine-checked proof certifies only the formal statement it proves, so the remaining human task is to confirm that each formal statement says what was intended. We organize the library around this task: a reviewer compares the formal statements with their natural-language counterparts and never needs to read a proof. Our experience is that the risks lie in the statements rather than in the proofs, and that simple automated tests on the statements can expose problems even in the established literature. We illustrate this with a textbook theorem whose hypothesis is more restrictive than asserted. We invite the inverse problems community to extend and build on the library.
| Subjects: | Artificial Intelligence (cs.AI) |
| MSC classes: | 68V20, 47A52 |
| Cite as: | arXiv:2611.06962 [cs.AI] |
| (or arXiv:2611.06962v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.06962 arXiv-issued DOI via DataCite |
Submission history
From: Lauri Oksanen [view email]
[v1]
Wed, 4 Nov 2026 08:30:31 UTC (21 KB)
来源：arXiv cs.AI · arxiv.org