Geometry solver combines neural networks and symbolic reasoning
Dense Neuro-Symbolic Reasoning in a Unified Geometry State
Artificial Intelligence
Summary
Solving geometry problems often involves making guesses and then checking them carefully. The authors created a system that combines neural networks (which make smart guesses) with symbolic reasoning (which checks these guesses with strict rules). Their system, called OmniGeo, works for many types of geometry problems and performs strongly on several challenging benchmarks. This approach helps computers solve complex geometry problems more accurately.
What this means in practice
- •For software engineers: Create automated tools that solve complex geometry problems, helping with design and verification tasks in engineering software.
- •For computer-aided design teams: Integrate advanced geometry reasoning to improve automated construction checking and problem solving in CAD systems.
Authors
Ruoran Xu, Wending Gao, Haoyu Cheng, Xiaoqiang Kang, Qiufeng Wang
Abstract
Geometry reasoning is naturally stateful: solving a problem repeatedly alternates between structural proposals and exact deductions. We formulate this process as dense neural-symbolic coupling, in which neural guidance and symbolic execution share a typed state and communicate through executable actions at every search step. Neural proposals contribute theorem instances, constructions, and algebraic bridges; the symbolic runtime applies registered rules, propagates exact constraints, and records provenance. A nested controller allocates computation first between neural and symbolic proposal sources and then among admitted actions. We instantiate the framework in OmniGeo, a single solver for plane, analytic, and solid geometry. With Claude Sonnet 4.6, OmniGeo reaches 94.2%, 88.5%, and 89.8% on FormalGeo7K, Conic10K, and SolidFGeo, respectively (90.8% macro average), and solves 21/30 IMO-AG-30 problems.