PaperlayerView exact revision on arXiv

Source-linked AI summary

NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry

Samuel Xiao, Judy Song, Rory Hu, Ziliang Zong

arXiv:2608.28481v1cs.CLcs.AI

TL;DR

Natural-language geometry must be translated into precise AlphaGeometry DSL before symbolic proving can begin, yet this auto-formalization task remains difficult and underexplored. NL2AGBench benchmarks executable translations, diagnoses syntax and logic failures, and evaluates prompting, fine-tuning, and human-guided hints, revealing a large closed–open source gap and measurable mitigation gains.

  • Problem

    Translating informal geometry into AlphaGeometry’s precise DSL remains difficult, although this conversion is required before symbolic theorem proving can begin.

  • Method

    NL2AGBench evaluates LLM translations of English geometry problems through direct AlphaGeometry execution and categorizes resulting failures into syntax and logic errors.

  • Results

    Closed-source models substantially outperform open-source alternatives, while targeted prompting and guidance improve translation pass rates across multiple model families.

  • Takeaways & Limitations

    The benchmark indicates that effective geometry auto-formalization requires both target-language syntax mastery and accurate geometric interpretation with constraint preservation.

  • Takeaways & Limitations

    Human-guided hints improve translation quality particularly when initial outputs are close to correct, limiting their demonstrated role to recoverable formalization errors.

Abstract

from arXiv · show

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.

I. INTRODUCTION

Auto-formalization translates informal geometry into precise symbolic inputs required by theorem-proving systems, but geometry-specific constraints make this difficult. NL2AGBench addresses this bottleneck by evaluating executable AlphaGeometry translations and studying model gaps, errors, and improvements.

  • Motivation: Auto-formalization is challenging because formal solvers require precise symbolic inputs rather than natural-language descriptions.The process is a prerequisite for theorem-proving and neuro-symbolic reasoning systems.
  • Motivation: Geometry problems require preserving implicit spatial relationships, diagram-dependent information, and complex constraints exactly during translation.Even small errors can alter the problem’s meaning and prevent valid downstream proofs.
  • Motivation: AlphaGeometry’s specialized DSL makes manual translation from mathematical English a barrier to accessibility, scalability, and deployment.The DSL must explicitly encode geometric objects, constraints, and incidence information before theorem proving can begin.
  • Benchmark and evaluation: NL2AGBench evaluates English-to-AlphaGeometry DSL translation through direct execution, measuring syntax and preservation of geometric semantics.The benchmark pairs geometry problems with verified formal representations and runs generated specifications inside AlphaGeometry.
  • Evaluation findings: 10 LLMs spanning open- and closed-source models reveal a substantial performance gap: the largest open-source model scores under 46%, while frontier closed-source models reach 85% and above.The evaluation covers multiple parameter scales.
  • Mitigation and diagnosis: Targeted prompting, fine-tuning, and human-guided hinting improve pass rates for Llama3.1:70b by 23%, GPT-4omini:8b by 8%, and Qwen3:235b by 33.3%.The paper also introduces a taxonomy separating syntax and logic errors in AlphaGeometry translations.

II. RELATED WORK

Prior work advanced formal theorem proving, mathematical reasoning, and LLM-assisted auto-formalization, but did not specifically benchmark translation of English geometry problems into AlphaGeometry syntax.

  • AlphaGeometry and related systems: AlphaGeometry combines symbolic deduction with neural auxiliary-construction generation for Euclidean geometry proofs, while related systems improve search or construction strategies.These systems still depend on formal or semi-formal problem representations.
  • Auto-formalization and theorem proving: Earlier studies explored translating informal mathematics into proof-assistant languages and using LLMs or proof sketches to support formal theorem proving.Examples include Lean, Isabelle, Metamath, and related formal-reasoning environments.
  • Benchmark gap: Existing benchmarks evaluated mathematical reasoning or language translation, but not mathematical translation into solver-compatible formal representations.MATH, GSM8K, OlympiadBench, and formal reasoning benchmarks measure adjacent capabilities rather than this specific translation task.

III. NL2AGBENCH

NL2AGBench is built from verified AlphaGeometry formalizations and selects a compact, diverse, execution-efficient subset of geometry problems for scalable evaluation.

  • Dataset construction: NL2AGBench begins with 231 geometry problems manually formalized in AlphaGeometry from the JGEX repository.These paired English and DSL instances support direct evaluation of automatic translation.
  • Benchmark selection: The selected problems cover circles, cyclic quadrilaterals, angle bisectors, orthocenters, circumcenters, midpoints, reflections, and perpendicular constructions.This provides varied geometric concepts and syntactic complexity.
  • Benchmark selection: Problems requiring excessive AlphaGeometry runtime or computational resources are excluded to maintain scalable evaluation costs.The resulting benchmark spans varying syntactic complexity and geometric reasoning difficulty.
  • Examples: Sample problems translate natural-language constructions into compact DSL clauses encoding objects, incidences, and target relations.Examples include midpoint, circle, line, perpendicular, cyclicity, and angle-equality statements.

