核心发现
方法论
本研究提出NL2AGBench基准，结合AlphaGeometry的执行验证机制，评估LLMs将自然语言几何题转化为DSL的能力。通过对10个模型（包括GPT-4、Gemini-3.1、Llama等）在不同参数规模下的表现，分析其语法正确性、逻辑一致性及错误类型，采用少样本提示、微调和人类引导等策略提升性能。模型输出通过在AlphaGeometry中执行验证，确保转化的可行性与正确性。
关键结果
- 闭源模型如GPT-4和Gemini-3.1在执行成功率上超过80%，而开源模型如Llama3.1仅达23%，差距明显。优化提示后，开源模型性能提升显著，Qwen3:235B从12.5%跃升至45.8%。错误分析显示，语法错误占主导，逻辑错误次之，模型在保持几何约束方面仍存在困难。
- 引入错误分类体系（语法、逻辑、值错误）帮助理解模型失败原因。微调和提示工程显著改善模型表现，特别是在复杂几何关系的保持与表达上。模型在不同几何概念（如圆、角平分线、垂线等）上的转化能力差异明显，反映模型对特定几何知识的掌握程度。
- 实验验证了执行验证机制的有效性，确保转化不仅在文本上相似，更在几何语义上正确。结果表明，当前闭源模型在自动化几何问题转化方面已达较高水平，但开源模型仍需突破语法和语义理解瓶颈。
研究意义
该研究填补了自然语言几何问题自动转化的评测空白，为神经符号几何推理系统的普及提供了标准化工具。通过结合执行验证机制，提升了自动形式化的可靠性，为未来自动推理、教育辅助和科学研究提供技术支撑。模型性能差异揭示了模型规模和训练数据对几何理解的影响，推动大模型在数学自动化中的应用发展。此工作也为自动化几何题解、符号推理和AI辅助数学教育提供理论基础与实践路径，具有重要学术和产业价值。
技术贡献
提出NL2AGBench基准，结合AlphaGeometry的执行验证机制，创新性地评估LLMs在几何自动形式化中的表现。系统分析模型在语法、逻辑和语义层面的错误类型，建立详细的错误分类体系。引入多策略（少样本提示、微调、人类引导）提升模型性能，验证了提示工程在符号推理中的有效性。实验结果明确展示了闭源模型的优势及开源模型的潜力，推动了大规模模型在数学自动化中的应用探索。
新颖性
首次系统性评估大模型将自然语言几何题转化为AlphaGeometry语法的能力，结合执行验证机制确保转化的实用性。提出详细的错误分类体系，为模型故障诊断提供工具。通过多策略优化模型表现，展示了提示工程在符号推理中的潜力。此工作在自动几何形式化领域具有开创性，填补了相关评测体系的空白。
局限性
- 模型在复杂几何关系和隐含空间信息的理解上仍存在不足，导致语义保持困难。
- 当前方法依赖大量提示和微调，计算成本较高，难以实现大规模自动化。
- 模型在保持几何约束和符号一致性方面表现不稳定，未来需增强几何知识的内在理解能力。
未来方向
未来将探索结合图像理解与文本生成的多模态模型，提升模型对几何图形的理解能力。加强模型在复杂几何关系中的推理能力，开发更高效的微调和提示策略，推动自动化几何题解的普及。同时，扩展基准到更广泛的数学领域，促进符号推理与自然语言处理的深度融合。
AI 总览摘要
近年来，随着大规模语言模型（LLMs）的快速发展，其在自然语言理解和数学推理方面展现出强大潜力。然而，将非正式的几何问题描述自动转化为符号化形式，仍是制约其应用的关键难题。AlphaGeometry作为一款高性能的神经符号几何推理系统，依赖于严格的领域特定语言（DSL）输入，手动转化繁琐且易出错，限制了其推广与应用。为解决这一瓶颈，本文提出NL2AGBench基准，结合AlphaGeometry的执行验证机制，系统评估模型自动转化能力。通过对十个代表性模型（包括GPT-4、Gemini-3.1、Llama等）在不同参数规模下的表现分析，发现闭源模型在成功率上显著优于开源模型，超过80%的成功率，而开源模型多在语法和几何约束保持方面表现不足。引入错误分类体系（语法、逻辑、值错误）帮助理解模型失败根源。实验还显示，少样本提示、微调和人类引导策略能有效提升模型性能，尤其是开源模型的表现提升显著。该研究不仅为自动几何形式化提供了标准化评测工具，也揭示了大模型在符号推理中的潜力与挑战，为未来智能几何推理系统的设计提供了重要参考。整体而言，本文推动了自然语言几何自动转化技术的边界，为AI在数学教育、科学研究及自动推理等领域的应用奠定了基础。
深度分析
研究背景
几何推理作为数学中的重要分支，近年来借助符号推理和神经网络的结合取得一定突破。代表性工作包括AlphaGeometry、HAGeo和TongGeometry等系统，它们在奥林匹克题目解答中表现出色，但普遍面临自然语言到符号表达的转化瓶颈。传统方法多依赖人工转写，效率低、易出错。近年来，LLMs如GPT系列、Llama和Mistral在自然语言理解方面表现优异，但在符号推理和自动形式化任务中仍存在挑战。现有基准如miniF2F、OlympiadBench主要评估推理能力，缺乏针对几何自动转化的专门评测体系。随着大模型规模的扩大，研究者开始关注其在数学符号化中的潜力，但缺乏系统性评估工具，限制了技术的深入发展。
核心问题
自动将自然语言几何题转化为AlphaGeometry的DSL，面临语义保持、符号正确性和几何约束的多重挑战。现有模型在语法正确性方面表现尚可，但在保持几何关系和空间信息方面仍有较大差距。手工转写虽准确但效率低，难以规模化应用。如何设计一种既能保证语义完整，又能自动生成符合DSL语法的转化方案，成为关键难题。这不仅关系到模型的理解能力，也涉及符号表达的准确性与推理的可靠性。
核心创新
本研究的创新点主要包括：1）提出NL2AGBench基准，结合AlphaGeometry的执行验证机制，系统评估模型自动转化能力；2）建立详细的错误分类体系，区分语法、逻辑和数值错误，为模型故障诊断提供工具；3）引入多策略（少样本提示、微调、人类引导）提升模型表现，验证提示工程在符号推理中的有效性。这些创新突破了现有仅关注推理能力的评测框架，强调符号表达的正确性和几何语义的保持，为自动形式化提供了新的技术路径。
方法详解
- �� 构建数据集：采集AlphaGeometry官方正式化的几何题，筛选出48个代表性题目，确保涵盖多样几何概念和难度。
- �� 设计提示模板：提供官方语法定义、规则和示范题，指导模型生成DSL表达。
- �� 模型输入：将自然语言题目与提示模板结合，要求模型输出题目编号和DSL表达，避免中间推理。
- �� 评估机制：在AlphaGeometry中执行生成的DSL，分类成功、语法错误和逻辑错误。
- �� 错误分析：建立错误分类体系，分析模型失败原因，优化提示策略。
- �� 提升策略：采用少样本提示、微调训练和人类引导，逐步提升模型性能。
实验设计
实验采用包括GPT-4、Gemini-3.1、Llama3.1等模型，覆盖不同参数规模。对比零样本和少样本提示效果，评估模型在语法正确性、几何关系保持和推理成功率上的表现。设置合理的超参数，控制推理时间，进行多轮实验验证。通过统计成功率、错误类型比例，分析模型在不同几何概念上的表现差异。还进行微调实验，验证提示工程的有效性。采用在AlphaGeometry中的执行验证作为核心指标，确保转化的实用性。
结果分析
闭源模型如GPT-4和Gemini-3.1在无提示情况下成功率超过80%，而开源模型如Llama3.1仅为23%。引入少样本提示后，开源模型表现显著提升，Qwen3:235B从12.5%跃升至45.8%。错误分析显示，语法错误占比最高，逻辑错误次之。微调和人类引导策略能有效降低错误率，尤其在复杂几何关系的保持上表现优异。模型在不同几何概念（如圆、角平分线、垂线）上的表现差异，反映其几何知识掌握水平。结果验证了执行验证机制的有效性，确保转化不仅文本相似，更符合几何语义。
应用场景
该方法可应用于自动化几何题解、数学教育辅助、符号推理系统开发等场景。通过自动转化自然语言题目，降低人工成本，提高解题效率。未来可结合图像理解，支持带图题目的自动转化，推动智能教育和科研工具的普及。长远来看，将促进AI在科学推理、自动证明和数学知识图谱构建中的应用，推动数学自动化的全面发展。
局限与展望
模型在复杂空间关系和隐含信息理解方面仍有限，导致语义保持困难。依赖大量提示和微调，计算成本较高，难以实现大规模部署。符号一致性和几何约束的保持仍不稳定，未来需增强模型的几何知识内在理解能力。
通俗解读 非专业人士也能看懂
想象你在厨房做菜，要按照食谱把食材放对位置、用对工具，才能做出美味的菜。自然语言问题就像食谱，描述了菜的样子，但要用专门的厨具（符号语言）表达出来，才能让机器人帮你做菜。现在的问题是，如何让AI理解你的食谱，把它变成机器能懂的指令。这个过程很复杂，因为食谱中有很多隐含的空间关系和细节，不能只看文字。研究人员设计了一个测试，让AI把自然的描述转成机器指令，然后用厨房的“机器人”验证这些指令是否正确。通过不断优化提示和训练，AI的转化能力逐步提升，就像教厨师更快学会用正确的工具做菜一样。这项工作帮助AI更好理解复杂的空间关系，未来可以让自动化厨房变得更智能，甚至帮忙设计新菜谱。
简单解释 像给14岁少年讲一样
想象你在学校参加科学比赛，题目用英语写得很复杂，描述了一个几何问题。你需要把这个英语题转成一种特殊的符号语言，才能让电脑帮你算。可是，这很难，因为英语里有很多隐含的空间关系和细节，不能随便写。科学家们想让电脑自己学会把英语题变成符号语言，就像教一个新手厨师用正确的刀和锅一样。于是，他们设计了一个测试，让电脑尝试转化，然后用专门的几何软件验证转化是否正确。研究发现，大公司做的电脑模型（比如GPT-4）能成功转化超过80%的题目，而开源模型（像Llama）成功率只有20%多一点。通过给模型更多例子和提示，效果会变得更好。这个研究很重要，因为它让电脑更聪明，能自己理解复杂的几何题，将来可以帮助学生学习、自动解题，甚至帮科学家验证几何猜想。
原文摘要
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.