PaperlayerView exact revision on arXiv

Source-linked AI summary

Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry

Zhaoyu Li, Hangrui Bi, Youyuan Zhang, Wenjie Ma, Zenan Li, Zhaolei Zhang, Xujie Si, Kaiyu Yang

arXiv:2608.14585v1cs.AI

TL;DR

Existing geometry-reasoning systems cover limited task types and lack accessible, diverse training resources; Euclid-Omni unifies symbolic deduction, algebraic computation, language, and vision, achieving strong calculation and proving performance with substantially less data and compute.

  • Problem

    Existing geometry systems separately address proving or calculation, often lack natural-language and diagram reasoning, and rely on small, inaccessible, or insufficiently diverse training resources.

  • Method

    Euclid-Omni couples Euclidea’s deductive and algebraic geometry engine with a configurable pipeline generating formal or natural-language, text or vision problems for calculation and proving.

  • Results

    Euclidea solves 99% of Geometry3K, while trained models reach state-of-the-art accuracy on three of four datasets and improve over the base model by 5.3% on average.

  • Takeaways & Limitations

    The framework supports geometric reasoning across multimodal calculation and Olympiad-level theorem-proving settings using substantially less training data and compute than prior methods.

  • Takeaways & Limitations

    Euclidea’s proofs can be lengthy for Olympiad-level problems and differ from those written by IMO contestants.

Abstract

from arXiv · show

Euclidean geometry is a compelling testbed for AI reasoning, as it demands the combination of intuitive diagram understanding, axiomatic deduction, and algebraic computation. Yet, existing approaches typically address only a subset of these abilities or struggle with competition-level problems. We introduce \textit{Euclid-Omni}, a unified neuro-symbolic framework that couples a formal geometry system with Large Language Models (LLMs) and Vision-Language Models (VLMs) to tackle both calculation- and proving-style problems, in formal and natural languages, up to Olympiad-level difficulty. At its core, we develop \textit{Euclidea}, a versatile symbolic geometry solver that automatically generates reasoning steps through deductive inference and algebraic computation. Building on this, we develop a data-generation pipeline that synthesizes symbolic problems and solutions, renders diagrams, and translates them into natural language, producing large-scale, diverse datasets for training LLMs and VLMs across a wide range of reasoning settings. Experiments show that VLMs trained on our synthetic data achieve superior performance on calculation tasks, and that LLMs combined with \textit{Euclidea} are competitive with state-of-the-art systems on Olympiad-level proving problems, despite using orders of magnitude less compute and training data. Code and scripts are publicly available at https://github.com/20171130/Euclid-Omni

1 Introduction

Euclid-Omni addresses the limited scope and accessibility of existing geometry systems with a unified neuro-symbolic framework spanning formal and natural languages, text and vision, and calculation and proving. It combines the Euclidea symbolic engine with a configurable synthetic-data pipeline for training LLMs and VLMs across difficulty levels.

  • Motivation: Existing IMO-level systems focus mainly on theorem proving, provide little algebraic computation, and rarely support natural language or visual diagrams.These limitations restrict their scope and usefulness for broader plane-geometry reasoning.
  • Motivation: Public geometry datasets remain small, insufficiently diverse, poorly stratified by difficulty, and generally lack released data-generation pipelines.The resulting compute and data-access barriers make modern LLM and VLM training difficult at scale.
  • Euclidea: Euclid-Omni introduces Euclidea, a symbolic engine that exhaustively applies admissible inference rules until reaching deductive closure.The framework is designed to support a broad range of geometric reasoning settings.
  • Data generation: Its data-generation pipeline synthesizes geometry problems across text and vision modalities, formal and natural language, and calculation and proving tasks.Datasets can be configured for specific training objectives and difficulty levels ranging from elementary problems to IMO-level challenges.

2 Related Work

Related work spans symbolic geometry solvers, manually annotated datasets and benchmarks, and learning-based neuro-symbolic methods that combine language or vision models with symbolic execution. Classical approaches divide between synthetic deduction and algebraic computation, while existing datasets remain small because annotation is costly.

  • Symbolic Approaches: Symbolic geometry solvers follow synthetic deduction or algebraic computation paradigms.Synthetic methods apply geometric rules through forward chaining, whereas algebraic methods encode geometric relations as polynomial equations.
  • Symbolic Approaches: Synthetic deductive databases systematically derive geometric facts but struggle with complex algebraic manipulation.
  • Datasets and Benchmarks: Geometry datasets pair problems with manually constructed symbolic formulations across calculation tasks and theorem proving, but remain relatively small because annotation is costly.Examples include GeoQA and Geometry3K for calculation, and UniGeo, JGEX-AG-231, and IMO-AG-30 for theorem proving.
  • Learning-Based Methods: Learning-based geometric reasoning increasingly uses neuro-symbolic methods in which LLMs or VLMs generate symbolic solution steps and solvers execute them.This design aims to provide correctness and interpretability.

