Google推出NL2AGBench基准，测试大模型将几何问题转为AlphaGeometry形式语言的能力，闭源模型表现远超开源模型。
研究人员推出NL2AGBench基准，评估大模型将英语几何问题转换为AlphaGeometry兼容形式表示的能力。该基准使用AlphaGeometry中的执行验证而非仅依赖文本相似性来评估翻译质量。实验显示闭源模型可执行翻译率超80%，而最大开源模型难以保持几何约束并产生有效形式化。研究团队引入错误分类法，研究少样本提示、微调和人工引导提示等缓解策略。
NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
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.