研究数学定理的同义改写如何导致自动形式化失败
Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization
- 用确定性改写规则测试不同数学题集的鲁棒性
- 发现代码生成层是主要故障来源，且问题类型随数据集变化
- 为自动形式化提供故障分类，适合改进模型训练
近年来，Lean 4 自动形式化受到广泛关注，前沿语言模型与开源权重的自动形式化工具已能生成有效数学定理的形式化表达。然而，现有评估多依赖单一标准表述，很少检验输出对输入自然变化的鲁棒性；先前研究显示，语义等价的改写常导致不同的形式化结果。本文通过应用确定性改写规则，对本科生及奥数级别数学题集进行测试。在四个前沿模型和三个开源权重自动形式化器上，我们发现改写敏感性主要源于代码生成层的失败，且失败模式因数据集而异。这些模式在开源模型中也存在，表明当前最先进的自动形式化器仍难以生成有效的 Lean 代码。研究结果为自动形式化提供了故障模式分类，并支持针对特定编译失败进行训练干预。
原文摘要 · Abstract (English)
Lean 4 autoformalization has become increasingly popular in recent years, with frontier language models and open-weight autoformalizers now producing valid formalizations of mathematical theorems. However, these evaluations often rely on single canonical phrasings of theorems and rarely probe whether outputs are robust to natural variation in inputs, while prior work has shown that semantically equivalent paraphrases often induce divergent formal outputs. We study the structure of these divergences in Lean 4 by applying deterministic paraphrase rules to datasets of undergraduate and Olympiad-level math problems. Across four frontier models and three open-weight autoformalizers, we find that paraphrase sensitivity is dominated by failures at the code-generation layer, and that these failures are typed differently by dataset. Furthermore, these patterns generalize to open-weight models, showing that state-of-the-art autoformalizers still struggle to generate valid Lean code. Our results provide a failure-mode taxonomy for autoformalization and motivate training-time interventions targeted at specific compilation failures.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。