NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
作者: Samuel Xiao, Judy Song, Rory Hu, Ziliang Zong
分类: cs.CL, cs.AI
发布日期: 2026-08-28
💡 一句话要点
提出NL2AGBench以解决自然语言几何问题的形式化转换难题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 自然语言处理 几何问题 形式化表示 错误分析 执行验证 神经符号系统
📋 核心要点
- 现有大型语言模型在将自然语言几何问题转换为正式表示时存在显著性能差距，尤其在保持几何约束方面表现不佳。
- 论文提出NL2AGBench基准，通过执行验证评估LLMs的翻译质量，旨在提高自然语言到AlphaGeometry的转换效率。
- 实验显示，闭源模型的可执行翻译率超过80%，而开源模型在准确性和有效性上存在明显不足，提出的改进策略有效提升了模型性能。
📝 摘要（中文）
近年来，大型语言模型（LLMs）在自然语言理解和数学推理方面展现了强大的能力。然而，它们将非正式数学问题转换为正式表示的能力仍未得到充分探索。特别是在神经符号几何系统如AlphaGeometry中，其定理证明引擎需要特定领域语言（DSL）的输入。为了解决这一挑战，本文提出了自然语言到AlphaGeometry基准（NL2AGBench），用于评估LLMs将英语几何问题翻译为AlphaGeometry兼容的正式表示。NL2AGBench通过在AlphaGeometry中进行执行验证来评估翻译质量，而不仅仅依赖文本相似性。我们评估了十种最先进的开源和闭源LLMs，并分析了可执行翻译的准确性、语法正确性和错误特征。实验结果显示，闭源模型的可执行翻译率超过80%，而最大的开源模型在保持几何约束和生成有效形式化方面存在困难。
🔬 方法详解
问题定义：本文解决的是大型语言模型在将自然语言几何问题转换为AlphaGeometry所需的正式表示时的性能不足，尤其是在保持几何约束方面的挑战。现有方法主要依赖文本相似性，未能有效评估翻译质量。
核心思路：论文的核心思路是引入NL2AGBench基准，通过执行验证的方式来评估LLMs的翻译质量，确保生成的形式化表示能够在AlphaGeometry中有效执行。
技术框架：整体架构包括数据集构建、模型评估和错误分析三个主要模块。数据集由多种几何问题组成，模型评估通过执行验证进行，错误分析则帮助识别和分类翻译中的错误类型。
关键创新：最重要的技术创新点在于使用执行验证而非文本相似性来评估翻译质量，这一方法能够更准确地反映模型在实际应用中的表现。
关键设计：在模型评估中，采用了错误分类法区分语法错误和逻辑错误，并探索了少量示例提示、微调和人类引导提示等策略，以提高模型的翻译准确性。实验结果表明，这些策略在多个模型家族中均取得了可测量的改进。
🖼️ 关键图片
📊 实验亮点
实验结果显示，领先的闭源模型在可执行翻译率上超过80%，而最大的开源模型在保持几何约束和生成有效形式化表示方面存在显著不足。通过引入错误分类和改进策略，模型性能得到了显著提升，展示了NL2AGBench的有效性。
🎯 应用场景
该研究的潜在应用领域包括教育、自动化定理证明和智能辅导系统。通过提高自然语言到形式化表示的转换效率，能够帮助学生更好地理解几何问题，同时为自动化定理证明系统提供更强的支持，推动相关领域的发展。
📄 摘要（原文）
Recent advances in large language models (LLMs) have demonstrated strong capabilities in natural language understanding and mathematical reasoning. However, their ability to translate informal mathematical problems into formal representations remains underexplored. This limitation is particularly important for neuro-symbolic geometry systems such as AlphaGeometry, whose theorem-proving engine requires inputs in a specialized domain-specific language (DSL). Although AlphaGeometry achieves near-IMO gold-medalist performance, manually converting natural-language problems into its formal syntax remains a significant usability bottleneck. To address this challenge, we introduce the Natural Language to AlphaGeometry Benchmark (NL2AGBench), which evaluates LLMs in translating English geometry problems into AlphaGeometry-compatible formal representations. NL2AGBench uses execution-based verification within AlphaGeometry to assess translation quality rather than relying solely on textual similarity. We evaluate ten state-of-the-art open- and closed-source LLMs across multiple parameter scales and analyze executable translation accuracy, syntactic correctness, and error characteristics. Our experiments reveal a substantial performance gap between closed- and open-source models: leading closed-source models achieve executable translation rates above 80%, while even the largest open-source models struggle to consistently preserve geometric constraints and produce valid formalizations. We introduce an error taxonomy distinguishing syntax and logic errors and investigate mitigation strategies, including few-shot prompting, fine-tuning, and human-guided hinting, which yield measurable improvements across multiple model families.