核心发现
方法论
框架核心是Python形式系统Euclidea：以点为原语，用度量关系和图示拓扑关系表达问题；SQL演绎数据库穷举规则闭包，SymPy代数系统处理线性、对数线性及复杂方程。Euclid-Omni进一步用构造规则生成符号题、坐标图、自然语言与证明轨迹，分别训练VLM计算模型和让LLM预测辅助构造。
关键结果
- Euclidea在Geometry3K的601题中解决595题（约99%），超过PyEuclid的567题和Inter-GPS的426题；在JGEX-AG-231上解决207/231题，在IMO-AG-30上解决16/30题。
- 采用20K合成样本训练的模型在GeoQA、Geometry3K、MathVista和MathVerse上分别达到76.6%、61.0%、74.7%和51.0%；相比Qwen2.5-VL-7B基线，四项均有提升。
- 消融显示协同机制不可替代：去除代数系统后仅解决Geometry3K的1题、JGEX的74题；去除演绎数据库后分别为36题和2题，说明单一推理范式明显不足。
研究意义
论文把几何计算、竞赛证明、图像理解、自然语言和形式语言放入同一框架，回应了现有系统任务专门化、数据规模小、证明不可解释等问题。它展示了一个重要方向：神经模型负责感知、语言表达和候选构造，符号系统负责可验证推导。公开代码与生成脚本也降低了研究复现门槛，有助于教育型数学AI和可靠推理研究。
技术贡献
Euclidea将演绎数据库与SymPy代数求解器交替运行，并用SQL表连接枚举适用定理。角度、长度关系可写成Ax=b并用Gaussian elimination求解；比例关系转为log-linear系统；证明轨迹则通过稀疏优化min_z||z||_t、约束[A|b]^Tz=c筛选最小支撑集。数据管线还统一了构造、渲染、模板翻译和难度控制。
新颖性
相较只做角度证明的AlphaGeometry、只做计算的Inter-GPS，以及专注形式证明的DD+AR，Euclid-Omni试图首次在公开管线中贯通视觉、自然语言、计算和证明。关键新意不是单个定理，而是以Euclidean Elements式关系表示连接演绎规则、方程求解和可读证明。
局限性
- 剩余失败包括无法被当前语言形式化、点数过多导致搜索空间和超时，以及需要额外辅助构造的问题；系统并非覆盖所有奥赛几何。
- 自然语言数据依赖人工验证模板和LLM改写，可能限制表达多样性；论文给出的实验摘录也未提供完整训练超参数、规模消融和所有基准结果。
未来方向
作者提出将管线扩展到自动形式化、图形生成和图形理解。后续可加强辅助构造搜索、处理更大图、引入更强的视觉解析与不确定性校验，并系统研究合成数据与真实题目之间的分布差异。
AI 总览摘要
平面几何同时要求看懂图形、使用公理定理并完成代数计算，因此一直是检验人工智能推理能力的理想场景。既有IMO系统擅长证明却不善计算，计算系统又常停留在基础题；公开数据集规模小、难度分层不足，也限制了大模型训练。
Euclid-Omni提出统一的神经符号框架，核心是Euclidea。它把点、长度、角度、共线和同侧关系存入形式状态，用SQL演绎数据库不断应用规则，再由SymPy处理方程。Euclid-Omni在此基础上随机执行尺规构造，采样坐标，绘制Matplotlib图形，并通过模板与LLM生成自然语言题目和解答。神经模型负责图像、语言及辅助构造，符号引擎负责验证。
结果显示，Euclidea解决Geometry3K的595/601题、JGEX-AG-231的207/231题和IMO-AG-30的16/30题。仅用20K合成样本训练的VLM在GeoQA、Geometry3K、MathVista、MathVerse上达到76.6%、61.0%、74.7%、51.0%。不过，复杂辅助构造、超大搜索空间和形式化覆盖仍是瓶颈。论文的价值在于提供了可复现的统一基础设施，而不是宣称几何推理已经完全解决。
深度分析
研究背景
几何AI经历了经典自动定理证明、代数方法和神经符号方法三个阶段。Gröbner basis、Wu’s method计算能力强但证明难读；NGS、Inter-GPS面向计算；LeanEuclid、DD+AR、AlphaGeometry偏向证明。GeoQA、Geometry3K、JGEX-AG-231和IMO-AG-30覆盖不同任务，但数据和统一系统仍不足。
核心问题
系统必须同时理解自然语言与图形，区分显式度量事实和隐含拓扑事实，完成演绎、代数消元及辅助构造。传统full-angle表示难以区分角与补角，不适合计算；纯神经链式推理又可能幻觉，难以验证。
核心创新
第一，Euclidea用Euclid’s Elements式关系统一计算与证明。第二，演绎数据库和代数系统交替扩展状态。第三，使用稀疏优化生成可追溯、较人类化的证明。第四，Euclid-Omni以构造规则、渲染器和模板翻译器生成形式、图像、自然语言配对数据，并可调节任务与难度。
方法详解
- �� 输入：点及其Metric/Diagrammatic关系。
- �� 演绎：SQL数据库匹配Angle Bisector Theorem、等腰三角形等规则，直到闭包。
- �� 代数：将角度和长度方程写为Ax=b，用Gaussian elimination；比例关系转为log-linear形式，复杂式用代入化简。
- �� 追踪：用PySCIPOpt寻找稀疏支持方程，构成依赖图并后序遍历。
- �� 生成：执行construct foot、construct square等规则，采样坐标、渲染图形、实例化模板，再由LLM改写。
实验设计
符号实验使用Geometry3K（601题）、JGEX-AG-231（231题）和IMO-AG-30（30题），与Inter-GPS、PyEuclid、DD+AR、Newclid比较；600秒限时，计算误差阈值为2%。VLM实验使用10K训练实例的设定摘要及表2中的20K模型结果，评估GeoQA、Geometry3K、MathVista、MathVerse，并进行去除代数或演绎模块的消融。
结果分析
Euclidea达到595、207、16题，分别对应三个基准；PyEuclid为567、202，DD+AR为198、14，Newclid为188、14。VLM的76.6/61.0/74.7/51.0%超过Qwen2.5-VL-7B的69.4/56.4/72.2/44.1%。模块消融证明两种推理必须结合。
应用场景
可用于几何作业辅导、自动生成分层练习、图形化解题反馈和形式证明验证。教师可配置构造规则与目标；研究者可用公开脚本生成视觉—语言—符号对齐数据。部署前仍需检查模板正确性、图形解析和超时情况。
局限与展望
系统依赖预定义形式语言、规则库和构造库，未知定理或非标准图形可能无法表达。点数增加会造成组合搜索和超时；需要辅助构造的奥赛题仍是主要失败源。合成图与真实教材图之间可能存在分布差异，且给定摘录未披露完整训练成本、超参数和统计显著性。
通俗解读 非专业人士也能看懂
把Euclid-Omni想成一间解题工厂。传送带先把题目中的点、线和圆登记成标签；质检员检查哪些东西相等、垂直或在同一直线上。规则工人像经验丰富的老师，看到“两个半径相等”就贴上“等腰三角形”标签。计算工人再把长度和角度写成方程，用消元找到答案。最后，记录员从答案倒着查每一步，删掉无用材料，生成一份能读懂的解答。
工厂还能自己出题：先按尺规步骤搭图，随机选择坐标，再画图、写自然语言，并保留标准答案。这样，模型不只背题，而是练习从不同入口完成同一任务。实验中，这家工厂解决了Geometry3K的595道题，并帮助视觉模型在四个基准上取得较高准确率。
简单解释 像给14岁少年讲一样
想象你在玩一个几何解谜游戏。屏幕上有点、线和圆，你要回答“某条线多长”或证明“这两个角相等”。普通聊天机器人可能会把步骤说得很像真的，却偷偷算错。Euclid-Omni像一个会核对答案的队友：语言模型负责读题、看图和提出“要不要画一条辅助线”，Euclidea则像裁判，逐条检查定理和计算。
它有两种技能。第一种像整理卡牌：把“相等”“垂直”“共线”等事实放进盒子，再不断套用规则。第二种像解方程：把角度和长度变成数学式，用消元找出未知数。两种技能互相提供线索，所以比只会背规则或只会算式更强。
它还会自己生成练习题：随机搭建图形，画出图片，再写成文字，并保存推理过程。结果很厉害：Geometry3K中601题解决595题，IMO-AG-30中解决16题。可是它也会卡住，尤其是图太复杂、点太多，或者必须猜出很巧妙的辅助线时。
术语表
Euclidea（形式几何求解器）
以点和关系为基础的Python几何系统。它结合规则推理与代数求解，并输出可追踪证明。
Euclid-Omni的符号核心。
Deductive database（演绎数据库）
保存事实、等价类和定理条件的数据库。SQL表连接用于寻找可应用规则。
负责不断扩展关系闭包。
Gaussian elimination（高斯消元）
把线性方程组化简并求出变量关系的方法。论文将角度、长度系统写成Ax=b。
用于计算和证明中的代数推理。
Neuro-symbolic（神经符号）
神经模型处理感知和语言，符号程序执行可验证推理。二者分工降低幻觉风险。
描述LLM、VLM与Euclidea的整体架构。
Auxiliary construction（辅助构造）
为证明目标而额外添加、但不属于原始图形的点或线。它通常是奥赛证明最困难的步骤。
LLM训练目标之一。
开放问题 这项研究留下的未解疑问
- 1 如何让系统自动发现超出现有构造库的辅助线，并在巨大搜索空间中保持可接受速度，仍未解决。
- 2 合成图形与真实教材、手绘图之间存在分布差异；需要更强视觉解析和跨域评测。
- 3 论文摘录未给出完整训练配置、数据规模消融及统计显著性，难以全面判断效率优势。
应用场景
近期应用
智能几何辅导
教育平台可输入题目和图形，由VLM读图、LLM组织语言，再调用Euclidea验证每一步。教师可按构造规则和目标类型生成分层练习，并获得可检查的证明，而非不可解释答案。
自动题库与证明检查
研究者或教材团队可用公开生成脚本批量创建形式题、自然语言题和图形。系统能筛选目标的最小支持构造，减少人工编题与标注成本，同时保留标准推理轨迹。
远期愿景
通用数学推理基础设施
若扩展定理库、视觉解析和辅助构造搜索，该框架可成为连接教材、竞赛数学与形式化证明的基础设施。主要障碍是开放世界知识、真实图形噪声和计算效率。
原文摘要
Euclidean geometry is a compelling testbed for AI reasoning, as it demands the combination of intuitive diagram understanding, axiomatic deduction, and algebraic computation. Yet, existing approaches typically address only a subset of these abilities or struggle with competition-level problems. We introduce \textit{Euclid-Omni}, a unified neuro-symbolic framework that couples a formal geometry system with Large Language Models (LLMs) and Vision-Language Models (VLMs) to tackle both calculation- and proving-style problems, in formal and natural languages, up to Olympiad-level difficulty. At its core, we develop \textit{Euclidea}, a versatile symbolic geometry solver that automatically generates reasoning steps through deductive inference and algebraic computation. Building on this, we develop a data-generation pipeline that synthesizes symbolic problems and solutions, renders diagrams, and translates them into natural language, producing large-scale, diverse datasets for training LLMs and VLMs across a wide range of reasoning settings. Experiments show that VLMs trained on our synthetic data achieve superior performance on calculation tasks, and that LLMs combined with \textit{Euclidea} are competitive with state-of-the-art systems on Olympiad-level proving problems, despite using orders of magnitude less compute and training data. Code and scripts are publicly available at https://github.com/20171130/Euclid-Omni