Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry
Euclid-Omni unifies deduction and algebra through Euclidea, solving 595/601 Geometry3K problems and 16 IMO-AG-30 problems.
Key Findings
Methodology
The framework centers on Euclidea, a Python formal geometry system that represents points, metric relations, and diagrammatic topology. An SQL deductive database saturates theorem rules, while a SymPy algebraic module solves linear, log-linear, and residual complex equations. Euclid-Omni then samples construction programs, coordinates, rendered diagrams, natural-language statements, and proof traces, training VLMs for calculation and LLMs to propose auxiliary constructions.
Key Results
- Euclidea solved 595/601 Geometry3K problems, approximately 99%, versus 567 for PyEuclid and 426 for Inter-GPS. It also solved 207/231 JGEX-AG-231 problems and 16/30 IMO-AG-30 problems.
- A model trained with 20K synthetic instances reached 76.6% on GeoQA, 61.0% on Geometry3K, 74.7% on MathVista, and 51.0% on MathVerse, exceeding the listed Qwen2.5-VL-7B baseline on all four benchmarks.
- Ablations show complementarity: removing the algebraic system leaves only 1 Geometry3K and 74 JGEX solutions, while removing the deductive database leaves 36 and 2, respectively. Neither component is sufficient alone.
Significance
The paper connects geometric calculation, Olympiad proving, visual understanding, natural language, and formal reasoning in one reproducible framework. Its central lesson is architectural: neural models can handle perception, language, and candidate construction, while a symbolic engine supplies verification and execution. Public code and generation scripts address a long-standing reproducibility problem in geometry AI. The work therefore matters not only for benchmark scores, but also for educational systems and reliable mathematical reasoning.
Technical Contribution
Euclidea alternates SQL-based deduction with SymPy algebra. Angle and length equations become Ax=b and are solved by Gaussian elimination; ratio relations are converted to log-linear systems; complex equations are simplified through accumulated substitutions. Proof extraction solves min_z||z||_t subject to [A|b]^Tz=c using PySCIPOpt, selecting sparse supporting equations. The data pipeline unifies construction rules, coordinate sampling, Matplotlib rendering, verified templates, LLM paraphrasing, and configurable difficulty.
Novelty
Compared with AlphaGeometry’s proof-oriented auxiliary construction, Inter-GPS’s calculation programs, and DD+AR’s formal proving specialization, Euclid-Omni aims to unify vision, language, calculation, and proving through a public pipeline. The novelty lies less in a single theorem than in connecting Euclid-style relational representation, forward deduction, algebraic solving, and readable proof reconstruction.
Limitations
- Failures arise when a problem cannot be expressed in the current formal language, when many points create prohibitive search spaces and timeouts, or when sophisticated auxiliary constructions are required. Thus the solver is not yet a universal Olympiad system.
- Natural-language diversity depends on manually verified templates followed by LLM paraphrasing. The supplied paper excerpt also omits complete training hyperparameters, scaling ablations, and statistical significance analyses.
Future Work
The authors identify autoformalization, diagram generation, and diagram understanding as natural extensions. Further work should expand auxiliary-construction search, improve large-diagram scalability and visual parsing, calibrate uncertainty, and measure the distribution gap between synthetic and authentic textbook or competition diagrams.
AI Executive Summary
Plane geometry is a demanding AI test because success requires reading a diagram, applying axioms, and manipulating algebra. Existing Olympiad systems mainly prove theorems, while calculation systems cover narrower tasks. Public datasets are also small and poorly stratified, making it difficult to train general-purpose language and vision models.
Euclid-Omni addresses this gap with Euclidea, a formal solver that stores points, metric facts, and topological relations. An SQL deductive database applies geometry rules until closure; a SymPy module solves equations. Around this engine, the authors build a generator that samples ruler-and-compass constructions, coordinates, rendered diagrams, natural-language descriptions, and aligned solutions. Neural models handle perception, language, and proposed constructions; the symbolic engine checks them.
Euclidea solves 595/601 Geometry3K problems, 207/231 JGEX-AG-231 problems, and 16/30 IMO-AG-30 problems. With 20K synthetic examples, a VLM reaches 76.6%, 61.0%, 74.7%, and 51.0% on GeoQA, Geometry3K, MathVista, and MathVerse. The system still struggles with auxiliary constructions, large search spaces, and formalization coverage. Its strongest contribution is therefore a reproducible, unified infrastructure for geometry reasoning rather than a claim that the domain is solved.
Deep Analysis
Background
Geometry AI spans classical theorem proving, algebraic methods, and neuro-symbolic learning. Gröbner-basis and Wu methods offer algebraic power but opaque proofs; NGS and Inter-GPS target calculation; LeanEuclid, DD+AR, and AlphaGeometry target proving. Datasets such as GeoQA, Geometry3K, JGEX-AG-231, and IMO-AG-30 cover distinct settings, but no broadly accessible pipeline previously unified them.
Core Problem
A robust system must parse language and diagrams, distinguish explicit metric facts from implicit topology, perform deduction and algebra, and invent auxiliary constructions. Full-angle notation can confuse an angle with its supplement and is unsuitable for many calculations. Pure neural chain-of-thought can hallucinate intermediate steps and offers weak formal verification.
Innovation
First, Euclidea uses an Elements-inspired relational representation for both calculation and proving. Second, its SQL deductive database and algebraic solver iteratively reinforce one another. Third, sparse optimization reconstructs compact proof traces. Fourth, Euclid-Omni combines construction programs, coordinate sampling, rendering, verified templates, and LLM paraphrasing into configurable multimodal data. This differs from systems specialized for either numerical answers or theorem proofs.
Methodology
- �� Input: points plus metric and diagrammatic relations.
- �� Deduction: SQL joins match rules such as the Angle Bisector Theorem and isosceles-triangle properties until closure.
- �� Algebra: angle and length equations become Ax=b and use Gaussian elimination; ratios become log-linear systems; complex equations are simplified by substitution.
- �� Tracing: PySCIPOpt selects sparse supporting equations, forming a dependency graph.
- �� Generation: rules such as construct foot and construct square create diagrams; coordinates are sampled, figures rendered, templates instantiated, and an LLM paraphrases aligned text.
Experiments
Formal evaluation uses Geometry3K (601 calculation problems), JGEX-AG-231 (231 textbook and Olympiad problems), and IMO-AG-30 (30 IMO problems). Baselines include Inter-GPS, PyEuclid, DD+AR, and Newclid. The time limit is 600 seconds; numerical answers count within 2% of labels, while proofs must be valid. VLM evaluation uses GeoQA, Geometry3K, MathVista, and MathVerse, with ablations removing either algebra or deduction.
Results
Euclidea solves 595, 207, and 16 problems across the three benchmarks; PyEuclid solves 567 and 202 on the first two, while DD+AR solves 198 and 14 on the proving sets. The 20K-trained VLM reaches 76.6/61.0/74.7/51.0%, versus Qwen2.5-VL-7B’s 69.4/56.4/72.2/44.1%. Ablations establish that hybrid reasoning, not either module alone, drives performance.
Applications
The framework can support geometry tutoring, automatically generated practice, diagram-based feedback, and formally checked solutions. Teachers can control construction rules and target relations; researchers can generate aligned symbolic, visual, and textual data. Deployment requires validation of templates, diagram parsing, and timeout behavior.
Limitations & Outlook
The solver depends on a predefined language, theorem library, and construction library; unfamiliar theorems or nonstandard diagrams may be unrepresentable. More points cause combinatorial search and timeouts, while auxiliary constructions remain a major bottleneck. Synthetic diagrams may not match handwritten or textbook distributions. The provided excerpt does not report complete training costs, hyperparameters, or significance tests.
Plain Language Accessible to non-experts
Imagine Euclid-Omni as a geometry factory. First, a clerk labels every point, line, circle, equality, and perpendicular relation. A rule worker then applies trusted instructions: if two sides are equal, it may mark a triangle as isosceles; if lines are perpendicular, it records the consequences. A calculation worker translates lengths and angles into equations and eliminates unknowns. Finally, an auditor works backward from the requested answer, keeps only the necessary checks, and prints an understandable solution.
The factory can also manufacture training exercises. It assembles a diagram with ruler-and-compass steps, randomly chooses valid coordinates, draws the image, writes a text version, and preserves the answer. This gives models many differently worded versions of the same kind of reasoning. In the experiments, the factory solved 595 of 601 Geometry3K problems and helped a vision model perform strongly on four benchmarks.
ELI14 Explained like you're 14
Think of a geometry video game. You see dots, lines, and circles, then the game asks for a length or a proof. A chatbot might give a confident-looking explanation while secretly making a wrong move. Euclid-Omni pairs the chatbot with a strict referee: the language model reads the problem, looks at the picture, and suggests an extra line; Euclidea checks every move using geometry rules and equations.
It has two main powers. One is like collecting game cards: facts such as “equal,” “perpendicular,” and “on the same line” are stored, then new cards are created by applying rules. The other is like solving a math puzzle: angles and lengths become equations, and elimination finds the missing value. Working together is much safer than guessing.
The system can even make practice levels by building random valid diagrams, drawing them, and writing explanations. It solved 595 of 601 Geometry3K problems and 16 of 30 IMO-AG-30 problems. But super-complicated pictures, too many points, and clever helper lines can still defeat it. So it is a powerful teammate—not an unbeatable champion!
Glossary
Euclidea
A Python formal plane-geometry solver built around points and relations. It combines rule-based deduction with algebraic computation and proof tracing.
The symbolic core of Euclid-Omni.
Deductive database
A database that stores facts, equivalence classes, and theorem conditions. SQL joins identify rules whose premises are satisfied.
It expands the state toward deductive closure.
Gaussian elimination
A procedure for reducing linear equations and exposing variable relations. The paper applies it to angle and length systems written as Ax=b.
It supports both calculation and proof.
Neuro-symbolic reasoning
A division of labor in which neural models handle perception and language while symbolic programs execute verifiable reasoning.
It describes the LLM/VLM–Euclidea architecture.
Auxiliary construction
An added point or line not directly given in the original diagram but introduced to complete a proof. Discovering it is often the hardest Olympiad step.
One of the LLM’s formal prediction targets.
Open Questions Unanswered questions from this research
- 1 How can a solver invent auxiliary lines outside its predefined construction library while controlling the combinatorial explosion and preserving proof validity?
- 2 How well do synthetic diagrams transfer to noisy photographs, hand-drawn figures, and authentic textbook layouts? Stronger vision parsing and cross-domain evaluation are needed.
- 3 The excerpt does not provide full training configurations, scaling studies, or significance tests, leaving the compute-efficiency claim incompletely characterized.
Applications
Immediate Applications
Geometry tutoring
An educational platform could let a VLM read the diagram, an LLM explain the problem, and Euclidea verify each step. Teachers could generate difficulty-controlled exercises and receive checkable proofs rather than opaque final answers.
Question-bank and proof generation
Textbook teams and researchers could use the released scripts to create formal problems, diagrams, natural-language variants, and verified traces. Minimal supporting constructions reduce manual authoring and annotation while preserving solution structure.
Long-term Vision
A mathematical-reasoning infrastructure
With broader theorem libraries, stronger visual parsing, and better auxiliary search, the framework could connect school geometry, competition mathematics, and formal proof assistants. Open-world knowledge, noisy diagrams, and efficiency remain major obstacles.
Abstract
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