Euclid-Omni : 用于平面几何的统一神经符号框架

arXiv cs.AI 论文
neuro-symbolic plane-geometry llm vlm reasoning automated-proving

摘要

Euclid-Omni 是一个神经符号框架，它整合了大型语言模型（LLMs）、视觉语言模型（VLMs）和一个符号求解器，用于处理从计算到奥林匹克级别的证明的平面几何问题，并使用合成数据生成进行训练。

arXiv:2608.14585v1 公告类型：新 摘要：欧几里得几何是人工智能推理的一个引人注目的测试平台，因为它需要结合直觉的图表理解、公理化推理和代数计算。然而，现有方法通常只处理这些能力的一个子集，或者在竞赛级别问题上遇到困难。我们介绍了 \textit{Euclid-Omni}，一个统一的神经符号框架，它将形式化几何系统与大型语言模型（LLMs）和视觉语言模型（VLMs）相结合，以处理从计算到证明式的问题，使用形式化和自然语言，直至奥林匹克级别难度。其核心是我们开发了 \textit{Euclidea}，一个多功能的符号几何求解器，它通过演绎推理和代数计算自动生成推理步骤。在此基础上，我们开发了一个数据生成管道，该管道合成符号问题和解决方案，渲染图表，并将它们翻译成自然语言，生成大规模、多样化的数据集，用于在广泛的推理环境中训练 LLMs 和 VLMs。实验表明，在我们合成数据上训练的 VLMs 在计算任务上取得了优异性能，并且结合了 \textit{Euclidea} 的 LLMs 在奥林匹克级别证明问题上与最先进的系统具有竞争力，尽管使用了几个数量级更少的计算和训练数据。代码和脚本在 https://github.com/20171130/Euclid-Omni 公开提供。
查看原文
查看缓存全文

缓存时间: 2026/08/18 09:48 

# 平面几何的统一神经符号框架  
来源：https://arxiv.org/html/2608.14585  
赵宇¹²，毕杭瑞²¹（脚注1:等同贡献），张有源²，马文杰³  
李泽南⁴，张兆雷²，司旭杰²，杨凯宇¹  
¹Apodex，²多伦多大学，³加州大学伯克利分校，⁴苏黎世联邦理工学院  
[email protected]，[email protected]，[email protected]，[email protected]，[email protected]，[email protected]，[email protected]  

###### 摘要  
欧几里得几何是人工智能推理的绝佳试验场，因为它需要结合直观的图表理解、公理化演绎和代数计算。然而，现有方法通常只处理这些能力的子集，或难以解决竞赛级问题。我们提出 **Euclid-Omni**，一个统一的神经符号框架，将形式化几何系统与大型语言模型（LLMs）和视觉语言模型（VLMs）相结合，以形式语言和自然语言处理计算与证明类问题，难度可达奥林匹克水平。其核心是开发 **Euclidea**，一个多功能符号几何求解器，能够通过演绎推理和代数计算自动生成推理步骤。在此基础上，我们构建了一个数据生成流程，用于合成符号问题与解答、渲染图表并将其转化为自然语言，生成大规模、多样化的数据集，用于训练 LLMs 和 VLMs 以适应广泛的推理场景。实验表明，在合成数据上训练的 VLMs 在计算任务中表现优异，而结合 **Euclidea** 的 LLMs 在奥林匹克水平的证明问题上与最先进的系统相当，尽管使用的计算资源和训练数据量少几个数量级。代码和脚本在 https://github.com/20171130/Euclid-Omni 公开。  

## 1 引言  
平面几何作为数学教育的基石已有两千多年历史，自欧几里得的《几何原本》以来，问题范围从基础课堂练习到国际数学奥林匹克（IMO）挑战。它在人工智能史上也占有特殊地位，启发了最早的一些自动定理证明符号系统 [13]。随着大型语言模型（LLMs）和视觉语言模型（VLMs）的兴起，平面几何再次成为探究和提升机器推理能力的热门平台 [45, 31, 60]，最先进的系统 [57, 11, 8] 已达到 IMO 金牌选手水平，标志着自动几何推理的新里程碑。然而，这些进展在范围和可及性方面仍有限制。  

在范围上，IMO 级别的系统几乎专门针对竞赛式定理证明，对计算类问题所需的代数计算支持甚少，尽管此类问题在平面几何中同样常见。它们产生的解决方案往往远离人类推理方式，很少涉及自然语言或视觉图表，限制了其在教育场景中的实用性。而针对计算任务的互补性工作则面临相反的问题：它们仅覆盖少量定理，且远未达到竞赛难度 [6, 30, 7]。  

在可及性方面，训练 IMO 级别的系统需要巨大的计算资源，且至今没有系统公开其数据生成流程或训练数据。公共数据集则规模较小、缺乏多样性，且难度分层不佳 [6, 30, 4, 7]，不足以大规模训练现代 LLMs 和 VLMs。总体而言，这些差距使现有方法难以作为几何推理研究的通用基础。  

为弥合这一差距，我们提出 **Euclid-Omni**，一个面向广泛几何推理场景的统一神经符号框架。其核心是 **Euclidea**，一个符号引擎，通过穷举应用可容许推理规则直至达到演绎闭包。现有的 IMO 级别系统大多基于全角符号 [14]，这虽便于某些竞赛式证明，但无法区分一个角或弧与其补角，因此不适合计算问题。相反，**Euclidea** 将其公理基础直接建立在欧几里得《几何原本》[1] 上，这使得它能够在单一框架内处理计算和证明任务，并产生与学校几何教学中相近的推理步骤。  

