在 AI 时代形式化逆问题：可能性、陷阱与邀请

arXiv:2611.06962 (cs)

[Submitted on 4 Nov 2026]

作者：Christian Clason、Tapio Helin、Medet Nursultanov、Lauri Oksanen

查看 PDF | HTML（实验性）

摘要#

证明助手（proof assistants）如 Lean 会把数学证明一直检验到公理，而 AI 智能体最近让撰写这类证明变得成本低廉。我们描述 AutoIP——一个 Lean 库，经典线性正则化理论（linear regularization theory）以及它所依赖的泛函分析（functional analysis）已由 AI 智能体在其中完成自动形式化（autoformalized）。机器检验的证明只证明它所证明的形式陈述，因此剩下的人类任务是确认每个形式陈述表达的正是原本意图。我们围绕这项任务来组织该库：评审者将形式陈述与其自然语言对应物进行比较，永远不需要阅读证明。我们的经验是，风险在于陈述而非证明，而对陈述进行简单的自动化测试甚至能暴露既有文献中的问题。我们用一个教科书定理来说明这一点，该定理的假设比所声称的更具限制性。我们邀请逆问题（inverse problems）社区扩展并基于该库继续构建。

主题：人工智能（cs.AI）

MSC 分类：68V20, 47A52

引用：arXiv:2611.06962 [cs.AI]（或 arXiv:2611.06962v1 [cs.AI] 引自本版本）

https://doi.org/10.48550/arXiv.2611.06962

提交历史#

来自：Lauri Oksanen [查看电子邮件]

• [v1] Wed, 4 Nov 2026 08:30:31 UTC (21 KB)