核心发现
方法论
采用结合Lean编译验证、跨模型语义判定（GPT-5.2与Gemini-2.5-Pro）和专家校准的多层次评价体系。通过400题数学声明的构建，结合人类专家审核，建立高保真度的信实性指标。利用工具增强的自动化流程，包括专家起草、Mathlib搜索和Lean细化反馈，采用三因素（起草、搜索、反馈）23阶因子设计，分析不同干预对编译率和语义忠实度的影响。
关键结果
- 完整系统实现中，编译率达89.5%，但信实性达60.5%，显示30%编译通过但语义不符的差距。人类审核确认，96%正向输出为信实，82.4%的负向输出为语义失败。现有模型在信实性指标上仍表现较低，强调单一指标不足，需区分有效性与忠实性。
- 工具干预中，Elaboration Feedback显著提升有效性，但伴随语义偏差扩大；搜索主要改善基础性和选择性；专家起草在有反馈和搜索支持下表现出较强替代性。因子分析揭示不同工具对验证边界的不同贡献。
- 多模型对比显示，单一模型在信实性上远低于全工具系统，Full agent达60.5%，而纯模型仅19-28%。编译率高不等于语义忠实，强调验证机制的重要性。
研究意义
本研究首次系统性结合Lean编译验证、跨模型语义判定和专家校准，提出信实性评估新范式，突破传统编译成功率的局限。揭示自动形式化中存在的30%“编译通过但语义偏差”问题，为未来自动化数学证明和教育应用提供理论基础。该方法提升了对模型生成内容的信任度，为AI在数学领域的可信应用奠定基础，推动形式化工具的实用化和普及。
技术贡献
提出结合Lean编译验证与多模型语义判定的信实性指标，创新性地采用23阶因子设计分析工具干预效果。构建高质量400题数学声明数据集，结合人类专家校准，建立可靠的评估体系。系统性分析不同模型和工具在验证边界的表现差异，为未来模型设计提供指导。实现了多模型、多工具协同的自动化流程，显著提升形式化的信实性和效率。
新颖性
首次将Lean编译验证与跨模型语义判定结合，提出信实性指标作为自动形式化的核心评价标准。区别于传统仅关注编译成功率的方法，本研究强调语义忠实性，揭示了30%的潜在偏差，填补了自动数学形式化评估中的空白。采用因子设计系统分析工具干预效果，为自动化流程优化提供新思路。
局限性
- 当前评估依赖GPT-5.2和Gemini模型的语义判定，存在模型偏差和判定不一致问题，未来需引入更多人类校准和多模态验证。
- 数据集虽覆盖多个数学领域，但规模有限，尚未涵盖所有数学声明类型，泛化能力有待验证。
- 工具干预效果存在交互复杂性，部分干预可能引入语义偏差，需进一步优化工具设计和集成策略。
未来方向
未来将扩展数据集规模，涵盖更复杂和多样的数学声明，提升模型泛化能力。探索多模态语义判定机制，结合符号和图像信息增强判定准确性。优化工具集成策略，减少偏差，提升整体信实性。推动自动形式化在数学教育和科研中的实际应用，促进可信AI的发展。
AI 总览摘要
本研究针对自然语言数学声明的自动形式化问题，提出一种结合Lean编译验证与跨模型语义判定的信实性评估框架。传统的自动化数学验证多依赖于证明成功率，但忽视了声明本身的语义忠实性。本文构建了包含400个研究生水平数学声明的高质量数据集，涵盖实分析、复分析、拓扑和代数领域。通过结合Lean编译验证、GPT-5.2与Gemini-2.5-Pro模型的语义判定，以及专家校准，建立了高保真度的信实性指标。实验证明，虽然完整系统的编译率达89.5%，但信实性仅为60.5%，揭示了30%的声明存在“编译通过但语义偏差”的问题。人类专家审核确认，正向输出的信实率高达96%，负向输出的语义失败率为82.4%。这一发现表明，单纯依赖编译成功不能充分保证声明的数学意义。为分析工具干预效果，采用23阶因子设计，结果显示，Elaboration Feedback在提升有效性方面最为显著，但也带来语义偏差的风险。搜索工具主要改善基础性和选择性，而专家起草在有反馈和搜索支持下表现出较强的替代性。多模型对比显示，单一模型在信实性上表现远低于全工具系统。研究强调，未来应在模型设计中兼顾有效性与信实性，扩展数据集，优化工具集成，推动自动形式化在数学教育和科研中的应用。该方法为自动化数学证明提供了新的评价视角，有助于实现可信、可解释的AI数学助手。
深度分析
研究背景
数学自动形式化经历了从符号推理到深度学习的演变，早期以逻辑推理为核心，代表作包括HOL Light和Coq。近年来，深度学习模型如GPT系列在自然语言理解方面取得突破，但在数学声明自动转化中仍面临语义偏差和验证难题。现有研究多关注证明生成（如DeepSeek-Prover、Kimina-Prover），但对声明本身的信实性缺乏系统评估。部分工作引入编译验证和语义一致性指标（如BEq），但缺乏大规模、标注丰富的基准数据集。随着模型能力提升，自动形式化在数学教育、科研辅助和自动证明等场景中展现潜力，但信实性保障仍是关键瓶颈。
核心问题
自动将自然语言数学声明转化为形式化代码，面临两个核心难题：一是声明的语义忠实性难以保证，二是编译成功并不代表语义正确。现有系统多依赖编译验证，忽视声明的数学含义，导致“编译通过但语义偏差”的问题普遍存在。如何在保证代码可编译的基础上，准确反映原始数学意图，成为自动形式化的关键挑战。该问题关系到模型的可信度和实用性，尤其在高阶数学和复杂定义中更为突出。
核心创新
本研究的创新点在于：1）提出结合Lean编译验证与跨模型语义判定的信实性指标，作为自动形式化的核心评价标准，突破传统只关注编译成功的局限；2）构建400题高质量数学声明数据集，涵盖多个数学领域，结合专家校准，确保评价的可靠性；3）采用23阶因子设计，系统分析不同工具（起草、搜索、反馈）对验证边界的影响，为工具优化提供理论依据。此方法实现了多层次、多工具协同的自动化流程，显著提升声明的信实性和效率。
方法详解
- �� 数据集构建：从公开教材和讲义中采集400个研究生水平声明，确保自然语言描述无对应正式代码。• 评价体系：结合Lean编译验证和GPT-5.2、Gemini-2.5-Pro模型的语义判定，建立高保真信实性指标。• 工具集成：引入专家起草（T）、Mathlib搜索（S）和Lean细化反馈（F），组成三因素23阶因子设计。• 流程控制：利用中央调度器（GPT-5.2）协调工具调用，动态调整声明生成路径。• 评估指标：编译率、信实性（两模型判定一致≥9分）和专家确认，确保多维评价。• 实验设计：逐个题目在所有工具配置下测试，分析工具干预效果，识别验证瓶颈。
实验设计
采用涵盖实分析、复分析、拓扑和代数的400题数据集，比较多模型（GPT-5.2、Gemini-2.5-Pro）和工具配置（起草、搜索、反馈）的性能。指标包括编译成功率、信实性（模型判定≥9分）和专家确认率。通过因子设计分析工具干预对验证和信实性的影响，进行AB测试和交互分析。实验还包括不同数学领域的子集分析，验证模型在复杂声明中的表现差异。采用严格的交叉验证和专家校准，确保评估的可靠性。
结果分析
全系统达成89.5%的编译率，但信实性仅为60.5%，显示30%的声明虽能编译但语义偏差严重。专家审核确认，正向输出中96%为信实，负向输出中82.4%为语义失败。工具干预中，Elaboration Feedback显著提升有效性（信实性提升约30%），但伴随偏差扩大。搜索工具改善基础性和选择性，起草在有反馈支持下表现优异。多模型对比显示，单模型信实性远低于全工具系统，强调多工具协同的重要性。
通俗解读 非专业人士也能看懂
想象你在厨房做饭。自然语言描述就像是你说“我想做一道意大利面”，而自动形式化就像是厨房的厨师把你的话变成具体的食谱。传统方法只看厨师是否能做出菜（编译成功），但这并不代表菜的味道和你想的一样。真正的挑战是，厨师做出来的菜要和你说的“意大利面”味道一致。我们用一种特殊的“味道检测器”来判断菜是否符合你的描述，还请了专家品尝确认。通过不断调整厨师的做法和用料，确保菜既能做出来，又符合你的期待。这就像让AI不仅能“做出菜”，还要“做出你想要的味道”。
简单解释 像给14岁少年讲一样
想象你在学校的厨房里，想让机器人帮你做一道你描述的菜。你告诉它：“我想要一份意大利面。”机器人会试着把你的话变成具体的食谱，但有时候它虽然能写出食谱（编译成功），但味道可能和你想的不一样（语义不符）。这就像是机器人能做出菜，但味道偏差。我们用一种特别的“味道检测器”来判断菜是不是你想要的味道，还请专家帮忙确认。通过不断调整机器人的做法，确保它既能做出菜，又符合你的期待。这就像让AI不仅会“做菜”，还会“做你想要的味道”。
原文摘要
Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400-entry graduate-level benchmark spanning real analysis, complex analysis, topology, and algebra, our protocol combines Lean compilation, cross-model semantic judging, and human expert calibration. The resulting picture is different from compile-rate evaluation: a full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap. Targeted human audits support the metric as a conservative decision boundary: across available case-level audits, 96.0% of consensus-positive outputs are human-confirmed faithful, while 82.4% of compile-pass consensus-negative outputs are human-confirmed semantic failures. Under this metric, existing one-shot formalizer models and prover-oriented Lean models remain low, suggesting that formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately. We then use a full $2^3$ factorial design to decompose three recurring interventions in formalization pipelines: parametric expert drafting, Mathlib/context search, and Lean elaboration feedback. Elaboration feedback is the largest validity intervention, but it also exposes a larger compile-pass semantic-failure bucket; search mainly improves grounding and selectivity; and fine-tuned drafting is largely substitutable in this tool stack once feedback and grounding are available.