Omni-Geo couples neural and symbolic reasoning in a unified typed geometry state, reaching 90.8% macro average across three geometry benchmarks and solving 21/30 IMO-AG-30 problems

Dense neural–symbolic coupling: neural proposals and symbolic execution share one typed state, and every admitted action is executed before the next decision, so a neural construction can immediately expose new symbolic consequences and a symbolic deduction can immediately reshape the next neural proposal. Where prior geometry systems established structured text–diagram reasoning, learned theorem guidance, executable formal states, and neural-guided search separately, this work organizes these capabilities around one continually updated typed geometry state. Supported by a formal description of the shared state, common execution interface, explicit provenance, and nested source/action allocation, with ablations measuring each component across three benchmarks and IMO-AG-30.

Instantiation as Omni-Geo: one formal language and solver spans plane, analytic (including conics), and solid geometry, with all three families using one parser, condition store, theorem matcher, equation engine, and goal checker. Prior systems were largely confined to a single geometry family; this work reuses one GeoLib/GeoDL declaration set and typed transition contract across domains. End-to-end evaluation on FormalGeo7K, Conic10K, and SolidFGeo, with the same runtime and search stack yielding cross-domain results under two frozen backends, Claude Sonnet 4.6 and Qwen3-VL-8B-Thinking.

A nested controller allocates computation first between neural and symbolic proposal sources via source-UCB and then among admitted actions via action-PUCT; ablations show a fixed source schedule lowers the macro average and removing neural bridge actions produces the largest drop. Source choice itself becomes a search decision, separating source allocation from action revisit allocation. Component ablations change one component at a time: fixed source schedule, no neural bridge actions, no admission filter, and one-pass formalization each reduce accuracy on every benchmark; a search-constant sweep places the shared setting at the highest observed accuracy in all three domains.

On IMO-AG-30, the Claude-based configuration solves 21/30 problems with a frozen neural backend and fewer than 200 registered executable schemas, placed alongside AlphaGeometry (trained from scratch on 100M theorem–proof examples) and TongGeometry (6.7B generated auxiliary problems with policy/value fine-tuning). Shows the same interface operating in an olympiad construction setting with a compact executable geometry library and no parameter adaptation. Table 3 keeps each system's specialization resource in its native unit and places Omni-Geo's compact executable theory in the same empirical context.

The results target benchmark solving in plane, analytic (including conics), and solid geometry, under settings that use official statement–diagram pairs (Conic10K uses its text input); the same runtime and search stack holds under two frozen backends, Claude Sonnet 4.6 and Qwen3-VL-8B-Thinking, indicating the symbolic substrate is reusable. The IMO-AG-30 experiment extends the same design to olympiad construction problems using fewer than 200 registered executable schemas. For readers wishing to reuse the interface, Appendix C gives complete prompts, the call interface, and search hyperparameters (nominal 600 s/problem, maximum depth 15, three neural expansion rounds), enabling reconstruction in their own geometry domains.

The formal guarantees are conditional soundness relative to the compiled instance; fidelity of the compiled instance to the raw text and diagram is a separate compilation property, and procedural outputs are reported separately and not treated as proof certificates. The search-constant sweep shows analytic geometry is relatively stable around the shared setting while solid geometry responds more strongly to the outer source-allocation constant, a difference worth watching in broader settings. Progress weights are set manually and held fixed across benchmarks, and the range of their influence remains an open question. On IMO-AG-30, 21/30 is placed alongside AlphaGeometry's 25/30 and TongGeometry's 30/30, but each system's specialization resource is recorded in its native unit, so cross-system comparison warrants careful interpretation.