AI Mathematics Olympiad は、500 万米ドルの賞金で、IMO の金メダルを獲得できる大型モデルを探しています。

巴比特_

2023-11-28 09:21:55

記事のソース: 量子ビット

画像出典:Unbounded AIによって生成

AIのために特別に設立されたIMO国際数学オリンピックはここにあります-

なんと1,000万ドルです!

競争は「新しいチューリングテストに代わって」と主張していますが、どのように比較しますか?

人類で最も賢い数学の天才と直接対決し、同じ基準の金メダルを獲得します。

このイベントを過小評価しないでください、数学のマスターTao Zhexuanでさえここにいて、公式ウェブサイトでそれを推奨しています:

このコンペティションは、AIの問題解決戦略を見極めるためのベンチマークであり、まさに今私たちが必要としているものです。

ニュースが出るやいなや、ネチズンはかなり興奮しました。

IMO会長が言ったように、世界で最も明るい若者の波に対抗できるモデルはどれですか?

いわゆる「ご褒美の下には勇敢な男がいなければならない」という、独自の道筋を持つAIは本当にエキサイティングです。

AIが最大500万ドルでIMOに参加

このコンペティションの略称はAI-MOです。

その本来の意図は、大規模言語モデルの数学的推論能力を促進し、最高レベルの人間の数学に匹敵する新しいAIモデルの開発を奨励することです(IMOコンペティション)。

なぜベンチマークとしてIMOを選ぶのですか?

IMOのトピックは、一般的に代数学、幾何学、整数論、組み合わせ論の4つのカテゴリに分類され、高度な数学的知識は必要ありませんが、参加者は正しい考え方と数学的リテラシーを持っている必要があります。

統計によると、金メダリストがフィールズメダルを獲得する可能性は、平均的なケンブリッジ博士課程の卒業生よりも50倍高いことが示されています。

さらに、フィールズ賞受賞者の半数はIMOの大会に出場しています。

このコンペティションに基づいて、AIに特化したこのAI-MOコンペティションは2024年初頭に開始されます。

組織委員会は、参加するAIモデルが人間の出場者と同じ形式で質問を処理し、人間が読める最終回答を生成し、IMO標準を使用して専門家パネルによって採点されることを要求しています。

本研究成果は、来年7月に英国バースで開催される第65回IMO総会で発表される予定です。

最終的に、ゴールドレベルに到達したAIには、500万ドルの大賞が贈られます。

「重要なマイルストーンを達成」した残りのAIモデルは、残りの進捗賞を分け合い、総額は500万ドルになります。

賞の資格を得るには、参加者がAI-MOパブリック共有契約に準拠する必要があること、つまり、受賞モデルがオープンソースでなければならないことに言及する価値があります。

具体的なルールについては、組織委員会で現在審議中であり、現在、公式は諮問委員会のメンバー(特に数学者、AI、機械学習の専門家)と大会を主導するディレクターを募集しており、これらはすべて有給で完全にリモートで行うことができ、どの大物が参加するかは不明です。

ただし、AI-MOはIMOが開始した公式のコンペティションではないことに注意する必要があります。

実際のスポンサーは、ロンドンを拠点とするノンバンク金融機関で、機械学習の定量的取引に従事するXTX Marketsです。

何はともあれ、XTX Marketsはヒーローに焦点を当てています。

また、昨年、オックスフォード大学と奨学金を設立し、女子学生に数学の勉強を奨励しました。

競争自体に関しては、一部のネチズンも憶測の波を始めました:どのAIモデルが最も有望ですか?

Wolframプラグインを搭載したGPT-4が最初に持ち出されたが、冷水を注がれたのも初めてだった。

しかし、その背後にあるOpenAIは依然として支持されています(ただし、大手テクノロジー企業は競争のターゲットオーディエンスではありません)。

一部の悲観的なネチズンは、次のように直接主張しました。

カッコイイけど、5年後には誰もできないはずだ。

同時に、次のようにも主張されています。

このようなモデルを訓練することは難しくありませんが、データの取得と処理は困難であり、結局のところ、これらの問題にはテキストだけでなく、複雑な意味を持つ多くの画像や記号も含まれます。

すべては2024年に明らかになります。

AI-MOはIMOに挑戦する最初のAIではないことは言及する価値があります。

2019年には、OpenAI、Microsoft、スタンフォード大学、Googleなどの大学や機関の研究者数人が、IMOグランドチャレンジと呼ばれるコンペティションをすでに開始していました。

これまで誰もこのチャレンジに成功したことがない

IMOグランドチャレンジは、IMOの金メダルを獲得できるAIを見つけるために設定されたコンテストでもあります。

この数学ゲームにおけるAIの5つのルールを見てみましょう。

フォーマットについて。証明プロセスの厳密さと検証可能性を確保するためには、問題と証明の両方を正式な(機械検証可能な)方法で行う必要があります。

つまり、IMO問題はリーンプログラミング言語に基づく式に変換され、リーン定理証明者を介してAIに入力され、AIもリーンプログラミング言語で証明を書く必要があります。

スコアについて。 AIの各証明問題は、IMOの審判が得点する時間でもあるため、10分以内に真偽が判断されます。人間と違って、AIには「部分的な点数」というものはありません。

リソースについて。 AIも人間と同じように、1日4.5時間(合計2日)で3つの問題を解く必要があり、コンピューティングリソースに制限はありません。

再現性について。 AIはオープンソースである必要があり、モデルはIMOの初日の終わりまでに公開され、再現可能でなければなりません。 AI がインターネットに接続できない必要があります。

チャレンジ自体について。最大の課題は、AIに人間のように金メダル🏅を獲得させることです。

このコンペティションは、7人のAI研究者と数学者によって開始されました。

OpenAI の Daniel Selsam 氏、Microsoft の Leonardo de Moura 氏、Imperial College の Kevin Buzzard 氏、ピッツバーグ大学の Reid Barton 氏、スタンフォード大学の Percy Liang 氏、Google AI の Sarah Loos 氏、ラドバウド大学の Freek Wiedijk 氏です。

それから4年が経った今、一部の出場者の注目を集めています。

しかし、多くのAIや数学の研究者がこの分野に挑戦しようと、あるいはこの分野の小さな目標に挑戦してきましたが、IMOチャンピオンシップで優勝するという最終目標にはまだほど遠いです。

このゲームには「シンプルモード」が必要だという提案もありました。

たとえば、研究者のXi Wangは、IMOの実際の質問を行うためにいくつかの既存のSMTソルバーを使用しようとしましたが、結果は平凡です。