我们在 Geometry3K [30]、JGEX-AG-231 [45] 和 IMO-AG-30 [45] 上评估了 **Euclidea**，这些数据集覆盖了计算和证明任务，发现其解决的问题数量多于现有形式化几何系统，且产生的解决方案更易于人类阅读。  

基于 **Euclidea**，我们的第二个贡献是用于训练 LLMs 和 VLMs 的多功能数据生成流程。该流程生成涵盖文本与视觉模态、形式与自然语言、计算与证明任务的几何问题。它高度可配置，因此生成的数据集可根据特定训练目标和难度级别（从基础问题到 IMO 级别挑战）进行定制。  

为评估该流程，我们使用其合成数据训练了两种处于几何推理谱系两端的模型：（i）具有图表可视化和自然语言描述的多模态几何计算；（ii）奥林匹克级别的形式定理证明。在第一种场景中，我们在 GeoQA [6]、Geometry3K [30]、MathVista [31] 和 MathVerse [60] 上评估了在合成数据上训练的 VLMs；尽管使用的训练数据量远少于先前工作，我们的模型在这些基准测试中达到或超越了现有方法。在第二种场景中，我们在 JGEX-AG-231 [45] 和 IMO-AG-30 [45] 上评估了一个在合成数据上训练的 LLM，其持续优于商业 LLM 基线，并与最先进的系统 [45] 竞争力相当，而使用的计算资源和训练数据量少几个数量级。  

## 2 相关工作  
**符号方法。** 经典的形式化几何求解器遵循两种主要范式 [13]：合成演绎和代数计算。合成方法（如演绎数据库方法 [15, 56]）采用前向链式推理系统地应用几何规则并推导新事实，但难以处理需要复杂代数操作的问题。代数方法（包括 Gröbner 基 [26] 和吴方法 [50]）将几何关系编码为多项式方程并用代数方式求解，具有强大的推理能力，但产生的证明通常难以解释。混合系统（如用于计算的 NGS [6] 和 Inter-GPS [30]，用于定理证明的 LeanEuclid [37] 和 DD+AR [45]）试图结合演绎和代数推理，但仍在特定任务类型上专业化，通用性有限。其他框架（如 FormalGeo [62] 和 PyEuclid [28]）追求统一方法，但在高效扩展到奥林匹克级别的问题上仍面临挑战。  

**数据集与基准。** 许多几何数据集源自教科书、练习和竞赛，其中的问题与人工构建的符号形式配对 [4, 7, 59, 62]。例如计算导向的数据集 GeoQA [6] 和 Geometry3K [30]，以及定理证明数据集 UniGeo [7]、JGEX-AG-231 [45] 和 IMO-AG-30 [45]。由于人工标注成本高昂，这些资源规模相对较小。为扩大覆盖范围，近期工作 [21, 61] 利用 LLMs 和 VLMs 通过增强现有问题生成更大的数据集，但其多样性仍受底层来源限制。同时，若干合成流程 [25, 17, 39, 19, 9, 49] 使用基本几何图元和谓词生成符号问题，但生成的实例在难度和种类上始终受限。其他基准 [58, 46, 42, 53]（包括 MathVista [31] 和 MathVerse [60]）收集了各种自然语言几何问题以评估 VLMs 的推理能力。除了求解几何问题，辅助数据集也被引入用于相关任务，如形式化 [37]、图表解析 [22]、图表理解 [23] 和几何图像生成 [3]。  

**基于学习的方法。** LLMs 和 VLMs 的最新进展催生了一波基于学习的几何推理方法 [65, 32]。一个方向采用在符号表示上操作的神经符号方法 [6, 30, 7, 40, 52, 21, 48, 45, 57, 18, 64, 63, 41]：这些方法利用 LLMs 或 VLMs 生成符号形式的求解步骤，并将执行委托给求解器，从而确保正确性和可解释性。例如，Inter-GPS [30] 预测程序序列以计算数值量，而 AlphaGeometry [45] 预测辅助构造并将其与符号引擎集成用于定理证明。此类系统能够实现忠实推理，但严重依赖求解器的设计和符号覆盖范围。相比之下，纯神经方法直接用自然语言推理 [21, 54, 17, 49]，通常针对具有可验证数值答案的计算问题，并使用思维链推理 [47] 产生逐步解决方案。尽管对简单问题有效，但这些方法常产生幻觉中间步骤且难以验证，限制了其在定理证明和其他复杂场景中的可靠性。一些方法 [38, 29, 27, 51, 12] 也旨在提升 VLMs 在几何推理中的视觉感知和图表理解能力。然而，目前仍缺乏统一框架来训练 LLMs 和 VLMs，以灵活支持形式语言和自然语言中的多样化几何任务。  

## 3 方法  
见图注  
图 1：**Euclidea** 求解证明类几何问题的示例。  

### 3.1 Euclidea  
**Euclidea** 是一个基于 Python 的形式化平面几何系统，编码文本和图表中的信息。其推理引擎结合了演绎推理和代数计算。**Euclidea** 的概览如图 1 所示。  

**问题形式化。** **Euclidea** 通过结合两种成熟的几何表示方法 [15, 1]（附录 A.1）来形式化平面几何。它将点作为基本图元，所有其他对象（如直线、三角形）均用点定义 [15]。图表被形式化为一组点及其关系，这些关系分为两类 [1]：  
- • **度量关系** 编码定量属性，如 **Perpendicular(a,b,c,d)**（ab⊥cd）或 **Angle(a,b,c)=π/2**（∠abc=90°），包括关于长度、角度、比率和面积等几何量的代数方程。  
- • **图表关系** 捕获可直接从图表读出的拓扑配置，如 **SameSide(a,b,c,d)**（点 a 和 b 位于直线 cd 的同侧）。  
与人类推理类似，度量关系必须明确陈述——要么由

相似文章