Dense Neuro-Symbolic Reasoning in a Unified Geometry State

Ruoran Xu; Wending Gao; Haoyu Cheng; Xiaoqiang Kang; Qiufeng Wang

cs.AIOct 3, 2026

Dense Neuro-Symbolic Reasoning in a Unified Geometry State

Authors: Ruoran Xu, Wending Gao, Haoyu Cheng, Xiaoqiang Kang, Qiufeng Wang

Organizations: Xi’an Jiaotong-Liverpool University

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.

Figures & tables

Figure 1: Omni-Geo overview. Staged formalization initializes a shared typed state, which neural guidance and symbolic rollout extend through adaptive search. Execution feedback informs subsequent steps, while provenance records their logical dependencies.

Figure 2: Nested source/action search. Source-UCB chooses symbolic enumeration or neural proposal at a leaf; both enter one typed admission interface. Inner PUCT traverses admitted children, while isolated execution, goal checking, progress evaluation, and provenance feed the next search decision.

General-purpose models
Method	FormalGeo7K	Conic10K	SolidFGeo	Avg.
Claude Sonnet 4.6	71.6	78.2	61.7	70.5
GPT-5.4	85.4	82.4	65.4	77.7
Gemini-3-Pro	85.3	79.8	63.8	76.3
DeepSeek-V4-Flash (text only)	61.2	84.6	63.0	69.6
Geometry-specific systems

Table 1: End-to-end accuracy (%) on the three main benchmarks. Avg. is the unweighted macro average over FormalGeo7K, Conic10K, and SolidFGeo.

Variant	FormalGeo7K	Conic10K	SolidFGeo	Avg.	$\Delta$ Avg.
Full Omni-Geo	94.2	88.5	89.8	90.8	–
Fixed source schedule	89.1	83.5	84.5	85.7	$-5.1$
No neural bridge actions	80.9	65.0	68.6	71.5	$-19.3$
No admission filter	87.8	79.5	82.6	83.3	$-7.5$
One-pass formalization	84.3	79.0	80.5	81.3	$-9.6$

Table 2: Component ablations with Claude Sonnet 4.6 as the neural backend.

\Delta

Avg. is the absolute percentage-point change from the full system.

Method	Parameter adaptation	Specialized resource	Solved
AlphaGeometry [ 31 ]	from-scratch LM	100M theorem–proof examples (9M aux.)	25/30
TongGeometry [ 32 ]	policy/value fine-tuning	6.7B generated aux. problems	30/30
Omni-Geo	None	$<200$ registered executable schemas	21/30

Table 3: Geometry-specific specialization regimes on IMO-AG-30. Resource quantities are reported in the native units of the corresponding systems.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Class	Role	Examples
Construction	Conservative introduction of entities	$\operatorname{Shape}(ABC)$ , $\operatorname{Collinear}(ABC)$ , $\operatorname{Cocircular}(O,AB)$ , $\operatorname{Coplanar}(U,ABC)$ , $\operatorname{Cospherical}(O,ABC)$
Entity	Typed geometric objects	$\operatorname{Triangle}(ABC)$ , $\operatorname{Circle}(O)$ , $\operatorname{Plane}(U)$ , $\operatorname{Sphere}(O)$ , $\operatorname{Cube}(ABCDEFGH)$ , $\operatorname{Cylinder}(P,Q)$ , $\operatorname{Conic}(\Gamma)$
Relation	Qualitative facts	$\operatorname{ParallelBetweenLine}(AB,CD)$ , $\operatorname{PerpendicularBetweenLineAndPlane}(AB,U)$ , $\operatorname{OnCurve}(A,\Gamma)$ , $\operatorname{Tangent}(l,\Gamma)$
Attribution	Exact geometry–algebra bridge	$\operatorname{LengthOfLine}(AB)$ , $\operatorname{MeasureOfAngle}(ABC)$ , $\operatorname{Coordinate}(A,x_{A},y_{A})$ , $\operatorname{RadiusOfSphere}(O)$ , $\operatorname{VolumeOfCylinder}(P,Q)$

