Microsoft AI が IMO コンテストに参加します!小さな目標：数学の金メダル

この記事はAI新メディアQuantum Bit（公開アカウントID：QbitAI）より許可を得て転載しています。転載の際は出典元にご連絡ください。

今年は「純粋な人間」が参加する最後のIMO（国際数学オリンピック）になるかもしれない。

△2020年IMOに出場する中国チーム（李金民の公式年齢情報は誤り）

来年はAIも金メダル争いに加わり、「シード選手」になるかもしれないからだ。

IMOイベントに潜入したAIはLeanと呼ばれ、マイクロソフトの研究者によって開発されました。

現在、来年の国際数学オリンピックにリーンが参加することを計画している。

つまり、世界中のオリンピック出場者とIMO金メダルを競うことになります。

リーンはIMOでそのスキルを発揮する準備ができている

実際、マイクロソフトの研究者が AI の IMO への参加を許可した理由は、それが優れた実験ツール (ツールマン) だからです。

IMOグランドチャレンジの創始者の一人であるマイクロソフトの研究員セルサム氏は、このコンテストの目標は人工知能システムを訓練し、世界最高峰の数学コンテストで金メダルを獲得することだと語った。

なぜなら、ここでは「最も簡単な」数学の問題（高度な数学を使用する必要はありませんが、解くことができない問題）が扱われるだけでなく、世界中からトップクラスの専門家が集まるからです。

AIが人間のようにこれらの数学の定理を証明できれば、AIに「人間のように考えさせる」ことはそれほど難しくないことも、ある程度説明できます。

この考えに基づき、マイクロソフトの研究者は、AI が独自の判断を下し、仮定に基づいて推論する能力を持てるようにすることを目指して、2013 年に Lean の開発を開始しました。

つまり、これは対話型の定理証明と自動定理証明の間のギャップを埋めることを目的としたオープンソース プロジェクトです。

自動定理証明: 数学で提案された定理や推測を証明または反証する方法を見つけます。システムは、仮定に基づいて推論できるだけでなく、特定の判断能力も備えている必要があります。

インタラクティブな定理証明: コンピューター支援証明ツールの助けを借りて、数学定理の正しさを理解して検証し、数学定理の証明を完了します。

Lean は 3 つのバージョンをリリースしており、4 番目のバージョンである Lean 4 は現在も改良が続けられています。現在のロジック システムは依存型理論に基づいており、従来のすべての数学定理を証明できるほど強力です。

言い換えれば、IMO で提起されたこれまで「見たことのない」数学的問題をそれ自体で証明することは、依然として非常に困難です。

現時点では、Lean 4 はまだ完全には準備ができていません。著者の Leonardo de Moura 氏は、今年の IMO に参加したとしても、「おそらく 0 ポイントしか得られないだろう」と述べています。

なぜなら、Lean は現在、特定の数学の問題にどのような概念が含まれているのか、またこれらの概念自体が何を意味するのかさえ理解できないからです。

証明の「最初のステップ」はアルゴリズムを困惑させた

多くの人にとって、数学は非常に抽象的で、十分に学ぶのが難しいものです。

実際、AI もあなたと同じように感じています。

AI は、アルゴリズム モデルが事前トレーニングの段階ですでに特定の種類の問題をある程度理解しているため、一般的なエンジニアリング アプリケーションの問題を解決するのに優れています。

つまり、現段階で AI が実行できる作業はまだ限られているということです。通常、AI が「より複雑な計算」を実行できるようになるには、与えられた条件とデータ、そして継続的な「練習」が必要になります。

これは「1」から「2」、「3」、さらには無限大へのプロセスです。

しかし、数学の問題を証明するという性質は異なります。公理や複雑な方程式を証明するには、ゼロから始める必要があります。

証明の最初のステップ: 合理的な証明パスを提案します。現在、この重要なタスクを 0 から 1 まで実行できるのは人間の脳だけです。

ほとんどの AI は、自分のアイデアを証明するための最初のステップを踏むのが難しいと感じています。

最も単純かつ最も古い数学の公理の 1 つを取り上げます。紀元前 300 年、ユークリッドは素数が無限に存在することを証明しました。

この結論を証明する鍵は、既知の素数をすべて掛け合わせて 1 を加えると、常に新しい素数を見つけることができることに気づくことです。この考えを念頭に置くと、次の証明は非常に簡単になります。

しかし、「このアイデアを考える」という行為自体は、AIにとっては非常に難しいものです。

私の意見に戻ると、公式コンテストの 3 つの問題は、微積分などの高度な数学は関係ないものの、出場者は中学校レベルの数学の知識をすべて使って巧みなアイデアや解決策を考え出す必要があります。

たとえば、2005 年の IMO の実際の質問は次のとおりです。

