NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
Computation and LanguageArtificial Intelligence
Summary
The authors studied how well large language models (LLMs) can turn everyday English geometry problems into a special language needed by a system called AlphaGeometry, which solves geometry theorems. They created a new test called NL2AGBench to check if the translations work correctly by running them in AlphaGeometry, instead of just comparing text. Their results show that closed-source LLMs do much better than open-source ones at making valid code. They also identified the main types of mistakes made and tried methods like giving examples, training more, and human hints to improve the models' translations.
Authors
Samuel Xiao, Judy Song, Rory Hu, Ziliang Zong
Abstract
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.