发表机构
Apodex; University of Toronto; UC Berkeley; ETH Zürich; Meta FAIR（Apodex; 多伦多大学; 加州大学伯克利分校; 苏黎世联邦理工学院; Meta FAIR）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出Euclid-Omni统一神经符号框架，结合形式几何系统与LLMs、VLMs，核心为符号几何求解器Euclidea，生成合成数据训练模型，在竞赛级几何问题上性能优异且成本更低。
AI 中文摘要
欧氏几何是AI推理的重要测试平台，因其要求结合直观的图形理解、公理演绎与代数计算能力。然而现有方法通常仅能处理部分能力，或难以应对竞赛级问题。本文提出Euclid-Omni，这是一个将形式几何系统与大语言模型（LLMs）、视觉语言模型（VLMs）相结合的统一神经符号框架，可处理形式语言与自然语言中的计算类和证明类问题，难度达到奥林匹克竞赛级别。其核心是开发了通用符号几何求解器Euclidea，该求解器通过演绎推理与代数计算自动生成推理步骤。在此基础上，本文开发了数据生成流水线，可合成符号问题与解答、渲染图形并将其转换为自然语言，生成大规模、多样化的数据集，用于在多种推理场景下训练LLMs与VLMs。实验表明，在本文合成数据上训练的VLMs在计算任务上表现优异；结合Euclidea的LLMs在奥林匹克竞赛级证明问题上的性能可与最先进系统相媲美，且使用的计算资源与训练数据量仅为后者的几个数量级。代码与脚本已公开于此httpsURL。
英文摘要
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
