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 で作成しました。
これは、前方検索、後方検索、AI 支援検索などのさまざまな方法を利用して、問題解決プロセスを検証するための対話型アシスタントと自動化された問題解決ツールの両方として機能します。
完全な形式言語アノテーションを使用して、6,981 (データ拡張により 186,832 に拡張) のジオメトリ問題を含む FormalGeo7k データセットにアノテーションを付けました。
形式システムの実装と FormalGeo7k での実験により、GFT の正確さと有用性が検証されます。
逆方向深さ優先探索法では、問題解決の失敗率は 2.42% しか得られませんが、深層学習技術を組み込むことで、より低い失敗率を達成できます。
FGPS および FormalGeo7k データセットのソース コードは、https://github.com/BitSecret/FormalGeo で入手できます。

要約(オリジナル)

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. With this formal system in place, we have been able to seamlessly integrate modern AI models with our formal system. Within this formal framework, 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, utilizing various methods such as forward search, backward search and AI-assisted search. We’ve annotated the FormalGeo7k dataset, containing 6,981 (expand to 186,832 through data augmentation) geometry problems with complete formal language annotations. Implementation of the formal system and experiments on the FormalGeo7k 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 FormalGeo7k dataset are available at https://github.com/BitSecret/FormalGeo.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google