Autoformalizing Euclidean Geometry

本文介绍了一种神经符号框架，用于将欧几里得几何自动形式化，该框架结合了领域知识、SMT求解器和大型语言模型(LLMs)。欧几里得几何的一个挑战是非正式证明依赖于图表，这导致文本中存在难以形式化的空白。为了解决这个问题，我们使用定理证明器自动填充这些图表信息，以便LLM只需要自动形式化明确的文本步骤，从而使模型更容易操作。我们还提供了自动语义评估以评估自动形式化的定理陈述。我们构建了LeanEuclid，这是一个自动形式化基准，包括欧几里得元素和UniGeo数据集中的问题，这些问题在Lean证明助手中进行了形式化。使用GPT-4和GPT-4V进行实验，展示了目前最先进的LLM在自动形式化几何问题方面的能力和局限性。数据和代码可在https://github.com/loganrjmurphy/LeanEuclid上获得。

本论文旨在解决自动形式化欧几里得几何定理和证明的问题，同时提出了一个神经符号框架来实现自动形式化。

该论文的关键思路是结合领域知识、SMT求解器和大型语言模型，利用定理证明器填补图形信息的空缺，从而实现自动形式化。

论文提出了一个名为LeanEuclid的自动形式化基准，包括欧几里得元素和UniGeo数据集中的问题，实验使用了GPT-4和GPT-4V，同时提供了自动语义评估和开源代码。此外，论文还探讨了当前大型语言模型在自动形式化中的局限性和未来研究方向。

近期相关研究包括《Deep Learning for Formal Mathematics: A Bibliography》、《Automated Reasoning in Geometry: A Survey》、《Formalizing 100 Theorems》等。