形式化数值分析：超越内核的智能体管线与质量审计

最近的工作表明，编码代理可以在 Lean 4 中形式化整个高级数学教科书，但现有的工作集中在 mathlib 中已经得到很好体现的数学分支上，并且仅通过内核接受程度来衡量成功。我们通过应用编码代理来形式化《常微分方程数值方法》（Mathlib 中基本上没有的数值分析教科书）来解决这两个限制，强调代理从头开始开发新理论的能力。我们进一步引入了一个系统的、可重复的三维框架，用于评估代理生成的形式化超出编译的质量：语义正确性、Mathlib 重用以及通过 LLM-as-judge 方法的跨文件重用。将此框架应用于我们自己的形式化以及 RepoProver 和 M2F 的发布输出，我们发现了反复出现的不忠实的形式化模式，包括不完整的多部分语句、添加的弱化假设和参数限制，而内核接受完全掩盖了这些模式。我们的结果表明，基于编译的指标大大夸大了形式化质量，并且我们提供了可重复的审计方法来支持对未来自动形式化系统进行更严格的评估。