当時、さまざまな国の参加者が少なくとも 3 つの異なる証明を提示しました。広く認知され議論された解決法は、コーシーの不等式を単純化するアイデアを利用したもので、A4 用紙の約半ページを占めていました。

モルドバからの別の出場者は、2行の式を使って創造的に証明を完成させました。

上の行は「なぜなら」、下の行は「だから」です。そのシンプルさと正確さ、さらには「大雑把で効果的」さが、観客に衝撃を与えました。

この独創的なアイデアは、その年のIMO特別賞も受賞しました。

なお、IMO 特別賞は総合得点ではなく、独自の問題解決方法を持つ出場者にのみ授与されます。

この画期的な「第一歩」は、現在の AI では達成することがほぼ不可能です。

マイクロソフトの研究者が「金メダルを獲得する」という目標を設定したのも、このためかもしれません。

賢い方法では人間の脳に勝てないのであれば、リーンはどのような方法で人間の脳と競争するのでしょうか?

リーンで数学を学ぶにはどうすればいいですか?

すべての AI アルゴリズムと同様に、Lean もトレーニングのために「データを入力」する必要があります。

現在の Lean では、IMO の質問に対する完全な証明プロセスを設計できないだけでなく、一部の質問に含まれる概念を理解することさえできません。

したがって、リーンにとっての最優先事項は、数学をもっと学ぶことです。

トレーニング データはMathlibライブラリから取得されます。 Mathlib は、大学 2 年生レベル以下のほぼすべての数学の知識を収録した基本的な数学データベースです。

しかし、Mathlib には中学校の数学に関してまだいくつかのギャップがあり、チームは Mathlib データベースの完成に取り組んでいます。

知識を習得することは最初のステップに過ぎません。それを柔軟に適用する方法が鍵となります。

チームは、チェスや囲碁 AI などと同じアプローチ、つまりアルゴリズムが最適な解決策を見つけるまで決定木に従うアプローチを採用しました。

IMO の多くの質問に対する鍵は、何らかの証明パターンを見つけることです。数学的な証明の真髄に到達することは、一連の非常に具体的かつ論理的なステップです。

研究者たちは、IMO 問題で実証されたすべての詳細を使用して Lean をトレーニングしようとしました。

ただし、このアプローチにも限界があります。それぞれの特定の質問はアルゴリズムにとって「専門的」すぎることが判明し、次の異なるタイプの質問は依然として解決できません。

この問題を解決するために、チームは以前の IMO の問題の詳細な形式的な証明を書く数学者を必要としていました。その後、チームは証明に使用されたさまざまな戦略を改良しました。

次に、リーンのタスクは、これらの戦略の中から「勝利」の組み合わせを見つけることです。

この作業は実際には聞こえるよりもはるかに困難で、チームは次のように説明しました。

囲碁では、最善の動きを見つけることが目標です。数学では、最高のチェスゲームを見つけ、そのゲーム内で最善の動きを見つけることが目標です。

チームは、来年も金メダルを獲得するのはまだ難しいかもしれないが、少なくともリーンには競技に参加するチャンスがあるだろうと語った。

この点に関して、一部のネットユーザーは近年のAIの急速な進歩を嘆いている。最初はチェス、次は囲碁…そして今やAIは国際オリンピックで金メダルを獲得しようとしている。

しかし、一部のネットユーザーは悲観的で、現段階ではAIは特定の側面においてのみ人間のレベルに近づくことができると考えている。

現在、AIのアルゴリズムはすべて人間の認知に基づいています...そのため、（数学の定理を証明する）などの特殊なタスクに関しては、私は否定的な態度をとります。結局のところ、世界中でほんの少数の人々だけが助けを提供することができます。

「数学的思考とは何か？」

この質問を徹底的に説明するのは驚くほど難しいです。数学者が新しい問題を解こうとするとき、ましてやそれをアルゴリズムに実装しようとするとき、数学者の頭の中で何が起こっているのかを説明するのは困難です。

一部の AI チームは数学的思考のより深いレベルへと一歩踏み出していますが、採用した戦略から判断すると、依然として過去のアイデアから学び、最も成功率の高い「順列と組み合わせ」を選択しているところです。

こうした AI アルゴリズムは、創造性や画期的な進歩において人間を上回るほど成熟するにはまだ程遠い。

そして、お隣の GPT も数学的証明の方向で初期の成果を達成しました。

最近、OpenAI は数学の問題に対して GPT-f をリリースしました。これは、Transformer 言語モデルの生成機能を使用して定理を自動的に証明します。

GPT-f によって発見された 23 の短い証明が、Metamath メインライブラリに受け入れられました。AI の数学的証明が業界に認められたのはこれが初めてです。

GPT は実際に、数学者を含め、すべての人の仕事を破壊することになるでしょう。

では、Lean と GPT-f のどちらを好みますか?

プロジェクトリンク:
リーンプローバー

オンラインでプレイ可能:
https://leanprover.github.io/live/master/