BiNSGPS:基于双向神经符号交互的几何问题求解
摘要
BiNSGPS 是一个框架,在多模态 LLM 顾问与符号求解器之间引入双向交互机制,用于几何问题求解。该框架允许求解器将反馈传递回顾问,以纠正错误并生成辅助假设。在 Geometry3K 和 PGPS9K 基准测试上分别取得了 90.5% 和 90.1% 的最优性能。
arXiv:2606.04648v1 公告类型:新论文
摘要:几何问题求解在人工智能领域面临独特挑战。现有方法通常分为两类范式:符号方法适应性有限,神经方法则容易产生幻觉。近期的神经符号混合方法主要依赖单向流水线,即将神经网络的输出直接输入求解器而不存在反馈机制,导致系统对早期错误十分脆弱。为打破这一单向瓶颈,我们提出 BiNSGPS——一个在 MLLM 顾问与符号求解器之间建立双向神经符号交互(BiNS)的框架。MLLM 顾问能够主动接收来自符号求解器的反馈,动态修正不一致的形式化表示或提出辅助假设,从而解决符号冲突并促成复杂推理的完成。
查看缓存全文
缓存时间: 2026/06/05 02:08
# BiNSGPS:基于双向神经符号交互的几何题求解
来源:https://arxiv.org/html/2606.04648
Qi Wang1,2, Peijie Wang1,211footnotemark:1, Fei Yin1,2, Cheng\-Lin Liu1,2 1中国科学院自动化研究所 MAIS 2中国科学院大学人工智能学院 wangqi226@mails\.ucas\.ac\.cn wangpeijie2023@ia\.ac\.cn \{fyin, liucl\}@nlpr\.ia\.ac\.cn
###### 摘要
几何题求解是人工智能领域的一项独特挑战。现有方法通常分为两类范式:符号方法(适应性有限)和神经方法(易产生幻觉)。近期的神经符号混合方法主要依赖单向流水线,将神经网络的输出送入求解器而无任何反馈,导致系统对早期错误十分脆弱。为突破这一单向瓶颈,我们提出 BiNSGPS——一个在 MLLM 顾问与符号求解器之间建立**双向神经符号交互**(BiNS)的框架。MLLM 顾问能够主动整合符号求解器的反馈,动态修正不一致的形式化表示或提出辅助假设,从而解决符号冲突并促进复杂推断。实验表明,BiNSGPS 达到了最先进的性能,在 Geometry3K 上的完成精度为 90.5%,在 PGPS9K 上为 90.1%,同时保持 96% 的逐步逻辑一致性,在推理能力与数学严谨性之间取得平衡。
BiNSGPS:基于双向神经符号交互的几何题求解
Qi Wang1,2††感谢:同等贡献。, Peijie Wang1,211footnotemark:1, Fei Yin1,2, Cheng\-Lin Liu1,2††感谢:通讯作者。1中国科学院自动化研究所 MAIS2中国科学院大学人工智能学院wangqi226@mails\.ucas\.ac\.cn wangpeijie2023@ia\.ac\.cn\{fyin, liucl\}@nlpr\.ia\.ac\.cn
参见图注图1:BiNSGPS 概览。BiNSGPS 通过迭代推理循环处理多模态输入(文本与图形)。当检测到不一致(情形 i:角度度量冲突)或缺失约束(情形 ii:梯形属性)时,MLLM 顾问触发表示修正或辅助假设生成。右侧两个示例说明了闭环反馈如何将初始尝试(标有红色警告)转化为经过验证的解答(绿色对勾)。
## 1 引言
几何题求解(GPS)是人工智能领域的典型挑战,也是评估高层次认知综合能力的严格任务Trinh等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib8)\);Wang等人\(2025b (https://arxiv.org/html/2606.04648#bib.bib10)\);Zhang等人\(2024a (https://arxiv.org/html/2606.04648#bib.bib31)\)。主流 GPS 方法传统上分为两种范式:**符号方法**和**神经方法**Zhang等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib33)\);Li等人\(2024b (https://arxiv.org/html/2606.04648#bib.bib15)\);Zhang等人\(2024c (https://arxiv.org/html/2606.04648#bib.bib38)\)。符号方法具有高精度和逻辑严谨性Lu等人\(2021 (https://arxiv.org/html/2606.04648#bib.bib12)\);Zhang等人\(2024d (https://arxiv.org/html/2606.04648#bib.bib40),2025 (https://arxiv.org/html/2606.04648#bib.bib42)\),但受制于严重的形式化瓶颈。将原始问题转化为结构化表示高度依赖人工标注,且由于符号方法对初始解析错误极为敏感,自动形式化的错误将导致系统崩溃Wu等人\(2022 (https://arxiv.org/html/2606.04648#bib.bib34)\);Gan and Yu \(2018 (https://arxiv.org/html/2606.04648#bib.bib57)\);Li等人\(2024a (https://arxiv.org/html/2606.04648#bib.bib60)\)。此外,符号系统的推理范围受限于预定义的定理规则集,难以适应多样化的几何构型Fu等人\(2025a (https://arxiv.org/html/2606.04648#bib.bib18)\);Ping等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib11)\)。相反,神经方法——从专用网络到多模态大语言模型(MLLMs)——通过直接处理多模态输入展现出更强的灵活性Li等人\(2024b (https://arxiv.org/html/2606.04648#bib.bib15)\);Gao等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib19)\);Shi等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib20)\);Chen等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib69)\);Gao等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib58)\);Zhu等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib21)\);Wang等人\(2025a (https://arxiv.org/html/2606.04648#bib.bib14)\)。然而,这些模型极易产生**幻觉**:它们常常生成表面合理但逻辑有误的推断,严重损害其数学可信度。
近年来,神经符号方法已成为一个有前景的研究方向,旨在将神经模型的多模态理解能力与符号引擎的严谨推理能力相结合Yang等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib24)\);yi chen等人\(2026 (https://arxiv.org/html/2606.04648#bib.bib70)\)。然而,现有框架主要依赖单向流水线:神经模型作为前端解析器,将多模态输入翻译成形式化表示,再送入后端符号求解器Ping等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib11)\)。这种架构存在严重缺陷:信息流严格单向传递,符号引擎被动接收可能存在缺陷的输入。在复杂几何场景中,神经形式化极易出现感知错误,而符号引擎又常受限于预定义定理集的内在不完备性。若缺乏从推理阶段"反馈"的双向机制,系统既无法修正解析幻觉,也无法在符号求解器陷入僵局时借助神经直觉来辅助推理。因此,哪怕是轻微的初始表示错误或单个缺失定理,都可能导致整个推理链的失败。
为解决上述瓶颈,我们提出 **BiNSGPS**——一个将神经符号范式重构为基于 MLLM 的智能体工具调用架构的新颖框架。我们方法的核心是**双向**神经符号交互(BiNS),它通过在 MLLM 顾问与符号求解器之间建立主动反馈循环,打破传统单向约束,实现信息的双向流动。在这一闭环系统中,符号求解器通过超图展开执行严格推理,识别逻辑不一致或推理僵局。具体而言,BiNS 使符号求解器能够生成诊断反馈,触发 MLLM 顾问修正不一致的形式化表示,或基于 MLLM 内部知识提出辅助假设,从而有效绕过预定义定理规则集的局限。如图1 (https://arxiv.org/html/2606.04648#S0.F1) 所示,MLLM 顾问能够动态纠正符号求解器识别出的感知错误,或引入外部几何直觉以打破推理僵局。大量实验表明,BiNSGPS 在实现最先进(SOTA)精度的同时,有效平衡了数学严谨性与推理灵活性。
我们的主要贡献如下:
1. **交互式修正与增强**:我们将 **BiNS** 机制引入神经符号方法,符号求解器向 MLLM 顾问提供诊断反馈,从而实现形式化错误的修正和推理的启发式增强。
2. **双向神经符号框架**:我们提出 **BiNSGPS**,将传统单向神经符号流水线重构为智能体工具调用架构。通过在 MLLM 顾问与符号求解器之间建立反馈循环,打破了传统 GPS 中固有的信息瓶颈。
3. **最先进性能**:在 Geometry3K 和 PGPS9K 上的大量评估表明,BiNSGPS 取得了新的 SOTA 性能,求解精度分别达到 90.5% 和 90.1%。BiNSGPS 还在逐步推断中确保了出色的逻辑一致性,在推理灵活性与数学严谨性之间建立了优越的平衡。
## 2 相关工作
### 2.1 几何题求解
几何题求解(GPS)是数学智能的标志性任务。现有文献大致可分为三种范式:1. **基于神经网络的方法**将 GPS 视为视觉问答任务。早期工作采用 PGPSNetZhang等人\(2022 (https://arxiv.org/html/2606.04648#bib.bib16)\) 和 LANSLi等人\(2024b (https://arxiv.org/html/2606.04648#bib.bib15)\) 等专用架构,近期工作则借助 G\-LLaVAGao等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib19)\) 和 Vision\-R1Huang等人\(2026 (https://arxiv.org/html/2606.04648#bib.bib53)\) 等 MLLMs 的推理能力。这些模型擅长灵活直觉推断,但易产生幻觉,缺乏数学证明所需的严谨性。2. **基于符号的方法**(如 InterGPSLu等人\(2021 (https://arxiv.org/html/2606.04648#bib.bib12)\)、E\-GPSWu等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib26)\))将原始输入翻译成结构化形式语言并执行推理。虽然逻辑严谨,但这些系统存在形式化瓶颈:对初始解析错误高度敏感,且缺乏处理硬编码定理之外构型的适应性。3. **神经符号方法**尝试弥合上述差距。AlphaGeometryTrinh等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib8)\) 和 AlphaGeometry2Chervonyi等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib9)\) 等近期突破性成果将语言模型与符号引擎结合,用于求解奥林匹克竞赛题。AutoGPSPing等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib11)\) 和 GeoDRLPeng等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib54)\) 等方法则利用 MLLM 组件指导定理选择或生成对齐表示。GeoparsingWang等人\(2026 (https://arxiv.org/html/2606.04648#bib.bib71)\) 通过引入统一形式语言进一步推进了感知阶段,支持平面和立体几何图形解析,使 MLLMs 能够将几何图形转化为结构化符号描述,作为下游推理的认知支架。然而,这些系统主要依赖单向流水线,符号求解器被动接收神经网络的输出。这种单向流意味着任何解析错误都无法恢复,求解器也无法"回头"向神经组件寻求帮助。相比之下,我们的 BiNSGPS 框架引入了双向交互:通过建立反馈机制,符号求解器可以提示 MLLM 修正不一致的表示并假设辅助构造,打破了以往神经符号方法的"单向"瓶颈。
### 2.2 MLLMs 用于几何推理
多模态大语言模型(MLLMs)已成为数学推理研究的焦点,MathVistaLu等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib44)\)、MATH\-VisionWang等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib23)\)、GeoEvalZhang等人\(2024b (https://arxiv.org/html/2606.04648#bib.bib39)\)、MV\-MATHWang等人\(2025a (https://arxiv.org/html/2606.04648#bib.bib14)\)、SolidGeoWang等人\(2025b (https://arxiv.org/html/2606.04648#bib.bib10)\) 和 GeoLauxFu等人\(2025b (https://arxiv.org/html/2606.04648#bib.bib46)\) 等专项基准测试彰显了其潜力。该领域研究主要沿两条并行路径展开。一条路径聚焦于监督微调和强化学习Xu等人\(2024a (https://arxiv.org/html/2606.04648#bib.bib63),b (https://arxiv.org/html/2606.04648#bib.bib64)\);Shao等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib65),2025 (https://arxiv.org/html/2606.04648#bib.bib66)\),以使模型适应几何领域,产生了 G\-LLaVAGao等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib19)\) 和 GeoGPT4VCai等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib32)\) 等模型。尽管这些模型展现出更强的直觉推断能力,但仍易受图形解析中感知错误和推理过程中逻辑幻觉的影响。另一条研究路径将 MLLMs 视为与外部工具交互以解决复杂任务的智能体Gou等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib27)\);Surís等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib35)\);Pan等人\(2023 (https://arxiv.org/html/2606.04648#bib.bib36)\)。Visual SKETCHPADHu等人\(2024 (https://arxiv.org/html/2606.04648#bib.bib49)\) 和 CODEPLOT\-COTDuan等人\(2025 (https://arxiv.org/html/2606.04648#bib.bib50)\) 等框架是这一思路的典型代表,利用辅助绘图模块或代码执行环境协助 MLLM 进行视觉分析与计算。
在本工作中,我们遵循基于智能体的范式,采用工具调用架构。在 BiNSGPS 框架中,MLLM 充当中央协调器,与专用神经网络和符号求解器进行交互。这种方式使 MLLM 能够充分利用领域专用工具的高质量输出,同时专注于策略制定与错误纠正。
## 3 方法
参见图注图2:BiNSGPS 流水线框架。**上方**:多模态表示对齐。几何图形-文本对首先进行标注,然后通过双解析器架构处理:专用神经网络提取图形结构基元,MLLM 解析文本约束。两者整合为初始逻辑形式 $\mathcal{L}$,经对齐与补全后形成完整的符号表示。**下方**:双向神经符号交互与证明生成。符号求解器构建超图进行演绎推理。当遇到不一致或推理僵局时,MLLM 顾问分析错误诊断信息,修正错误的形式化表示或提出辅助假设 $\mathcal{H}$。一旦找到解答,求解器识别最小推理子图,MLLM 随后将其翻译成人类可读的证明。
### 3.1 概述
BiNSGPS 框架如图2 (https://arxiv.org/html/2606.04648#S3.F2) 所示。BiNSGPS 是一个闭环神经符号系统,由三个主要组件构成:多模态表示对齐、符号求解器和 MLLM 顾问。系统遵循迭代执行流程,弥合神经直觉与符号严谨性之间的差距。给定几何题 $(\mathcal{D}, \mathcal{T})$,图形 $\mathcal{D}$ 和文本 $\mathcal{T}$ 首先由多模态表示对齐模块处理,生成形式化规格,即初始表示集 $\mathcal{L} = (l_1, l_2, \ldots, l_n)$,作为问题的基础几何事实。
符号求解器随后接收 $\mathcal{L}$ 进行推理。借助预定义定理规则集 $R$,求解器将推理过程建模为超图展开……相似文章
可验证的几何问题求解:求解器驱动的自动形式化与定理提出
本文介绍了 SD-GPS,一个求解器驱动的几何问题求解框架,利用求解器反馈引导的自动形式化和经过验证的定理提出,来克服神经符号系统中的瓶颈。
FormalAnalyticGeo:一个基于神经符号的多模态解析几何问题生成框架
介绍了FormalAnalyticGeo,这是一个基于神经符号的框架,用于自动生成多模态解析几何问题。它利用形式化中间表示(CDL)和LLM组件,生成了包含超过7K个经过验证的问题的AnalyticGeo7K数据集,具有高几何精度。
基于MaxSAT的反馈引导视觉语言模型解决数独
本文提出了一种神经符号方法,将MaxSAT预言机作为一致性验证器,引导视觉语言模型(VLM)解决数独谜题,从而提高逻辑一致性和求解实例数量。
SG-WAM:几何感知策略空间中的自引导世界建模
本文提出SG-WAM,一种自引导框架,用于直接在策略派生的表示空间中学习几何感知的、以动作为条件的世界模型。它在LIBERO和LIBERO-Plus基准测试上取得了最先进的成功率,在真实世界评估中超越了强基线。
BIM中几何密集型合规检查的自动化:基于图的语义推理框架
本文介绍了SGR-BIM,一种图驱动的语义推理框架,能够动态地将法规意图与BIM几何对齐,自动化几何密集型合规检查,在消防安全规范查询上达到了84.3%的准确率。