热点事件持续更新

KAPPA发布：LLM智能体用Lean 4核查统计学论文证明

1 篇报道1 个报道来源16 小时前更新

先了解这件事

AI 综述

研究者（Zihua She）发布开源工具KAPPA，用Claude Code驱动的语言模型智能体将LaTeX统计学论文中的证明逐条翻译为Lean 4（配合Mathlib库）并逐一核查，给出四种判定结论。该工具遵循论文原有证明步骤核查，而非寻找新证明；所有判定均基于可在不依赖语言模型的情况下重跑的Lean证据。对三篇已发表的统计论文进行盲测，KAPPA均在勘误所指步骤找出了已发表的错误，并发现了经研究者人工确认的其他问题。作为对照，同一模型直接面对论文时在最长一篇上的分类正确率更低。

AI 根据报道生成 · 3 小时前更新

最新进展10月26日 23:22

KAPPA：用 Lean 4 与语言模型智能体核查统计学论文中的证明

报道时间线

沿着报道，了解事件的不同侧面。

10月26日

23:22
arXiv · cs.AI
KAPPA：用 Lean 4 与语言模型智能体核查统计学论文中的证明
研究者推出开源工具 KAPPA，由 Claude Code 驱动的语言模型智能体将 LaTeX 统计学论文中的证明逐条翻译为 Lean 4（配合 Mathlib 库）并逐一核查，给出四种判定结论。对三篇已发表的统计论文进行盲测，该工具均在勘误所指步骤找出了已发表的错误，并发现了经人工确认的其他问题。作为对照，同一模型直接面对论文时在最长一篇上分类正确率更低，而 KAPPA 的所有判定均未超出其 Lean 证据范围。

本事件热度走势

可比范围当前: 6
可比范围峰值: 710月27日 13:00
近 24 小时变化: –

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。