FormalAnalyticGeo：一个基于神经符号的多模态解析几何问题生成框架

# FormalAnalyticGeo：一种基于神经符号的多模态解析几何问题生成框架

来源：https://arxiv.org/html/2607.12982

###### 摘要。随着多模态大语言模型（MLLMs）的快速发展，数学推理取得了显著进展，但解析几何仍然是一个尚未充分探索的领域，主要原因是标注样本的匮乏。现有的图表生成方法在处理解析几何时存在困难：模板方法无法处理约束驱动的布局，而生成模型缺乏精确渲染带有标注的圆锥曲线的几何精度。我们提出FormalAnalyticGeo，一个用于全自动生成多模态解析几何问题的可扩展框架。利用形式语言的严谨性，我们围绕CDL（条件描述语言）设计框架，这是一种形式化中间表示，通过有符号距离场（SDF）引擎将自由形式的问题文本与精确的图表渲染连接起来。该框架依次使用四个专门的LLM组件：Generator生成多样化的解析几何问题，Formalizer将每个问题转换为CDL以进行基于SDF的渲染，Measurer通过对渲染图进行基于视觉的测量来提取真实答案，以及Quality Verifier在三个阶段检查输出。来自Quality Verifier的结构化反馈驱动自动重试，形成一个闭环，彻底消除人工标注的需求。大规模应用FormalAnalyticGeo产生了AnalyticGeo7K，一个包含超过7K个经过验证的多模态问题的数据集，每个问题都配有对齐的文本、图表、形式化注释和真实答案。实验表明，生成的问题的中位真实相对误差为0.70%，82.3%的答案落在精确符号解的5%以内。我们的框架和数据集将公开发布。††版权声明：无{NoHyper}††脚注：西交利物浦大学 *同等贡献。†通讯作者：[email protected]

## 1. 引言

