TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving

📄 arXiv: 2504.15780v2 📥 PDF

作者: Daocheng Fu, Jianlong Chen, Renqiu Xia, Zijun Chen, Qi Liu, Yuan Feng, Hongbin Zhou, Renrui Zhang, Shiyang Feng, Peng Gao, Hongyuan Zha, Junchi Yan, Botian Shi, Yu Qiao, Bo Zhang

分类: cs.AI, cs.CL

发布日期: 2025-04-22 (更新: 2025-08-29)

🔗 代码/项目: GITHUB

💡 一句话要点

TrustGeoGen：用于可信多模态几何问题求解的形式化验证数据引擎

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 几何问题求解 形式化验证 数据引擎 多模态学习 大型语言模型 数据集生成 GeoTrust-200K

📋 核心要点

  1. 现有大型语言模型在几何问题求解中存在幻觉问题，导致生成的数据集质量不高，缺乏验证。
  2. TrustGeoGen通过多模态对齐、形式化验证和连接思维等创新方法，生成高质量、可信赖的几何问题数据集。
  3. 实验表明，在TrustGeoGen生成的数据集上训练的模型，在几何问题求解任务上性能显著提升，并具有良好的泛化能力。

📝 摘要（中文）

数学几何问题求解(GPS)需要可验证的逻辑连贯性和多模态推理能力。虽然大型语言模型(LLM)在GPS方面取得了快速进展，但其发展受到缺乏可靠基准和系统方法的阻碍。一个关键的挑战是LLM中固有的幻觉，这导致合成的GPS数据集通常是嘈杂的、未验证的和自相矛盾的。为了解决这个问题，我们引入了TrustGeoGen，一个数据引擎，它生成形式化验证的几何问题，以建立一个有原则的和可信的基准。我们的引擎集成了四个关键创新：1)多模态对齐，同步图、文本和逐步解决方案的生成；2)形式化验证，确保所有推理路径都符合规则；3)连接思维，将形式演绎与类人逻辑步骤联系起来；4)我们的GeoExplore系列算法，产生具有多个解决方案和自我反思回溯的多样化问题变体。使用这个引擎，我们创建了GeoTrust-200K数据集和相应的GeoTrust-test基准，两者都保证了跨模态的完整性。实验表明，最先进的模型在GeoTrust-test上仅达到45.83%的准确率，突显了其重大挑战。此外，在我们的合成数据上进行训练可以显著提高模型在GPS任务上的性能，并具有很强的泛化能力，可以推广到领域外(OOD)基准。

🔬 方法详解

问题定义：论文旨在解决数学几何问题求解中，由于现有大型语言模型（LLM）的幻觉问题，导致生成的几何问题数据集质量不高，缺乏形式化验证，存在噪声和自相矛盾的问题。现有方法难以保证数据集的可靠性和逻辑一致性，阻碍了LLM在几何问题求解方面的进一步发展。

核心思路：论文的核心思路是构建一个形式化验证的数据引擎TrustGeoGen，通过多模态对齐、形式化验证和连接思维等关键技术，生成高质量、可信赖的几何问题数据集。该引擎旨在消除LLM的幻觉，确保生成的数据集在逻辑上是连贯的、规则符合的，并且具有跨模态的一致性。

技术框架：TrustGeoGen数据引擎包含以下主要模块：1) 多模态对齐模块：同步生成几何图形、问题文本和逐步解决方案，确保三者之间的一致性。2) 形式化验证模块：对推理路径进行形式化验证，确保每一步推理都符合几何规则。3) 连接思维模块：将形式演绎与类人逻辑步骤联系起来，使生成的问题更贴近人类的思维方式。4) GeoExplore系列算法：用于生成多样化的几何问题变体，包括具有多个解决方案的问题和需要自我反思回溯的问题。

关键创新：该论文的关键创新在于提出了一个形式化验证的数据引擎TrustGeoGen，它能够生成高质量、可信赖的几何问题数据集。与现有方法相比，TrustGeoGen通过形式化验证确保了数据集的逻辑一致性和规则符合性，从而解决了LLM的幻觉问题。此外，GeoExplore系列算法能够生成多样化的几何问题变体，提高了数据集的丰富性和挑战性。

关键设计：TrustGeoGen的关键设计包括：1) 多模态对齐策略：采用特定的算法和规则，确保几何图形、问题文本和逐步解决方案在语义上保持一致。2) 形式化验证规则：基于几何公理和定理，构建形式化验证规则，用于验证推理路径的正确性。3) 连接思维算法：模拟人类的思维方式，将形式演绎与类人逻辑步骤相结合，生成更自然、更易于理解的几何问题。4) GeoExplore系列算法：通过随机扰动、约束修改等方法，生成多样化的几何问题变体。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，最先进的模型在GeoTrust-test基准上仅达到45.83%的准确率，突显了该基准的挑战性。此外，在TrustGeoGen生成的数据集上进行训练可以显著提高模型在GPS任务上的性能，并具有很强的泛化能力，可以推广到领域外(OOD)基准。这表明TrustGeoGen生成的数据集具有很高的质量和实用价值。

🎯 应用场景

该研究成果可应用于数学教育、智能辅导系统、几何定理自动证明等领域。高质量的几何问题数据集可以用于训练更强大的几何问题求解模型，提高模型在实际应用中的准确性和可靠性。此外，该数据引擎的设计思想也可以推广到其他需要形式化验证的领域，例如程序验证、逻辑推理等。

📄 摘要（原文）

Mathematical geometric problem solving (GPS) demands verifiable logical coherence and multimodal reasoning capabilities. While large language models (LLMs) have shown rapid progress in GPS, their advancement is hindered by the lack of reliable benchmarks and systematic methodologies. A critical challenge is the inherent hallucination in LLMs, which leads to synthetic GPS datasets that are often noisy, unverified, and self-contradictory. To address this, we introduce TrustGeoGen, a data engine that generates formally verified geometric problems to establish a principled and trustworthy benchmark. Our engine integrates four key innovations: 1) Multimodal Alignment, which synchronizes the generation of diagrams, text, and step-by-step solutions; 2) Formal Verification, ensuring all reasoning paths are rule-compliant; 3) Connection Thinking, bridging formal deduction with human-like logical steps; and 4) our \textit{GeoExplore} series algorithms, which produce diverse problem variants with multiple solutions and self-reflective backtracking. Using this engine, we create the GeoTrust-200K dataset and the corresponding GeoTrust-test benchmark, both with guaranteed cross-modal integrity. Experiments reveal that state-of-the-art models achieve only 45.83\% accuracy on GeoTrust-test, highlighting its significant challenge. Furthermore, training on our synthesized data substantially improves model performance on GPS tasks, with strong generalization to out-of-domain (OOD) benchmarks. Our code and data are available at https://github.com/Alpha-Innovator/TrustGeoGen