3) Evaluation Objective:

The evaluation objective is to generate an AlphaGeometry DSL formalization from an English geometry problem that is both syntactically valid and semantically faithful, using a constrained two-line output.

  • Objective: Given an English geometry problem PNL, the LLM must generate a corresponding AlphaGeometry formalization PAG.The task frames auto-formalization as a direct mapping from natural language to solver input.
  • Correctness criteria: Syntactic correctness requires the generated DSL to conform to AlphaGeometry grammar.This is one of the two explicit success requirements.
  • Correctness criteria: Semantic correctness requires preserving all geometric objects, constraints, and target conclusions from the original problem.A translation succeeds only if AlphaGeometry executes it without error and produces a valid problem specification.
  • Prompting setup: The prompting framework supplies official syntax definitions, handwritten clause and formatting rules, and the target geometry problem.These materials provide models with knowledge of the required DSL.
  • Prompting setup: Models must output only one two-line translation containing the problem identifier and DSL representation.The format excludes explanations, commentary, alternatives, and intermediate reasoning.

C. Translation Verification

NL2AGBench verifies generated AlphaGeometry translations by executing them and classifying outcomes as successful, syntactic, or logical failures. This execution-based framework measures whether translations preserve the semantics required by symbolic theorem proving and supports interpretable failure analysis.

  • C. Translation Verification: Execution-based evaluation runs each generated DSL specification in AlphaGeometry rather than relying on string similarity.This accommodates syntactically different formalizations that may be semantically equivalent.
  • C. Translation Verification: Successful translations are accepted and execute successfully, while syntax errors violate DSL grammar or construction rules.These categories distinguish valid execution from failures in formal-language structure.
  • C. Translation Verification: Logic errors are syntactically valid specifications that are semantically inconsistent with the intended geometry problem.They indicate that the generated formalization does not preserve the problem’s intended meaning.
  • C. Translation Verification: The framework measures whether generated translations function as an interface between natural-language geometry problems and AlphaGeometry’s symbolic reasoning engine.Execution therefore tests downstream usability, not merely textual or grammatical similarity.
  • C. Translation Verification: The error taxonomy maps low-level AlphaGeometry runtime failures to interpretable categories for analyzing model behavior.It addresses the limited information often provided by raw execution exceptions.
  • C. Translation Verification: Syntax errors prevent the symbolic engine from parsing or constructing the geometric configuration.The passage identifies invalid argument counts as one syntax-error case, often reflecting partial understanding but incomplete DSL knowledge.

1) Assertion Error:

The Assertion and Key error cases describe structurally invalid AlphaGeometry translations, often caused by missing arguments, malformed clauses, special-character misuse, or incorrect point repetition. These failures can reflect partial geometric understanding but violate the DSL’s construction and parsing requirements.

  • 1) Assertion Error:: AssertionErrors occur when a construction receives an invalid number of arguments.Examples include incomplete reflection, malformed circle constructions, and incorrectly specified auxiliary points.
  • 1) Assertion Error:: The example reflect c b fails because reflection requires three points, but only two are provided.The missing point prevents the line of reflection from being defined.
  • 1) Assertion Error:: KeyErrors can result from improperly used clauses, delimiters, construction arguments, or special characters such as semicolons and proof operators.The taxonomy includes misuse of semicolons, whitespace, and proof operators among these causes.
  • 1) Assertion Error:: AlphaGeometry permits repeated output points, but incorrect repetition or point placement can trigger a KeyError.A circumcenter clause normally takes three defining points; the valid repeated form includes the output point on the right.
  • 1) Assertion Error:: Misplaced clauses, malformed declarations, and invalid output-variable references are additional structural sources of KeyError and ValueError failures.These cases show that syntactically plausible translations can still violate DSL organization rules.
  • 1) Assertion Error:: An extra eqangle in a proof clause causes a KeyError, illustrating how hallucinated DSL clauses invalidate otherwise structured translations.The example adds an unsupported predicate to the proof statement.

3) Value Error:

ValueErrors arise when AlphaGeometry translations define geometric objects inconsistently or use invalid construction and proof parameters. The examples center on self-reference, circular definitions, and incorrect argument counts that violate underlying construction rules.

  • 3) Value Error:: ValueErrors include circular point definitions, self-referential constructions, invalid proof predicates, and incorrect parameter counts.These categories capture semantically or structurally invalid uses of otherwise recognizable DSL constructs.
  • 3) Value Error:: A point cannot be used to determine its own position before it has been constrained.The example defining d with on_circum clauses uses d recursively and therefore triggers a ValueError.
  • 3) Value Error:: ValueErrors indicate syntactically plausible structures that violate underlying geometric construction rules.The failure therefore concerns construction validity rather than only surface formatting.
  • 3) Value Error:: An eqangle clause accepts 8 arguments, so passing 12 arguments produces a ValueError.The example’s proof predicate has four extra arguments beyond the required two four-point angles.
  • 3) Value Error:: The on_tline construction requires three argument points to establish a point of tangency between a circle and a line.The cited example violates this construction requirement while defining c.

B. Logic Errors

Logic errors are syntactically valid translations whose geometric meaning is incorrect, exposing failures in relations, target predicates, or terminology interpretation. The taxonomy treats these errors as evidence about mathematical understanding and uses execution behavior to classify prolonged failures.

  • B. Logic Errors: Logic errors occur when a syntactically valid translation is semantically incorrect.Typical causes include incorrect geometric relations, incorrect target predicates, and misinterpreted terminology.
  • B. Logic Errors: Logic errors reveal limitations in mathematical understanding rather than deficiencies in syntax generation.This distinction separates semantic interpretation failures from DSL-formatting failures.
  • B. Logic Errors: The r_triangle example is incorrect because it asserts AB perpendicular to BC although the construction makes CA perpendicular to AB.The right angle created by r_triangle is at A, so the target predicate names the wrong relation.
  • B. Logic Errors: Runs exceeding five minutes without new output are terminated and classified as logic errors.This rule addresses cases where incorrect formalizations cause AlphaGeometry to freeze or continue unsuccessfully.
  • B. Logic Errors: The taxonomy supports fine-grained diagnosis of whether failures arise from syntax generation, geometric interpretation, or semantic reasoning.This diagnosis is intended to inform future mitigation strategies for LLM-based mathematical formalization.

D. Baseline Model Performance Results

The baseline evaluation compares zero-shot and few-shot AlphaGeometry translation, revealing broad few-shot gains but a persistent gap between closed-source and open-source models.

  • Closed-source models frequently generate executable AlphaGeometry translations, whereas open-source models often fail through syntax violations, omitted constraints, or incorrect geometric interpretations.
  • 54 paired reference examples expose models to geometric constructions, DSL syntax patterns, and proof predicates.
  • 83.3% accuracy is achieved by Gemini-3.1 with few-shot prompting, up from 62.5% zero-shot.
  • 45.8% accuracy is reached by Qwen3:235B with few-shot prompting, up from 12.5%, while Llama3.1:70B rises from 0% to 23%.
  • Few-shot prompting consistently improves executable translation rates without requiring retraining, although a substantial closed-source advantage remains.

B. Human-Guided Hints

Human-guided correction uses diagrams to recover missing geometric context and targeted hints to fix localized translation errors, improving frontier-model translation without parameter updates but limiting scalability.

  • Diagram-based guidance adds spatial information about collinearity, circle memberships, and auxiliary constructions that may be difficult to infer from text alone.
  • Error-specific hints target incorrect clause parameters, predicate misuse, or invalid constructions while preserving the remaining translation structure.
  • The two-stage framework first supplies a geometry diagram and then provides targeted error-specific hints after an initial translation.
  • 14.29% improvement for GPT-5.4, 14.63% for Gemini 3.1, 26.47% for Claude Sonnet 4.6, and 32.14% for Grok-3 demonstrate gains without modifying model parameters.
  • Human-guided hints have limited scalability because diagrams require additional resources and error-specific feedback requires manual output inspection.

C. Supervised Fine-Tuning

The paper also studies supervised fine-tuning for smaller open-source models, using verified geometry formalizations to improve DSL adherence and reduce grammar-related errors.

  • Fine-tuning uses HAGeo-409, a human-verified collection pairing geometry problems with AlphaGeometry formalizations.
  • Models are trained to generate AlphaGeometry DSL representations directly from natural-language inputs.
  • Fine-tuning improves adherence to AlphaGeometry syntax and reduces several grammar-related error categories.
  • The paper places supervised fine-tuning alongside few-shot prompting and human-guided hints as mitigation strategies for translation failures.
  • Future work includes specialized autoformalization models, multimodal diagrams, symbolic feedback, and iterative self-correction.
Loading 2608.28481v1…