Autoformalizing Euclidean Geometry

📄 arXiv: 2405.17216v1 📥 PDF

作者: Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si

分类: cs.LG, cs.AI, cs.LO, stat.ML

发布日期: 2024-05-27

备注: Accepted to ICML 2024. The first two authors contributed equally

🔗 代码/项目: GITHUB

💡 一句话要点

提出结合领域知识、SMT求解器和LLM的欧几里得几何自动形式化框架

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

关键词: 自动形式化 欧几里得几何 定理证明 大型语言模型 神经符号 Lean 几何证明

📋 核心要点

  1. 现有欧几里得几何自动形式化方法难以处理非正式证明中依赖图表而产生的文本空白。
  2. 该论文提出利用定理证明器自动填充图表信息，使LLM只需处理显式文本步骤，降低形式化难度。
  3. 构建了LeanEuclid基准测试LLM在欧几里得几何自动形式化上的能力，并分析了GPT-4和GPT-4V的性能。

📝 摘要（中文）

本文提出了一种神经符号框架，用于自动形式化欧几里得几何，该框架结合了领域知识、SMT求解器和大型语言模型（LLM）。欧几里得几何中的一个挑战是，非正式证明依赖于图表，导致文本中存在难以形式化的空白。为了解决这个问题，我们使用定理证明器自动填充这些图表信息，从而使LLM只需自动形式化显式的文本步骤，降低了模型的难度。我们还为自动形式化的定理语句提供了自动语义评估。我们构建了LeanEuclid，这是一个自动形式化基准，包含来自欧几里得《几何原本》和UniGeo数据集的问题，并已在Lean证明助手中形式化。使用GPT-4和GPT-4V进行的实验展示了最先进的LLM在自动形式化几何问题上的能力和局限性。

🔬 方法详解

问题定义：论文旨在解决欧几里得几何的自动形式化问题。现有方法在处理非正式的几何证明时，由于证明过程中大量依赖图表，导致文本描述中存在许多隐含的步骤和信息，这给自动形式化带来了很大的挑战。传统的自动形式化方法难以有效地补全这些隐含信息，导致形式化过程困难重重。

核心思路：论文的核心思路是利用定理证明器来自动补全非正式证明中缺失的图表信息。通过定理证明器，可以自动推导出图表中隐含的几何关系，从而将非正式证明转化为更加完整和明确的形式，降低了LLM自动形式化的难度。

技术框架：该框架主要包含以下几个模块：1) 领域知识库：包含欧几里得几何的基本定理和公理；2) 定理证明器：用于自动推导图表中的几何关系，补全证明过程中的隐含信息；3) 大型语言模型（LLM）：用于将补全后的证明文本自动转化为形式化的定理和证明；4) 自动语义评估模块：用于评估自动形式化的定理语句的正确性。整体流程是，首先利用定理证明器补全非正式证明，然后利用LLM将补全后的证明转化为形式化语言，最后利用自动语义评估模块评估形式化结果。

关键创新：该论文的关键创新在于将定理证明器与LLM相结合，用于解决欧几里得几何的自动形式化问题。通过定理证明器自动补全图表信息，降低了LLM自动形式化的难度，提高了形式化的准确率和效率。此外，论文还提出了自动语义评估方法，可以自动评估形式化结果的正确性。

关键设计：论文构建了LeanEuclid基准，包含来自《几何原本》和UniGeo数据集的问题，并使用Lean证明助手进行形式化。实验中，使用了GPT-4和GPT-4V等先进的LLM进行自动形式化，并分析了它们的性能。具体的参数设置、损失函数和网络结构等技术细节未在摘要中详细描述，属于未知信息。

📊 实验亮点

实验结果表明，GPT-4和GPT-4V在LeanEuclid基准上展现了一定的自动形式化能力，但仍存在局限性。该研究揭示了当前LLM在处理复杂几何问题时的优势和不足，为未来研究提供了重要的参考。

🎯 应用场景

该研究成果可应用于自动化数学定理证明、智能教育系统、形式化验证等领域。通过自动形式化几何证明，可以提高数学研究的效率，辅助学生理解几何概念，并为形式化验证提供基础。未来，该技术有望扩展到其他数学领域，实现更广泛的数学知识自动化。

📄 摘要（原文）

Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs). One challenge in Euclidean geometry is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. To address this issue, we use theorem provers to fill in such diagrammatic information automatically, so that the LLM only needs to autoformalize the explicit textual steps, making it easier for the model. We also provide automatic semantic evaluation for autoformalized theorem statements. We construct LeanEuclid, an autoformalization benchmark consisting of problems from Euclid's Elements and the UniGeo dataset formalized in the Lean proof assistant. Experiments with GPT-4 and GPT-4V show the capability and limitations of state-of-the-art LLMs on autoformalizing geometry problems. The data and code are available at https://github.com/loganrjmurphy/LeanEuclid.