3 Method

Euclid-Omni combines Euclidea’s formal neuro-symbolic geometry reasoning with synthetic problem generation, diagram rendering, and natural-language translation. Euclidea integrates deductive inference and symbolic algebra to solve calculation and proving tasks while producing human-readable reasoning traces.

  • Euclidea: Euclidea combines a deductive database with symbolic algebra to derive relations, simplify equations, and solve unknown geometric quantities.Its algebraic system uses SymPy, with linear systems solved by Gaussian elimination and other forms reduced to log-linear systems.
  • Euclidea: Euclidea formalizes diagrams as points and relations, treating metric and geometric information within a unified representation.Points are the basic primitives, while lines and triangles are defined from them.
  • Euclidea: The solver traces dependencies from goals back to initial conditions and linearizes the resulting dependency graph into ordered, human-readable symbolic solutions.Relations become intermediate nodes, given conditions become leaves, and post-order traversal produces the reasoning sequence.
  • Euclid-Omni pipeline: Euclid-Omni integrates a synthetic problem generator, diagram renderer, and natural-language translator to create large-scale, diverse training data for geometry tasks.The framework supports flexible configurations and can translate symbolic problems and solutions into fluent textual form.
  • Synthetic Problem Generation: The generator iteratively applies construction rules, samples coordinates satisfying their conditions, and selects minimally supported inferred goals as problem targets.Random coordinates can produce distinct topological configurations even under the same construction sequence.
  • Euclid-Omni pipeline: The pipeline can also be configured for autoformalization, diagram generation, and diagram understanding, although these applications are left for future work.The paper identifies these capabilities as potential applications rather than evaluated contributions in this section.

4 Experiments

Across calculation and proving benchmarks, Euclidea achieves strong solve rates and higher-quality proofs, while its integration of deduction and algebra is essential. Euclid-Omni’s synthetic-data pipeline improves VLM accuracy, supports efficient auxiliary-construction search, and produces correct, difficult, and diverse training problems.

  • Formal solver evaluation: Euclidea solves 99% of Geometry3K and two additional challenging IMO problems, outperforming existing formal geometry systems.Its deductive database and algebraic system are individually insufficient; their integration enables an order of magnitude more solved problems.
  • Formal solver evaluation: Euclidea produces more human-like, diagram-aligned, and compact symbolic proofs than DD+AR and Newclid.Unsolved problems involve formalization limits, large search spaces, timeouts, or required auxiliary constructions.
  • Calculation VLM evaluation: The fine-tuned VLM achieves state-of-the-art accuracy on three of four datasets, improves over the base model by 5.3% on average, and remains competitive on GeoQA.Training uses 20K combined examples, substantially less data than prior methods, while generalizing to substantially different evaluation diagrams.
  • Auxiliary-construction proving: With only 100K training samples, the hybrid system solves 223 problems on JGEX-AG-231 and 22 on IMO-AG-30, competing with AlphaGeometry trained on 100M problems and exceeding its 20M variant.Beam search proposes auxiliary constructions with branching factor 32, beam size 128, and maximum depth 4.
  • Synthetic-data analysis: Gemini solves 69.6% of sampled problems when generating solutions directly, whereas Euclidea-backed translations remain consistent with ground truth.The Euclid-Omni dataset has the largest average and median solution lengths, a more uniform embedding distribution, and broader goal-type coverage.

5 Limitations and Future Work

Euclid-Omni’s current system produces lengthy, less human-like proofs and samples construction rules uniformly without human priors. Future work targets richer deductive rules and better-aligned problem generation.

  • More Expressive and Human-Like Euclidea: Euclidea proofs can be lengthy for Olympiad-level problems and differ from proofs written by IMO contestants.Adding sophisticated theorems such as Menelaus’ or Desargues’ theorem could make proofs more compact and broaden the system’s range.
  • Better Design and Broader Usage of Euclid-Omni: Euclid-Omni samples construction rules uniformly, without using human priors or empirical distributions from existing problems.Future work could incorporate problem statistics or structural priors such as symmetries to align generated problems with target tasks.

