发表机构
Xi’an Jiaotong-Liverpool University（西交利物浦大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出密集神经符号耦合框架OmniGeo，统一处理平面、解析和立体几何，通过共享状态和可执行动作实现推理，在多个基准上取得领先性能。
AI 中文摘要
几何推理本质上是状态化的：解决一个问题需要在结构提议和精确演绎之间反复交替。我们将这一过程表述为密集的神经-符号耦合，其中神经引导和符号执行共享一个类型化状态，并在每一步搜索中通过可执行动作进行通信。神经提议贡献定理实例、构造和代数桥梁；符号运行时应用注册规则、传播精确约束并记录来源。一个嵌套控制器首先在神经和符号提议源之间分配计算，然后在已接纳的动作之间分配。我们在OmniGeo中实例化了该框架，这是一个用于平面、解析和立体几何的单一求解器。使用Claude Sonnet 4.6，OmniGeo在FormalGeo7K、Conic10K和SolidFGeo上分别达到94.2%、88.5%和89.8%（宏平均90.8%），并解决了30个IMO-AG-30问题中的21个。
英文摘要
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.
CommentsNeurIPS@Math-AI
