Autoformalizing Euclidean Geometry

要約

自動形式化には、非形式的な数学を機械検証可能な形式的な定理や証明に自動的に変換することが含まれます。
ユークリッド幾何学は、自動形式化を研究するための興味深い制御可能な領域を提供します。
この論文では、ドメイン知識、SMT ソルバー、および大規模言語モデル (LLM) を組み合わせた、ユークリッド幾何学を自動形式化するための神経記号フレームワークを紹介します。
ユークリッド幾何学の課題の 1 つは、非形式的な証明が図に依存しており、形式化するのが難しいテキストにギャップが残ることです。
この問題に対処するために、定理証明器を使用してそのような図式情報を自動的に入力します。これにより、LLM は明示的なテキストのステップを自動形式化するだけで済み、モデルが容易になります。
また、自動形式化された定理ステートメントの自動意味評価も提供します。
Euclid の要素からの問題と、リーン証明アシスタントで形式化された UniGeo データセットから構成される自動形式化ベンチマークである LeanEuclid を構築します。
GPT-4 および GPT-4V を使用した実験では、幾何学問題の自動形式化に関する最先端の LLM の機能と限界が示されています。
データとコードは https://github.com/loganrjmurphy/LeanEuclid で入手できます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google