Omni-Geo以统一类型化几何状态耦合神经与符号推理，在三个几何基准上取得90.8%宏平均并在IMO-AG-30解出21/30
核心概要
该工作提出稠密神经—符号耦合框架，让神经提议与符号执行共享一个类型化几何状态并在每步搜索中通过可执行动作交互，实例化为覆盖平面、解析（含圆锥曲线）与立体几何的单一求解器Omni-Geo；使用Claude Sonnet 4.6时在FormalGeo7K、Conic10K、SolidFGeo上分别达到94.2%、88.5%、89.8%（宏平均90.8%），并在IMO-AG-30上解出21/30题。
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.
arXiv深度剖析
提出稠密神经—符号耦合：神经提议与符号执行共享同一类型化状态，每个被接纳动作在执行后才进入下一步决策，使神经构造能立即暴露新的符号推论，符号推论也能立即重塑下一次神经提议。 相较以往将文本—图示推理、学习式定理引导、可执行形式状态与神经引导搜索分别处理的几何系统，该工作把这些能力组织在一个持续更新的类型化几何状态之上。 以共享状态、统一执行接口、显式溯源与嵌套源/动作分配的形式化描述支撑，并在三个基准与IMO-AG-30上通过消融测量各组件。
实例化统一几何求解器Omni-Geo：一个形式语言与求解器覆盖平面、解析（含圆锥曲线）与立体几何，三类几何族共用同一解析器、条件存储、定理匹配器、方程引擎与目标检查器。 此前系统多局限于单一几何族；该工作用一套GeoLib/GeoDL声明与类型化转移契约跨域复用。 在FormalGeo7K、Conic10K、SolidFGeo三个基准上端到端评测，且同一运行时与搜索栈在Claude Sonnet 4.6与Qwen3-VL-8B-Thinking两个冻结后端下均取得跨域结果。
嵌套控制器先在外层用source-UCB在神经与符号提议源之间分配计算，再在内层用action-PUCT在已接纳动作间分配回访；消融显示固定源调度使宏平均下降、移除神经桥接动作降幅最大。 将源选择本身作为搜索决策，并区分源分配与动作回访两类分配问题。 组件消融逐项改变一个组件：固定源调度、移除神经桥接动作、移除接纳过滤、单遍形式化均在每个基准上降低准确率；搜索常数扫描显示共享设置在三个域中观测准确率最高。
在IMO-AG-30上以冻结神经后端和少于200条注册可执行模式解出21/30题，与AlphaGeometry（从零训练、100M定理—证明示例）和TongGeometry（6.7B生成辅助问题并做策略/价值微调）的专门化资源并列呈现。 展示同一接口在奥林匹克构造题设定下、以紧凑可执行几何库运行，无需参数适配。 表3以各系统原生单位记录专门化资源，将Omni-Geo的紧凑可执行理论置于同一经验语境。
启示与展望
该结果面向平面、解析（含圆锥曲线）与立体几何的基准求解，适用于使用官方题面—图示对（Conic10K为文本输入）的设定；同一运行时与搜索栈在Claude Sonnet 4.6与Qwen3-VL-8B-Thinking两个冻结后端下均成立，说明符号基底可复用。IMO-AG-30实验把同一设计扩展到奥林匹克构造题，使用少于200条注册可执行模式。对希望复用该接口的读者，附录C给出完整提示、调用接口与搜索超参数（名义600秒/题、最大深度15、三次神经扩展轮），便于在自身几何域上重建。
形式保证是相对于编译实例的条件可靠性，编译结果对原始文本与图示的保真度是另一项编译属性；返回记录中procedural类输出被单独报告且不作为证明证书。搜索常数扫描显示解析几何在该点附近相对稳定，而立体几何对外层源分配常数更敏感，这一差异在更广设定下的表现值得继续观察。进度权重为人工设定并在各基准间固定，其取值对结果的影响范围仍是开放问题。IMO-AG-30上21/30与AlphaGeometry的25/30、TongGeometry的30/30并列呈现，但各系统专门化资源以原生单位记录，跨系统比较需谨慎解读。