Dense Neuro-Symbolic Reasoning in a Unified Geometry State

arXiv:2610.04280 · cs.AI · Submitted 2026-10-03 · Read on arXiv

cs.AI

Submitted: 2026-10-03

Updated: 2026-10-03

Comments: NeurIPS@Math-AI

License: http://creativecommons.org/licenses/by/4.0/

The gist: Geometry reasoning is naturally stateful: solving a problem repeatedly alternates between structural proposals and exact deductions.

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.

Sources

Related papers