論文の概要: FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning

• arxiv url: http://arxiv.org/abs/2310.18021v2
• Date: Mon, 30 Oct 2023 01:08:02 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-31 11:47:38.368800
• Title: FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning
• Title（参考訳）: FormalGeo:人間ライクなIMOレベルの自動推論への第一歩
• Authors: Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yang Li, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhenbing Zeng, Shaorong Xie, Xiangfeng Luo, Tuo Leng
• Abstract要約: これは、私たちが過去3年間に達成した一連の研究の中で、初めての論文です。 我々は完全かつ互換性のある形式平面幾何学システムを構築した。 これは、IMOレベルの平面幾何学の課題と、可読性のあるAI自動推論の間に重要な橋渡しとなる。
• 参考スコア（独自算出の注目度）: 9.73597821684857
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.
• Abstract（参考訳）: これは、私たちが過去3年間に達成した一連の研究における最初の論文です。 本稿では,完全かつ互換性のある形式平面幾何システムを構築した。 これは、IMOレベルの平面形状問題と可読性AI自動推論の間に重要な橋渡しとなる。 このフォーマルなシステムがあれば、最新のAIモデルを私たちのフォーマルなシステムとシームレスに統合することができます。 この形式的なフレームワークの中で、AIは、他の自然言語を扱うのと同じように、IMOレベルの平面幾何学問題に対する推論的推論ソリューションを提供することができ、これらの証明は読みやすく、トレース可能で、検証可能である。 本稿では,幾何形式体系の発展を導くために,幾何形式化理論(GFT)を提案する。 GFTに基づいて、88の幾何述語と196の定理からなるフォーマルジオを確立した。 IMOレベルの幾何学問題を表現、検証、解決することができる。 また、PythonでFGPS(形式幾何学問題の解法)も作成しました。 これは、問題解決プロセスを検証するインタラクティブアシスタントと、前方探索、後方探索、AI支援検索などの様々な手法を活用する自動問題解決ツールの両方として機能する。 FormalGeo7kデータセットには6,981(データ拡張による186,832)の幾何学的問題と完全な形式言語アノテーションが含まれています。 フォーマルシステムの実装とフォーマルGeo7kの実験は、GFTの正しさと実用性を検証する。 奥行き優先探索法は2.42%の問題解決失敗率しか生み出せず,より低い解を得るために深層学習手法を組み込むことができる。 FGPSとFormalGeo7kデータセットのソースコードはhttps://github.com/BitSecret/FormalGeoで公開されている。

関連論文リスト

• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  平面幾何学的問題解法 (PGPS) のニューラルネットワークモデルを提案し, モーダル融合, 推論過程, 知識検証の3つの重要なステップについて述べる。 推論のために、幾何学的推論過程を記述するための説明可能な解プログラムを設計し、自己限定デコーダを用いて解プログラムを自動回帰的に生成する。 また, PGPS9Kと呼ばれる大規模幾何学的問題データセットを構築し, テキスト節, 解法プログラム, 関連知識解決器の詳細なアノテーションを含む。
  論文  参考訳（メタデータ） (2024-07-10T02:45:22Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning [1.137457877869062]
  我々はFGeoDRLと呼ばれるニューラルシンボリックシステムを構築し、人間のような幾何学的推論を自動的に行う。 神経部分は強化学習に基づくAIエージェントであり、問題解決方法を自律的に学習することができる。 フォーマルなgeo7kデータセットで実施された実験は、86.40%の問題解決成功率を達成した。
  論文  参考訳（メタデータ） (2024-02-14T09:48:39Z)
• FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems [1.137457877869062]
  本稿では,FGeo-TP (Theorem Predictor)を導入し,この言語モデルを用いて定理列の予測を行い,幾何学的問題を解く。 本研究では,FormalGeo7kデータセット上での言語モデル強化FGeo-TPの問題解決率を著しく向上させることを示す。
  論文  参考訳（メタデータ） (2024-02-14T09:44:28Z)
• G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model [124.68242155098189]
  大規模言語モデル(LLM)は、人間レベルの推論と生成能力に顕著な習熟性を示している。 G-LLaVAは幾何学的問題の解法において例外的な性能を示し、7Bパラメータしか持たないMathVistaベンチマークにおいて GPT-4-V を著しく上回っている。
  論文  参考訳（メタデータ） (2023-12-18T17:36:20Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。 我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。 また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
  論文  参考訳（メタデータ） (2022-12-06T04:37:51Z)
• GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning [172.36214872466707]
  我々は、テキスト記述、視覚図、定理知識の包括的理解を必要とする幾何学的問題を解くことに注力する。 そこで本研究では,5,010の幾何学的問題を含む幾何学的質問応答データセットGeoQAを提案する。
  論文  参考訳（メタデータ） (2021-05-30T12:34:17Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。 我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。 イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
  論文  参考訳（メタデータ） (2021-05-10T07:46:55Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。