用智能体形式化常微分方程数值方法，发现编译通过不等于正确。
Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
- 用智能体从零构建数值分析新理论，填补mathlib空白。
- 发现三类未忠实形式化模式，编译通过也掩盖问题。
- 提出三维评估框架，适合研究自动形式化质量的学者。
近期工作表明编码智能体可在Lean 4中形式化完整高等数学教材，但现有研究集中于mathlib已覆盖的领域，且仅以内核接受作为衡量标准。本文将编码智能体应用于《常微分方程数值方法》这一mathlib中几乎缺失的数值分析教材，强调其从零构建新理论的能力。我们进一步提出一个系统化、可复现的三维评估框架，用于检验超越编译通过的形式化质量：语义正确性、mathlib复用度、跨文件复用率，采用大模型作为评判者。对自研成果及RepoProver、M2F发布的输出进行评估，发现普遍存在不忠实形式化现象，包括多部分命题不完整、额外添加弱化假设、参数限制等，这些均被内核接受所掩盖。结果表明，仅依赖编译指标会严重夸大形式化质量，我们提供了可复现的审计方法，以支持未来自动形式化系统的更严谨评估。
原文摘要 · Abstract (English)
Recent work has demonstrated that coding agents can formalize entire advanced mathematics textbooks in Lean 4, yet existing efforts concentrate on branches of mathematics already well-represented in mathlib and measure success solely through kernel acceptance. We address both limitations by applying a coding agent to formalize Numerical Methods for Ordinary Differential Equations, a textbook in numerical analysis that is largely absent from mathlib, stressing the agent's capacity to develop new theory from scratch. We further introduce a systematic, reproducible three-dimensional framework for evaluating the quality of agent-produced formalizations beyond compilation: semantic correctness, Mathlib reuse, and cross-file reuse via LLM-as-judge methods. Applying this framework to our own formalization and to the released outputs of RepoProver and M2F, we uncover recurring unfaithful formalization patterns, including incomplete multi-part statements, added weakening hypotheses, and parameter restrictions, that kernel acceptance entirely obscures. Our results suggest that compilation-based metrics substantially overstate formalization quality, and we provide a reproducible audit methodology to support more rigorous evaluation of future autoformalization systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。