知识卡片：NL2AGBench：评测LLM将自然语言几何题自动形式化为AlphaGeometry输入

英文标题：NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry

英文关键词：Auto-Formalization; AlphaGeometry; Benchmark; Large Language Models; Neuro-Symbolic Geometry; Execution-Based Verification; Domain-Specific Language

原始来源：arXiv:2608.28481v1 [cs.CL]；URL: https://arxiv.org/abs/2608.28481v1

一句话结论

NL2AGBench 是一个专门评测大语言模型（LLM）能否把英文几何题自动翻译成 AlphaGeometry 可执行形式语言（DSL）的基准，结果显示最强闭源模型的可执行翻译率超过 80%，而开源模型即使在最大规模下也较难稳定保持几何约束并生成合法形式化表示。

事件概述或研究问题

AlphaGeometry 这类神经符号几何系统在定理证明上已接近 IMO 金牌选手水平，但它的证明引擎要求输入用专门的领域特定语言（DSL）书写。目前，把自然语言几何题手动转换成这种形式语法是重要的使用瓶颈。论文提出 NL2AGBench，研究 LLM 能否自动完成这一“形式化”步骤。

方法/产品要点

基准任务：给定英文几何问题，要求 LLM 输出与 AlphaGeometry 兼容的形式化表示。
评估方式：不依赖文本相似度，而是用 AlphaGeometry 执行验证翻译质量，即检查输出是否能被执行并参与推理。
评测对象：10 个前沿开源和闭源 LLM，覆盖多个参数规模。
分析维度：可执行翻译准确率、句法正确性、错误特征。
错误分类：区分语法错误和逻辑错误。
缓解策略：尝试 few-shot prompting、微调、人工引导提示（human-guided hinting），并在多个模型族上观察到可测改进。

主要结果或产业意义

闭源与开源模型之间存在显著性能差距：领先闭源模型的可执行翻译率高于 80%，而最大开源模型仍难以一致地保持几何约束并生成合法形式化。
该基准指向一个实际工程方向：通过自动形式化降低 AlphaGeometry 类系统的使用门槛，使自然语言几何题可以直接进入形式证明流程。
对“LLM + 形式推理”的神经符号系统落地具有直接参考价值：瓶颈不仅在于证明搜索，也在于问题输入的形式化环节。

为什么重要

已有相关卡片主要关注 LLM 的自我改进、推理调度、KV 缓存压缩等方向，而本条聚焦“LLM 自动形式化”这一相对未被充分探索的能力，并且直接以 AlphaGeometry 作为评测载体。它补充了现有脉络中的增量信息：即使推理模型很强，自然语言到形式 DSL 的翻译仍是神经符号系统的可用性瓶颈；NL2AGBench 提供了可执行性验证的评测方法，而不仅仅是文本匹配。

局限与不确定性

摘要中未给出具体模型名称、参数量、数据集规模、评测题目数量，以及闭源模型超过 80% 的精确数值，均待核实。
错误分类中各错误类型的具体比例、缓解策略的量化改进幅度未在摘要中提供，待核实。
“执行验证”的具体流程、是否覆盖完整 AlphaGeometry 推理链、以及是否存在人工修正环节，需查看全文确认。
基准是否涵盖多种几何题型、难度分布、对 IMO 真题的覆盖程度，摘要未说明，待核实。

可用于图书/PPT/简报的角度

用一句话说明“自然语言到形式语言”是 AI 数学推理的新战场。
引用“闭源超 80%，开源仍吃力”作为模型能力差距的例证。
强调“执行验证比文本相似度更可靠”的评测理念，适用于讲解 LLM 评估方法。
以 AlphaGeometry 为案例，展示神经符号系统的实际瓶颈不完全在推理，而在“输入形式化”。

原始材料

标题：NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
arXiv ID：2608.28481v1
作者：Samuel Xiao, Judy Song, Rory Hu, Ziliang Zong
提交/更新：2026-08-28T16:07:16Z
分类：cs.CL, cs.AI
摘要：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.
URL：https://arxiv.org/abs/2608.28481v1