Broader Impact · A Euclidea · A.1 Problem Formalization

Euclid-Omni aims to advance machine learning for geometric reasoning with a formalization that combines metric and diagrammatic relations. Euclidea emphasizes diagrammatic semantics, extensibility, and simplified point-based modeling to support faithful, human-like reasoning while anticipating only common misuse or overreliance risks.

  • Broader Impact: Euclid-Omni’s expected broader impact is positive, with no anticipated societal risks beyond common concerns such as misuse or overreliance.
  • A.1 Problem Formalization: Euclidea formalizes geometric relations as either metric relations or diagrammatic relations.Metric relations use predicate propositions or equations, while diagrammatic relations encode topological configurations such as Between and SameSide.
  • A.1 Problem Formalization: Euclidea distinguishes Collinear from Not(Collinear) because collinearity requires formal proof, whereas non-collinearity is usually directly inferred from diagrams.
  • A.1 Problem Formalization: Euclidea’s extensible relation system can add richer diagrammatic predicates and higher-level metric semantics to make formalizations more concise and reasoning steps more streamlined.Examples include acute or obtuse angles, relative segment lengths, and composite relations defined through existing ones.
  • A.1 Problem Formalization: Euclidea’s key innovation over existing IMO-level systems is integrating diagrammatic relations for human-like reasoning about angular and topological relationships.
  • A.1 Problem Formalization: Without diagrammatic relations, angle equality ambiguities hinder faithful natural-language translation, theorem proving, unique angle determination, and consistent numerical results.Euclidea uses diagrammatic information to distinguish equal from supplementary angles based on relative side-of-line configurations.
  • A.1 Problem Formalization: Euclidea extracts diagrammatic inferences from the initial diagram rather than embedding them in deduction rules, avoiding contradiction- and disjunction-based reasoning that would make proofs complex and verbose.
  • A.1 Problem Formalization: Unlike E, Euclidea treats points as the only first-class entities with implicit connections, simplifying rule-based deduction and avoiding trivial auxiliary constructions.

A.2 Deductive Database · A.3 Algebraic System

Euclidea combines a relational deductive database with staged algebraic solving to derive geometric consequences efficiently. Its algebraic system separates linear, log-linear, and nonlinear reasoning, propagating solved constraints without simultaneously solving an intractable nonlinear system.

  • A.2 Deductive Database: Euclidea stores geometric entities and predicates in an in-memory SQL database, representing each predicate as a relational table.A union-find structure maintains equivalence relationships among geometric quantities.
  • A.2 Deductive Database: Conjunctions of geometric conditions become table joins, enabling applicable inference rules to be enumerated declaratively through SQL queries.The Midpoint predicate is translated into joins over points, lengths, collinearity, and betweenness relations.
  • A.2 Deductive Database: A lexical partial order on variable names removes redundant permutations by retaining one canonical ordering for equivalent configurations.For example, b.name < c.name treats Midpoint(a,b,c) and Midpoint(a,c,b) as the same configuration.
  • A.3 Algebraic System: At each iteration, Gaussian elimination solves linear angle, linear length, and log-linear length equations before combining their results to solve other nonlinear equations.Examples include angle-sum and angle-ratio constraints, length equalities and ratios, and area relations.
  • A.3 Algebraic System: Euclidea keeps the three (log-)linear length systems separate because solving them jointly can produce high-order polynomials and intractable symbolic solutions.It substitutes their solutions into remaining nonlinear equations, including trigonometric and higher-order polynomial constraints.
  • A.3 Algebraic System: When substitution determines a single variable or yields a new (log-)linear equation, Euclidea records the result or reintroduces it into the appropriate subsystem.This propagates constraints among the three (log-)linear systems without requiring simultaneous solution of the full nonlinear system.
  • A.3 Algebraic System: In the rectangle example, Gaussian elimination finds AB = 3 and BC = 4, after which post-processing and removal of negative lengths yield AC = 5.The resulting AC = 5 constraint is added to both the linear and log-linear length systems for later iterations.

A.4 Solution Generation … B.2 Examples of Templates and Prompts for Natural Language Translation