Appendix

Table 4: Representative declarations in the unified signature.

Role	Inputs	Required output	Cap	Retry/round limit
Construction compiler	statement, optional image, typed whitelist, examples	JSON list of construction GeoDL strings	4096	1
Condition compiler	statement, image, construction GeoDL , typed whitelist, examples	JSON object with text/image GeoDL lists	4096	1
Goal compiler	statement and compiled GeoDL	typed goal_geodl and model-generated $\tilde{y}_{\theta}$	4096	1
Compiler critic	statement and candidate GeoDL	JSON ok / missing record	2048	2 rounds
Search planner	current formal state, equations, goal, subgoal hints	geometry plan naming concrete next steps	8192	3 rounds/problem
Action extractor	plan, engine symbols, equations, action schema	$\leq 3$ typed actions with scores in $[0,1]$	4096	paired with planner

Appendix

Table 5: Neural call interface used in every benchmark. “Cap” is the maximum completion length per call.

Parameter	Value
Nominal search cap	600 s/problem
Worker watchdog grace	30 s
$c_{\rm puct}$	1.5
$c_{\rm meta}$	1.5
Maximum tree depth	15
Neural expansion rounds	3/problem

Appendix

Table 6: Shared inference settings.

Figure 3: Sensitivity to the inner PUCT constant

c_{\rm puct}

and the outer source-allocation constant

c_{\rm meta}

. Each sweep varies one constant and holds the other at

1.5

Mathematical Reasoning

Mathematical reasoning studies how AI systems solve problems, construct proofs, use tools, and discover or verify mathematical results.

See all 153 papers

Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
Jun 26, 2026Can Li, Ting Zhang, Junbo Zhao +1Automated Theorem Proving Multimodal Reasoning
Beijing Normal University
Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning
May 11, 2026Ruoran Xu, Haoyu Cheng, Bin Dong +1Symbolic Reasoning Multimodal Reasoning
Xi’an Jiaotong-Liverpool University · Ricoh Software Research Center Beijing Co.,Ltd.
BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction
Jun 3, 2026Qi Wang, Peijie Wang, Fei Yin +1Mathematical Reasoning Neuro-Symbolic Reasoning
1MAIS, Institute of Automation of Chinese Academy of Sciences · School of Artificial Intelligence, University of Chinese Academy of Sciences

Jun 26, 2026J/K move · Enter open · S save

Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing

Can Li, Ting Zhang, Junbo Zhao, Hua Huang

Beijing Normal University

Automated Theorem Proving Multimodal Reasoning Mathematical Reasoning Neuro-Symbolic Reasoning Autoformalization

Open paper AskPDF arXiv

Geometry Problem Solving have increasingly adopt the neuro-symbolic paradigm, combining neural intuition with symbolic rigor. However, current frameworks suffer from severe bottlenecks in two core stages: autoformalization, which treats multimodal translation as a static task decoupled from downstream solver compatibility, and theorem prediction, where solvers frequently hit a deductive impasse due to fixed rule libraries. To address these, we propose SD-GPS, a solver-driven framework that treats the symbolic solver as an execution oracle throughout both formalization and deduction. First, Solver-Driven Autoformalization unifies supervised formal-language adaptation and solvability-guided reinforcement learning into a single module built on QwenVL3-2B, making executability the central training signal. Second, Verified Theorem Proposing introduces an impasse-aware agent that proposes local auxiliary lemmas from current proof states, ensuring soundness by filtering all proposals through symbolic verification. Empirical evaluations on Geometry3K and PGPS9K demonstrate that SD-GPS consistently outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes, proving that closing the loop between multimodal perception and symbolic execution significantly improves geometric reasoning, offering profound insights into how neural agents can be grounded by formal systems to achieve verifiable problem-solving capabilities.

Abstract

Mathematical Reasoning

Explore similar work

Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing

Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning

BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction