FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning

要約

これは、私たちが過去 3 年間にわたって達成した一連の研究の最初の論文です。
この論文では、完全で互換性のある形式平面幾何学システムを構築しました。
これは、IMO レベルの平面ジオメトリの課題と可読性の高い AI 自動推論の間の重要な橋渡しとして機能します。
この正式なフレームワーク内で、私たちは最新の AI モデルを正式なシステムとシームレスに統合することができました。
AI は現在、他の自然言語を扱うのと同じように、IMO レベルの平面幾何学問題に対して演繹的推論による解決策を提供できるようになり、これらの証明は読み取り可能、追跡可能、検証可能です。
幾何形式体系の開発を導くために、幾何形式形式化理論 (GFT) を提案します。
GFT に基づいて、88 の幾何学的述語と 196 の定理からなる FormalGeo を確立しました。
IMO レベルの幾何学問題を表現、検証、解決できます。
また、FGPS (形式幾何学問題ソルバー) を Python で作成しました。
これは、問題解決プロセスを検証するための対話型アシスタントと自動化された問題解決ツールの両方として機能します。
formgeo7k および formeo-imo データセットにアノテーションを付けました。
前者には 6,981 個 (データ拡張により 133,818 個に拡張) の幾何学問題が含まれており、後者には 18 個 (2,627 個に拡張され、継続的に増加) の IMO レベルの難しい幾何学問題が含まれています。
注釈付きの問題にはすべて、詳細な形式言語の説明と解決策が含まれています。
正式なシステムの実装と実験により、GFT の正確さと有用性が検証されます。
逆方向深さ優先探索法では、問題解決の失敗率は 2.42% しか得られませんが、深層学習技術を組み込むことで、より低い失敗率を達成できます。
FGPS のソース コードとデータセットは https://github.com/BitSecret/FGPS で入手できます。

要約(オリジナル)

This is the first paper in a series of work we have accomplished over the past three years. In this paper, we have constructed a complete and compatible formal plane geometry system. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning. Within this formal framework, we have been able to seamlessly integrate modern AI models with our formal system. AI is now capable of providing deductive reasoning solutions to IMO-level plane geometry problems, just like handling other natural languages, and these proofs are readable, traceable, and verifiable. We propose the geometry formalization theory (GFT) to guide the development of the geometry formal system. Based on the GFT, we have established the FormalGeo, which consists of 88 geometric predicates and 196 theorems. It can represent, validate, and solve IMO-level geometry problems. we also have crafted the FGPS (formal geometry problem solver) in Python. It serves as both an interactive assistant for verifying problem-solving processes and an automated problem solver. We’ve annotated the formalgeo7k and formalgeo-imo datasets. The former contains 6,981 (expand to 133,818 through data augmentation) geometry problems, while the latter includes 18 (expand to 2,627 and continuously increasing) IMO-level challenging geometry problems. All annotated problems include detailed formal language descriptions and solutions. Implementation of the formal system and experiments validate the correctness and utility of the GFT. The backward depth-first search method only yields a 2.42% problem-solving failure rate, and we can incorporate deep learning techniques to achieve lower one. The source code of FGPS and datasets are available at https://github.com/BitSecret/FGPS.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google