Euclid-Omni generates traceable, human-like geometry solutions by recording inference dependencies, constructing proof graphs, and translating formal problems and solutions into varied natural-language and multiple-choice formats.

  • A.4 Solution Generation: Euclidea records each inferred relation together with its inference rule and all conditions used to derive it.For SAS congruence, the recorded source includes non-collinearity, two equal side-length conditions, and an equal-angle condition.
  • A.4 Solution Generation: Euclidea traces algebraic dependencies differently for linear and nonlinear systems, using Gaussian elimination for linear equations and substitution with symbolic solving for nonlinear equations.The dependency strategy reflects the solver used by each equation class.
  • A.4 Solution Generation: Backtracking from the target constructs a dependency graph whose root is the goal, leaves are initial conditions, and post-order traversal yields sequential proof steps.The graph also contains intermediate relations as internal nodes.
  • A.4 Solution Generation: Euclidea makes proofs more concise by merging steps with shared or hierarchical conditions and omitting diagrammatic relations that are usually trivial in human-written proofs.The framework can choose between ℓ0 and ℓ1 dependency formulations according to system complexity and user requirements, trading minimal sparsity against efficiency.
  • B.1 Problem Synthesis: Euclid-Omni synthesizes problems by sampling construction rules and consistent diagrams, using parameterized rules for fully determined calculation diagrams and freer constructions for proving problems.Generated diagrams may vary by sampled coordinates while preserving construction-level invariant relations.
  • B.2 Examples of Templates and Prompts for Natural Language Translation: The framework translates formal constructions and relations through multiple randomly selected templates, such as alternative verbalizations of circumcenters and perpendicular lines.Template variation is applied separately to construction rules and solution relations.
  • B.2 Examples of Templates and Prompts for Natural Language Translation: Dedicated LLM prompts rewrite template-based problems and solutions into fluent language while preserving meaning, simplifying redundant steps, and restricting output to the requested content.Solution prompts place the final answer inside \boxed{} and allow step-wise formatting only when it improves clarity.
  • B.2 Examples of Templates and Prompts for Natural Language Translation: Formal problems and solutions can also be converted into multiple-choice questions with exactly four labeled options, one correct answer, plausible distractors, and a final boxed choice label.The reference answer is used only to determine correctness, while the rewritten solution must match the provided final choice.

B.3 Examples of Synthetic Data Instances

This section presents synthetic Euclidean geometry instances spanning final-answer and multiple-choice calculation formats, with rendered diagrams and worked solutions. It also includes symbolic problems requiring auxiliary constructions for concyclicity and angle relations.

  • Calculation Problems: The generated calculation instances include one final-answer problem and one multiple-choice problem, each paired with a corresponding diagram.The final-answer example appears with Figure 7, and the multiple-choice example with Figure 8.
  • Calculation Problems: The final-answer example asks for triangle BDG’s area in a square-and-circle configuration and derives the result 20000√2/9.The solution uses right-triangle similarity to obtain DG = 400/3 and BG = 100√2/3 before computing the area.
  • Calculation Problems: The multiple-choice example asks for triangle BCD’s area and selects 4096/13 from four choices after applying triangle similarity.The construction uses AB = 52, BC = 32, and CD = 256/13.
  • Auxiliary-Constructions Problems: Two additional synthetic instances require auxiliary constructions: one targets Concyclic(a,c,e,f), and the other targets an angle expression equal to 180.The construction sequences use segments, circles or diameters, lines, perpendicular bisectors, and angle bisectors.

C Experiments · C.1 Examples of Generated Formal Solutions

