摘要
近期的研究表明，编码代理能够在 Lean 4 中形式化整个高级数学教材，但现有工作主要集中在已经在 mathlib 中得到良好表示的数学分支，并且仅通过内核接受来衡量成功。我们通过将编码代理应用于形式化《常微分方程的数值方法》这一在 mathlib 中缺乏的数值分析教材，解决了这两个局限，强调了代理从零开始发展新理论的能力。
我们进一步引入了一种系统的、可重复的三维框架，用于评估代理生成的形式化质量，超越了简单的编译检查：语义正确性、Mathlib 重用以及通过 LLM-as-judge 方法的跨文件重用。将该框架应用于我们的形式化以及 RepoProver 和 M2F 的发布输出，我们发现了反复出现的不忠实形式化模式，包括不完整的多部分语句、添加的弱化假设以及参数限制，这些在内核接受中完全被掩盖。
我们的结果表明，基于编译的指标显著夸大了形式化的质量，并且我们提供了一种可重复的审计方法论，以支持对未来自动形式化系统进行更严格的评估。
博主点评： 这项研究不仅扩展了数学形式化的边界，还提出了评估形式化质量的新方法，强调了传统内核接受标准的不足，具有重要的实践意义和理论价值。它为自动形式化系统的未来发展奠定了坚实的基础。