Wu’s Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

要約

幾何学定理の証明は、直感的スキルと論理的スキルの両方を組み合わせた視覚的推論の特徴を構成します。
したがって、オリンピックレベルの幾何学問題の自動定理証明は、人間レベルの自動推論における注目すべきマイルストーンと考えられています。
1 億の合成サンプルでトレーニングされた神経象徴モデルである AlphaGeometry の導入は、大きな進歩をもたらしました。
国際数学オリンピック (IMO) の問題 30 問中 25 問が解決されましたが、Wu の方法に基づいて報告されたベースラインでは 10 問しか解決されませんでした。
このノートでは、AlphaGeometry で導入された IMO-AG-30 チャレンジを再検討し、Wu の手法が驚くほど強力であることを発見しました。
ウー氏の方法だけで 15 個の問題を解決できますが、その中には他の方法では解決できない問題もあります。
これにより、2 つの重要な発見が得られます。(i) Wu の手法を、演繹データベースおよび角度、比率、距離追跡の古典的な合成手法と組み合わせると、5 分の制限時間で CPU のみのラップトップを使用するだけで、30 の手法のうち 21 が解決されました。
問題ごとに。
基本的に、この古典的な手法は、AlphaGeometry よりもわずか 4 つ少ない問題を解決し、IMO 銀メダリストのパフォーマンスに匹敵するのに十分な強度を備えた最初の完全にシンボリックなベースラインを確立します。
(ii) Wu の方法は、AlphaGeometry が解決できなかった 5 つの問題のうち 2 つも解決します。
したがって、AlphaGeometry と Wu の手法を組み合わせることで、IMO-AG-30 での自動定理証明の新しい最先端技術を確立し、30 問題中 27 問題を解決しました。これは、IMO 金メダリストを上回る初の AI 手法です。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google