論文の概要: Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry
- arxiv url: http://arxiv.org/abs/2404.06405v2
- Date: Thu, 11 Apr 2024 14:37:29 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-12 17:46:48.906778
- Title: Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry
- Title（参考訳）: Wuの手法はシンボルAIを銀メダリストに、AlphaGeometryはIMO Geometryで金メダリストに勝る
- Authors: Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, Matthias Bethge,
- Abstract要約: 我々は、AlphaGeometryで導入されたIMO-AG-30 Challengeを再考し、Wuの手法が驚くほど強いことを発見した。
ウーの方法だけでは15の問題を解くことができ、そのうちのいくつかは他の方法では解けない。
IMO-AG-30では,30問題中27を解き,IMOゴールドメダリストに勝るAI手法として,新たな最先端の自動定理を定めている。
- 参考スコア（独自算出の注目度）: 16.41436428888792
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proving geometric theorems constitutes a hallmark of visual reasoning combining both intuitive and logical skills. Therefore, automated theorem proving of Olympiad-level geometry problems is considered a notable milestone in human-level automated reasoning. The introduction of AlphaGeometry, a neuro-symbolic model trained with 100 million synthetic samples, marked a major breakthrough. It solved 25 of 30 International Mathematical Olympiad (IMO) problems whereas the reported baseline based on Wu's method solved only ten. In this note, we revisit the IMO-AG-30 Challenge introduced with AlphaGeometry, and find that Wu's method is surprisingly strong. Wu's method alone can solve 15 problems, and some of them are not solved by any of the other methods. This leads to two key findings: (i) Combining Wu's method with the classic synthetic methods of deductive databases and angle, ratio, and distance chasing solves 21 out of 30 methods by just using a CPU-only laptop with a time limit of 5 minutes per problem. Essentially, this classic method solves just 4 problems less than AlphaGeometry and establishes the first fully symbolic baseline strong enough to rival the performance of an IMO silver medalist. (ii) Wu's method even solves 2 of the 5 problems that AlphaGeometry failed to solve. Thus, by combining AlphaGeometry with Wu's method we set a new state-of-the-art for automated theorem proving on IMO-AG-30, solving 27 out of 30 problems, the first AI method which outperforms an IMO gold medalist.
- Abstract（参考訳）: 幾何学的定理を証明することは、直感的および論理的スキルを兼ね備えた視覚的推論の目印となる。
したがって、オリンピアドレベルの幾何学問題を証明した自動定理は、人間レベルの自動推論において顕著なマイルストーンであると考えられている。
1億の合成サンプルで訓練されたニューロシンボリックモデルであるAlphaGeometryの導入は、大きなブレークスルーとなった。
IMO(International Mathematical Olympiad)問題30件のうち25件を解決したが、Wu法に基づく報告ベースラインは10件に過ぎなかった。
本稿では,AlphaGeometry で導入された IMO-AG-30 Challenge を再検討し,Wu の手法が驚くほど強いことを示す。
ウーの方法だけでは15の問題を解くことができ、そのうちのいくつかは他の方法では解けない。
これは2つの重要な発見につながります。
(i)CPUのみのラップトップを1時間5分に制限しただけで30の手法のうち21の手法をWu法と古典的なデダクティブデータベース、角度、距離追尾法を組み合わせることで解決する。
基本的には、この古典的な手法はAlphaGeometryより4つの問題を解くだけで、IMO銀メダリストのパフォーマンスに匹敵するほどに、最初の完全に象徴的なベースラインを確立する。
(ii)Wuの手法は、AlphaGeometryが解けなかった5つの問題のうち2つを解く。
したがって、AlphaGeometry と Wu の手法を組み合わせることで、IMO-AG-30 で証明された自動定理の最先端を新たに設定し、30 問題のうち27 を解き、IMO ゴールドメダリストを上回った最初のAI手法である。
関連論文リスト
- Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models [63.31878920079154]
Olympiadレベルでの大規模言語モデルの数学的推論を評価するためのベンチマークを提案する。
既存のOlympiad関連のベンチマークとは異なり、我々のデータセットは数学にのみ焦点をあてている。
実験の結果,最も先進的なモデルであるOpenAI o1-miniとOpenAI o1-previewでさえ,高度に難解なオリンピアドレベルの問題に悩まされていることが明らかとなった。
論文 参考訳（メタデータ） (2024-10-10T14:39:33Z) - Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
平面幾何学的問題解法 (PGPS) のニューラルネットワークモデルを提案し, モーダル融合, 推論過程, 知識検証の3つの重要なステップについて述べる。
推論のために、幾何学的推論過程を記述するための説明可能な解プログラムを設計し、自己限定デコーダを用いて解プログラムを自動回帰的に生成する。
また, PGPS9Kと呼ばれる大規模幾何学的問題データセットを構築し, テキスト節, 解法プログラム, 関連知識解決器の詳細なアノテーションを含む。
論文 参考訳（メタデータ） (2024-07-10T02:45:22Z) - Proving Olympiad Algebraic Inequalities without Human Demonstrations [3.3466865213133836]
複雑な不等式定理を自律的に生成できる代数的不等式証明システムである AIPS を提案する。
20 Olympiadレベルの不等式に関するテストセットでは、AIPSは10の解決に成功し、最先端の手法よりも優れていた。
1つの定理が2024年の大都市オリンピアードの競争問題に選ばれた。
論文 参考訳（メタデータ） (2024-06-20T11:37:53Z) - Can Language Models Solve Olympiad Programming? [40.54366634332231]
本稿ではUSACOベンチマークについて,USA Computing Olympiadの307の問題点について紹介する。
競争型プログラミングのための様々なLM推論手法を初めて構築・テストする。
GPT-4 は 8.7% パス@1 の精度しか達成していない。
論文 参考訳（メタデータ） (2024-04-16T23:27:38Z) - FormalGeo: An Extensible Formalized Framework for Olympiad Geometric
Problem Solving [9.73597821684857]
これは、私たちが過去3年間に達成した一連の研究の中で、初めての論文です。
本稿では,一貫した平面幾何学システムを構築した。
これは、IMOレベルの平面幾何学の課題と、可読性のあるAI自動推論の間に重要な橋渡しとなる。
論文 参考訳（メタデータ） (2023-10-27T09:55:12Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - 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) - Learning Equational Theorem Proving [2.8784416089703955]
深層強化学習環境下で証明された方程式定理を学習するための最短解イミテーション学習(3SIL)を開発した。
自己学習されたモデルは、準群論におけるトップオープン予想の1つによって生じる問題を証明する上で、最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2021-02-10T16:33:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。