arXiv cs.AI· Zihua She, Xiao Wang·· 14 小时前AI 评分55
KAPPA：用 Lean 4 与大模型智能体核查统计学论文证明
KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
AI 导读
KAPPA 是一套开源软件，它组织由 Claude Code 驱动的语言模型智能体，把 LaTeX 论文中的证明逐条翻译成 Lean 4 与 Mathlib 中的形式化证明并加以核验，每条编号结果会得到四种结论之一：无条件验证通过、带命名假设的条件验证通过、记录问题并标注位置与责任方，或未完成并说明原因。
正文 · AI 翻译
摘要：统计理论中的论文依赖于冗长的证明，很少有读者会逐行核查。我们提出 KAPPA（Kit of Agents for Proof-checking Papers with a proof Assistant），这是一款开源软件，它组织由 Claude Code 运行的语言模型智能体，将 LaTeX 论文中的证明逐条结果翻译为证明助手 Lean 4 及其库 Mathlib 中的形式，并在其中进行检验。每个编号结果会得到四种判定之一：无条件验证通过；有条件验证通过，其中每个被引用或未证明的输入都作为具名假设陈述；记录问题，并注明其在论文中的位置以及出错的一方；或未完成，并说明原因。该工具包逐步遵循论文自身的证明，而非寻找新的证明。写作与审查由不同的智能体负责，每个陈述在证明之前都与论文进行比对，证明之后则进行指纹标记，并且每一项判定都基于无需语言模型即可重新运行验证的证据。该工具包可无人值守运行数小时，等待使用限额结束，仅重新检查修订所改动的部分，并按角色、模型和结果报告其成本。我们描述了其设计，演示了一次完整运行，并将该工具包应用于四篇附有答案的示例论文以及三篇已发表的统计论文，这些论文均在其公开更正之前的版本上进行了盲检。在这三篇论文中，该工具包都在更正所指出的步骤上发现了已发表的错误，以及我们手工确认的更多问题。在直接给定相同论文的情况下，同一个使用 Lean 的语言模型在最长的那篇论文上正确分类的结果更少，并且将一些比论文陈述更窄的陈述报告为已证明；该工具包没有任何判定声称超出了其 Lean 证据所显示的范围。
| 评论： | 31 页，2 幅图。软件：此 https URL |
| 主题： | 计算 (stat.CO)；人工智能 (cs.AI)；计算机科学中的逻辑 (cs.LO) |
| 引用为： | arXiv:2610.35596 [stat.CO] |
| （或 arXiv:2610.35596v1 [stat.CO] 为此版本） | |
| https://doi.org/10.48550/arXiv.2610.35596 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Zihua She [查看电子邮件]
[v1]
2026 年 10 月 26 日星期一 15:22:15 UTC（45 KB）
来源：arXiv cs.AI · arxiv.org