多模态大语言模型在数学推理方面展现了令人印象深刻的性能。然而，现有的大多数多模态数学推理研究主要集中于初等平面几何和立体几何，使得解析几何成为一个很大程度上未被探索的领域，而对视觉图表和复杂代数结构的联合理解能力仍然是一个相当大的挑战，它要求对方程、坐标系、包括圆锥曲线在内的几何图形，以及它们之间复杂的空间关系有综合性的理解。尽管解析几何在教育和标准化考试中都很重要，但MLLMs对其的多模态理解仍然在很大程度上未被探索，部分原因是现有的几何基准只处理平面几何，而唯一的大规模圆锥曲线资源（Conic10K（Wu等人，2023 (https://arxiv.org/html/2607.12982#bib.bib1)））纯粹是基于文本的。因此，自动化数据生成至关重要，然而为解析几何构建一个可靠的生成框架面临着现有方法尚未解决的方法论挑战。

参见图1的说明。图1：同一解析几何问题的图表生成。(a) ChatGPT：圆未使用焦距作为直径，且点P在圆上但不在双曲线上。(b) Nano Banana：输出在几何上毫无意义。(c) Gemini 3 Pro：曲线扭曲，点放置不准确。(d) 我们的方法：具有精确坐标到像素映射的几何精确渲染，可直接进行真实答案的视觉测量。

我们识别出三个这样的挑战。

**(i) 表示鸿沟。** 生成多模态问题需要一种形式化表示，该表示既能捕捉代数关系，又能捕捉渲染图表所需的几何构造。现有的几何形式体系（Inter-GPS（Lu等人，2021 (https://arxiv.org/html/2607.12982#bib.bib2)），FormalGeo（Zhang等人，2024d (https://arxiv.org/html/2607.12982#bib.bib3)））针对平面几何，无法表达坐标系或圆锥曲线；Conic10K（Wu等人，2023 (https://arxiv.org/html/2607.12982#bib.bib1)）的断言逻辑编码了代数关系，但缺乏渲染所需的构造原语。

**(ii) 渲染鸿沟。** 解析几何图表涉及嵌入在坐标系中的由代数定义的曲线。现有工具如GeoGPT4V（Cai等人，2024 (https://arxiv.org/html/2607.12982#bib.bib4)）仅限于欧几里得构造；MAVIS（Zhang等人，2024c (https://arxiv.org/html/2607.12982#bib.bib13)）涵盖解析几何，但缺乏形式化的文本-图表验证。传统的绘图库要求所有位置预先计算，没有提供约束驱动布局的机制。

**(iii) 验证鸿沟。** 现有的生成方法是单次通过的，接受输出而不进行跨阶段验证；任何阶段的错误都会未被检测地传播到最终数据集中。

我们提出FormalAnalyticGeo，一个可扩展的框架，通过形式语言解决所有三个挑战。为了弥合*表示鸿沟*，我们设计了CDL（条件描述语言），一种形式化中间表示，既能捕捉代数关系又能捕捉几何构造，实现自动一致性检查。为了弥合*渲染鸿沟*，我们开发了一个基于SDF的渲染引擎，将CDL程序编译成可微分的Signed Distance Fields，统一了约束求解和图表渲染，使得欠定位置通过梯度下降得到解决。为了弥合*验证鸿沟*，一个Quality Verifier在三个门控位置检查每个阶段的输出，并返回结构化反馈以进行自动重试，形成一个闭环，彻底消除人工标注的需求。该框架包括四个阶段：Generator生成多样化问题，Formalizer将每个问题翻译成CDL，SDF引擎渲染图表，以及Measurer通过基于视觉的测量从渲染图中提取真实答案。大规模应用FormalAnalyticGeo产生了超过7K个经过验证的问题，每个问题都包含一个自然语言问题、一张标准化图表、一个CDL注释和一个通过视觉提取的真实答案，中位相对误差为0.70%。我们的主要贡献如下：

- •一个闭环生成框架：FormalAnalyticGeo将多模态解析几何数据生成分解为由形式语言连接的专门阶段，并通过反馈驱动的质量门控消除了对人工标注的需求。
- •一种解析几何形式语言：CDL连接了自然语言问题描述和几何渲染，实现了自动句法验证和完备性检查。
- •一个基于SDF的渲染引擎：SDF Engine将CDL编译成可微分的Signed Distance Fields，统一了约束求解和图表渲染，以实现精确的解析曲线。
- •一个大规模多模态数据集：作为该框架的产物，AnalyticGeo7k涵盖了超过7K个经过验证的问题，并附有验证每个组件的消融研究。
- •全面的实证分析：我们对8个最先进的模型进行了全面的实验，并为推进多模态空间和数学推理提供了可操作的见解。

## 2. 相关工作

我们回顾三个领域的相关工作：多模态数学推理基准、几何数据生成以及多代理系统和工具使用。

### 2.1. 多模态数学推理基准

最近的基准推动了多模态数学推理的快速进展。MathVista（Lu等人，2024 (https://arxiv.org/html/2607.12982#bib.bib18)）将28个现有数据集整合成一个包含6,141个问题的套件，并显示GPT-4V（OpenAI，2024a (https://arxiv.org/html/2607.12982#bib.bib20)）仅达到49.9%，而人类为60.3%。MathVerse（Zhang等人，2024b (https://arxiv.org/html/2607.12982#bib.bib17)）进一步揭示，一些MLLMs在隐藏图表时表现*更好*，表明模型经常忽略视觉内容。MATH-Vision（Wang等人，2024 (https://arxiv.org/html/2607.12982#bib.bib16)）将此扩展到涵盖16个学科（包括解析几何）的3,040个竞赛级问题，GPT-4V（OpenAI，2024a (https://arxiv.org/html/2607.12982#bib.bib20)）仅得分23.98%。DynaMath（Zou等人，2024 (https://arxiv.org/html/2607.12982#bib.bib19)）从501个种子问题构建了5,010个变体，以评估VLM在系统性视觉扰动下的鲁棒性。对于平面几何，GeoQA（Chen等人，2021 (https://arxiv.org/html/2607.12982#bib.bib5)）、UniGeo（Chen等人，2022 (https://arxiv.org/html/2607.12982#bib.bib29)）、Geometry3K（Lu等人，2021 (https://arxiv.org/html/2607.12982#bib.bib2)）和PGPS9K（Zhang等人，2023 (https://arxiv.org/html/2607.12982#bib.bib14)）共同提供了超过30,000个专注于欧几里得构造（三角形、圆和四边形）的问题，并附有符号注释和程序解决方案。解析几何仍然很大程度上未被覆盖。GeoEval（Zhang等人，2024a (https://arxiv.org/html/2607.12982#bib.bib15)）明确包含了解析几何，但在其语料库中占比不到1%。000GeoEval在总共5,050个问题中包含28个解析几何问题。Conic10K（Wu等人，2023 (https://arxiv.org/html/2607.12982#bib.bib1)）是唯一的大规模圆锥曲线数据集（10,861个问题），具有形式化的AL注释和多步推理链，但它纯粹是基于文本的：它既不提供渲染图表，也不提供多模态评估协议。FormalAnalyticGeo直接填补了这一空白，提供了一个无需注释的生成框架，为每个问题配对一个标准化的、基于SDF渲染的图表。

### 2.2. 几何数据生成

自动化几何数据生成已有几种形式。AlphaGeometry（Trinh等人，2024 (https://arxiv.org/html/2607.12982#bib.bib12)）通过结合神经语言模型与符号演绎引擎（DDAR）合成了1亿个证明轨迹，在IMO平面几何问题上达到了金牌水平的表现。R-Co（Linger等人，2025 (https://arxiv.org/html/2607.12982#bib.bib21)）提出了一种两阶段的前向-反向流水线，首先生成图表描述，然后从中推导出问题。这些方法局限于欧几里得证明任务，并且不产生适合代数或度量推理的多模态对。最近的工作直接瞄准多模态几何数据。GeoGPT4V（Cai等人，2024 (https://arxiv.org/html/2607.12982#bib.bib4)）使用GPT-4（OpenAI，2024a (https://arxiv.org/html/2607.12982#bib.bib20)）和GPT-4V（OpenAI，2024a (https://arxiv.org/html/2607.12982#bib.bib20)）配合Wolfram Alpha生成了4.9K个平面几何问题及其图表图像。G-LLaVA（Gao等人，2025 (https://arxiv.org/html/2607.12982#bib.bib11)）将形式化逻辑表示转换为Geo170K（Gao等人，2025 (https://arxiv.org/html/2607.12982#bib.bib11)）多模态对，而TrustGeoGen（Fu等人，2026 (https://arxiv.org/html/2607.12982#bib.bib22)）为欧几里得几何数据引擎引入了形式化验证保证。NeSyGeo（Wu等人，2025 (https://arxiv.org/html/2607.12982#bib.bib10)）提出了一个神经符号框架，定义了一个实体-属性-关系DSL，并结合符号构造与基于LLM的问题生成，合成了10万个平面几何标题和推理样本。AutoGeo（Huang等人，2025 (https://arxiv.org/html/2607.12982#bib.bib9)）以及同期的工作Socratic-Geo（Jiao等人，2026 (https://arxiv.org/html/2607.12982#bib.bib8)）进一步展示了平面几何图表合成的多智能体流水线。尽管取得了进步，所有这些系统都专门针对欧几里得或平面几何。

几何形式语言和形式化方法支撑着渲染和推理流水线。Inter-GPS（Lu等人，2021 (https://arxiv.org/html/2607.12982#bib.bib2)）定义了91个用于平面图形逻辑形式的几何谓词；FormalGeo（Zhang等人，2024d (https://arxiv.org/html/2607.12982#bib.bib3)）将其扩展到88个谓词和196个定理。AutoGPS（Ping等人，2026 (https://arxiv.org/html/2607.12982#bib.bib26)）引入了一个多模态问题形式化器，从几何图表和文本中提取形式化表示，馈送给演绎符号推理器进行可解释的、逐步的问题求解。Conic10K（Wu等人，2023 (https://arxiv.org/html/2607.12982#bib.bib1)）的AL使用90个算子形式化了圆锥曲线问题，但AL只编码了代数关系，缺乏渲染图表所需的几何构造信息（例如，明确的点位置、交点、切线）。我们的CDL将AL扩展了构造原语，以驱动基于SDF的渲染。据我们所知，没有先前的工作解决过多模态基准的解析几何数据生成问题。

### 2.3. LLM代理与工具使用

基于LLM的代理，以迭代感知、推理和行动为特征，已成为复杂任务自动化的主导范式。ReAct（Yao等人，2023 (https://arxiv.org/html/2607.12982#bib.bib7)）框架将代理行为结构化为交错的推理轨迹和工具调用动作，将语言模型输出基于外部观察。多代理平台如AutoGen（Wu等人，2024 (https://arxiv.org/html/2607.12982#bib.bib23)）和MetaGPT（Hong等人，2024 (https://arxiv.org/html/2607.12982#bib.bib24)）将其扩展到协作流水线，其中具有不同角色的专门代理协调工作，以解决单个模型能力之外的任务。

工具增强的推理对于需要基于计算的任务尤为关键。Toolformer（Schick等人，2023 (https://arxiv.org/html/2607.12982#bib.bib28)）证明了LLM可以自主学习在适当位置调用外部API（计算器、搜索引擎）。在多代理数据合成中，MATRIX（Tang等人，2025 (https://arxiv.org/html/2607.12982#bib.bib27)）和AgenticMath（Liu等人，2026 (https://arxiv.org/html/2607.12982#bib.bib25)）表明，专门的生成器-验证器流水线比单模型生成产生更高质量的训练数据。FormalAnalyticGeo采用这种多组件范式，并增加了领域特定的质量层。与通用框架不同，我们的框架嵌入了一个专用的Quality Verifier，配备了包括CDL语法验证、符号可解性检查和跨组件答案验证在内的几何特定工具，应用于三个门控位置。这种设计提供了闭环反馈，驱动上游重试，直到每个生成的问题满足可测性和正确性阈值，从而为多模态解析几何产生无需注释的真实答案。

参见图2的说明。图2：该框架包括三个专门的生成组件和一个专用的验证组件。每个生成组件在一个特定任务的ReAct循环中运行，并接受来自Quality Verifier的重试结构化反馈；Quality Verifier在阶段之间的三个门控位置强制执行数据质量。

## 3. FormalAnalyticGeo

FormalAnalyticGeo是一个可扩展的框架，自动生成具有形式化验证的文本-图表一致性的多模态解析几何问题。与之前依赖模板合成或单模型引导的数据生成方法不同，FormalAnalyticGeo将任务分解为由形式化中间语言连接的专门阶段，并通过具有反馈驱动重试的质量门控来强制执行。我们首先给出一个概览。