The section compares formal proofs generated by Euclidea, AlphaGeometry, Newclid, and PyEuclid on two randomly selected geometry problems. The examples show that systems can reach the same conclusions through substantially different deduction styles, representations, and strategies.

  • C.1 Examples of Generated Formal Solutions: The evaluation compares Euclidea with AlphaGeometry, Newclid, and PyEuclid on one JGEX-AG-231 problem and one IMO-AG-30 problem.Both problems are presented with natural-language formulations and corresponding diagrams.
  • C.1 Examples of Generated Formal Solutions: For the JGEX-AG-231 problem, Euclidea derives AE = AF through collinearity, perpendicularity, angle relations, length relations, and algebraic computation.Its displayed proof concludes with Angle_a_e_f - Angle_a_f_e => Length_a_e - Length_a_f.
  • C.1 Examples of Generated Formal Solutions: AlphaGeometry proves the same JGEX-AG-231 result using perpendicular-line relations, similar triangles, and the ratio OC:OE = AF:AE.The proof then continues from the midpoint and circle-related relations toward the target equality.
  • C.1 Examples of Generated Formal Solutions: Newclid reaches AF = AE for the first problem through midpoint, perpendicularity, parallelism, equal-angle, and isosceles-triangle deductions.Its proof explicitly applies rules including “Hypotenuse is diameter,” “Properties of midpoint,” and “Equal base angles imply isosceles.”
  • C.1 Examples of Generated Formal Solutions: PyEuclid also concludes Length_a_e - Length_a_f for the first problem, using symbolic angle and length equations together with square-root expressions.The displayed final step equates two expressions involving sqrt(Length_d_f)*sqrt(Length_e_f)/2.
  • C.1 Examples of Generated Formal Solutions: For the IMO-AG-30 problem, Euclidea’s displayed proof uses length equalities, angle relations, and a rhombus deduction before continuing toward the target.The shown steps include equal distances from O and an implication to Rhombus.
  • C.1 Examples of Generated Formal Solutions: AlphaGeometry’s second proof establishes E,A,F,C as concyclic, derives AF = AE, and then uses collinearity and angle equalities.The displayed chain includes the implications E,A,F,C are concyclic and AF = AE.
  • C.1 Examples of Generated Formal Solutions: The systems’ proofs vary substantially in style and strategy: AlphaGeometry and Newclid use full-angle formalization and line-pair angle representations, which can create supplement and ambiguity issues.The passage contrasts these representations with Euclidea and notes that they may produce angle relations that appear incorrect under human reasoning.

C.2 Ablation Study over Training Datasets

The ablation fine-tunes Qwen2.5-VL-7B under matched settings on several 20K training-data choices, including individual datasets, mixtures, and Ours 10K. Under comparable compute, Euclid-Omni data yields competitive or superior performance on geometry reasoning benchmarks.

  • Experimental setup: Qwen2.5-VL-7B is fine-tuned under matched settings for a controlled comparison of training datasets.The evaluated data choices include Geo170K, GeoGen, TR-CoT, two 20K mixtures, and Ours 10K.
  • Training data choices: The study trains on 20K subsets of Geo170K, GeoGen, and TR-CoT, plus 10K+10K mixtures of Geo170K with GeoGen or TR-CoT.An additional Ours 10K condition is included as an ablation.
  • Results: Under comparable compute, Euclid-Omni data consistently achieves competitive or superior results on geometry reasoning benchmarks.Table 5 reports accuracy (%) across four benchmarks under different training-data choices.

C.3 Examples of Generated Natural Language Solutions · C.4 Examples of Generated Formal Auxiliary Constructions

Examples show that synthetic-data finetuning improves informal geometry understanding and algebraic computation, while the formal approach generates auxiliary constructions that can differ from AlphaGeometry and sometimes use fewer constructions. Together, the examples illustrate multiple valid solution strategies across natural-language and formal geometry tasks.

  • C.3 Examples of Generated Natural Language Solutions: Training on the synthetic dataset improves the finetuned model’s ability to understand and solve informal geometry problems compared with base Qwen2.5-VL.The section compares generated solutions on GeoQA and Geometry3K examples.
  • C.3 Examples of Generated Natural Language Solutions: The GeoQA example demonstrates that finetuning enables correct interpretation of diagrammatic relationships in a tangent-to-circle problem.The problem specifies BA tangent to circle O, angle B = 45.0, and AB = 2.0.
  • C.3 Examples of Generated Natural Language Solutions: The Geometry3K example demonstrates robust algebraic computation by solving the quadrilateral-angle equation to obtain ∠R = 58°.The angles sum to 360°, yielding x = 58 and therefore ∠R = 58°.
  • C.4 Examples of Generated Formal Auxiliary Constructions: Our predicted auxiliary constructions often differ from AlphaGeometry’s, showing that multiple valid auxiliary strategies can achieve the same goal.The comparison uses two examples from the IMO-AG-30 dataset.
  • C.4 Examples of Generated Formal Auxiliary Constructions: In the first IMO-AG-30 example, our LLM constructs K as the circumcenter of triangle AMN, whereas AlphaGeometry constructs K with KM = KN and adds point L.The two systems therefore produce different formal construction sequences for the same problem.
  • C.4 Examples of Generated Formal Auxiliary Constructions: In the second example, our LLM constructs p as an intersection, while AlphaGeometry constructs three midpoints X, Y, and Z.The LLM construction intersects circle (O, A) with Line (H, Q).
Loading 2608.14585v1…