DeepMindは、一般のプログラマーに匹敵するAlphaCodeをリリースしました。同日、OpenAIが数学オリンピックで優勝しました。

カールしすぎ！

中国が春節を祝っている間、2つの有名なAI研究機関であるDeepMindとOpenAIがそれぞれ重要な研究成果を発表しました。DeepMindは、人間に匹敵するコンピュータプログラムを書くことができるTransformerモデルに基づくAlphaCodeをリリースしました。同時に、OpenAIが開発したニューラル定理証明器は、国際数学オリンピックの問題2つを無事に解きました。

AI によって征服されたこれら 2 つの領域は、あなたにとって馴染み深いものですか?そうです、2021年にOpenAIはAIコード補完ツールGitHub Copilotをリリースし、その背後にある技術であるCodeXを発表しました。同様に、DeepMindも昨年後半に、難しい数学の問題を解くAI研究の成果を発表し、Nature誌に掲載されました。

2つの研究機関の新たな研究結果は、AIが古い問題を解決するための新しいアイデアを提供したが、ネットユーザーはAIの分野が競争が激しすぎるとため息をつくしかない。

出典: ネットユーザーのWeiboのスクリーンショット

AlphaCodeは出場者の46%に勝利した

最近の論文で、DeepMind の研究者は AlphaCode を紹介しました。 AlphaCode は、Transformer ベースの言語モデルを使用して大規模なコード生成を実現し、それをプログラムとして記述します。

論文リンク: https://storage.googleapis.com/deepmind-media/AlphaCode/competition_level_code_generation_with_alphacode.pdf

研究者たちは、チェスで使用されるElo評価システムに似た、毎週のプログラミング課題と問題のランキングを共有する競争プログラミングプラットフォームであるCodeforcesの課題でAlphaCodeをテストしました。プログラマーが商用アプリケーションを構築するときに直面する可能性のあるタスクとは異なり、Codeforces の課題はより独立しており、コンピューター サイエンスのアルゴリズムと理論的概念に対する幅広い理解を必要とし、一般的には論理、数学、コーディングの専門知識を組み合わせた非常に特殊なパズルです。

AlphaCode は、Codeforces ウェブサイトで 5,000 人のユーザーが解決した 10 個の課題に対してテストされ、全体の上位 54.3% にランクされ、出場者の 46% に勝利しました。 DeepMind は、AlphaCode システムの Codeforces Elo が 1,238 であると推定しており、これは過去 6 か月間にサイトで競争したユーザーの上位 28% に入ることになります。

たとえば、AlphaCode をテストするあるチャレンジでは、参加者は有限の入力セットを使用して、ランダムに繰り返される s と t の文字の文字列を同じ文字の別の文字列に変換する方法を見つけることが求められました。たとえば、競技者は新しい文字を入力するだけでなく、「バックスペース」コマンドを使用して元の文字列からいくつかの文字を削除する必要がありました。 AlphaCode にとって、これは中程度の難易度の課題にすぎません。

課題のうち 10 件は、人間が行うのとまったく同じ形式で AlphaCode に入力されました。次に、AlphaCode は、人間の競技者と同じように、コードを実行して出力を調べることで、多数の可能な回答を生成し、それらを精査します。 「プロセス全体は自動で行われ、最適なサンプルを手動で選択する必要はない」と、アルファコード論文の共同リーダーであるユージア・リー氏とデビッド・チョイ氏は述べた。

Codeforces チャレンジで目立つのは簡単ではありません。 AlphaCode プロジェクトは 2 年以上前に開始されました。大規模な Transformer モデルの進歩と大規模なサンプリングおよびフィルタリング技術の組み合わせにより、DeepMind の研究者は AI が解決できる問題の数を大幅に増やすことができました。

疫病の影響により、プロジェクト作業のほとんどは自宅で完了しました。

研究者らは、選択された公開GitHubコードでモデルを事前トレーニングし、比較的小規模な競技プログラミングデータセットで微調整しました。評価中、私たちはそれぞれの問題に対して、これまでの作業よりも桁違いに多い数の C++ および Python プログラムを作成しました。これらのソリューションはその後、選別され、クラスター化され、外部評価のために提出された 10 個の候補プログラムの小さなセットに再ランク付けされました。この自動化システムは、デバッグ、コンパイル、テスト合格、最終提出という競合他社の試行錯誤のプロセスに代わるものです。

全体的に見ると、AlphaCode は競合他社の中ではほぼ中間にランクされています。競争に勝つには程遠いものの、この結果は AI の問題解決能力の大きな飛躍を表した。この進歩は、批判的思考を必要とするタスクに対するディープラーニング モデルの可能性を示しています。 DeepMind は、AlphaCode の現在のスキル セットは競技プログラミングにのみ適用できるが、その機能はプログラミングを容易にし、将来的には完全に自動化する将来のツールを作成するための新たな扉を開くと指摘しています。

他の多くの企業も同様のアプリケーションを開発しています。エンドユーザーにとって、これらのシステムは Gmail のスマート作成機能と同じように機能し、書いている内容に対して提案を提供します。

近年、AI プログラミング システムの開発は大きく進歩しましたが、これらのシステムが人間のプログラマーの仕事を引き継ぐにはまだほど遠い状態です。生成されるコードにはバグが含まれることが多く、システムは公開コードベースでトレーニングされることが多いため、著作権で保護された素材をコピーすることもあります。

GitHub Copilot AIプログラミングツールの調査で、研究者らは、このツールが出力するコードの約40%にセキュリティ上の脆弱性が含まれていることを発見した。セキュリティアナリストは、悪意のある人物が故意にコードを書き、それを隠されたバックドア付きのオンラインで共有し、そのコードを使って AI プログラムを訓練し、将来のプログラムにそのバグを挿入する可能性があるとさえ示唆しています。

このような課題は、AI プログラミング システムがプログラマーの仕事に徐々に統合される可能性が高いことを意味します。つまり、プログラマーはアシスタントとして研修を受け、自律的に作業を実行できると信頼されるまで、その提案は懐疑的に見られることになります。

DeepMind は現在、競技レベルのプログラミング問題と解答のデータセットを GitHub で公開しており、このデータセットには、これらのテストに合格したプログラムが正しいことを確認するための広範なテストのデータも含まれており、これは現在のデータセットに欠けている重要な機能です。 DeepMind は、このベンチマークが問題解決とコード生成におけるさらなる革新を推進することを期待しています。

GitHub プロジェクト アドレス: https://github.com/deepmind/code_contests

数学オリンピックの問題を解くニューラル定理証明器

科目競技の分野では、国際数学オリンピック（IMO）が非常に有名です。私たちがよく知っている多くの数学の巨匠（魏東毅など）がこの競技で優れた成績を収めています。

2021年、この大会には若干の変化がありました。マイクロソフトが長年開発してきた数学AI「Lean」もこの大会に加わり、人間のプレイヤーと競い合うようになったのです。 Lean は、2013 年に Microsoft Research が発表したコンピューター定理証明器であると報告されています。数学者は数式をコードに変換し、それを Lean に入力して、プログラムに定理が正しいかどうかを検証させることができます。

Lean が金メダルを目指す中、マイクロソフトに買収された OpenAI を含む研究者らは Lean を絶えず改良し続けている。ちょうど今、OpenAI は、IMO から採用した 2 つの問題と、AMC12 および AIME 競技からのいくつかの問題を含む、さまざまな高校オリンピックの難問を解くために、Lean 用のニューラル定理証明器を作成したと発表しました。

証明者は言語モデルを使用して、正式なステートメントの証明を見つけます。新たな証明が発見されるたびに、研究者はそれを新たなトレーニング データとして使用し、ニューラル ネットワークを改善して、ますます困難な命題に対する解決策を反復的に見つけられるようにします。

証明者は、高校オリンピックの難しい問題のセットを含む miniF2F ベンチマークで SOTA (41.2% vs 29.3%) を達成しました。

研究者たちは、この方法論をカリキュラム学習と呼んでいます。これは、手作業で収集されたさまざまな難易度の命題のセット (証明は不要) で構成されており、最も難しい命題は目標ベンチマークに似ています。当初、彼らのニューラル証明機は弱く、ほんの数個しか証明できませんでした。そこで彼らは、新たな証明を繰り返し探し、新たに見つかった証明に基づいてニューラル ネットワークを再トレーニングしました。 8 回の反復を経て、彼らの証明者は miniF2F で優れた結果を達成しました。

形式数学は、1) 豊富な内容があり、推論、創造性、洞察力を必要とする任意の定理を証明できること、2) 証明が成り立つかどうかを自動的に判断する方法 (つまり、形式システムによって検証されているかどうか) があるという点でゲームに似ていることから、興味深い研究分野です。以下の例に示すように、正式な命題を証明するには、一連の証明ステップを生成する必要があり、各ステップには戦術の呼び出しが含まれます。

正式なシステムによって受け入れられる成果物は低レベル (アセンブリ コードなど) であり、人間が作成するのは困難です。この戦略は、形式化を支援するために、より高レベルの命令からこのような成果物検索手順を生成することです。

これらの戦略は数学的な用語を引数として取り、戦略を呼び出すたびに、証明すべき現在の命題が証明しやすい命題に変換され、証明すべきものがなくなるまで続きます。

研究者たちは、ポリシーパラメータに必要な生の数学的用語を生成する能力がトレーニングプロセスで現れたことを観察したが、これはニューラル言語モデルなしでは不可能なことだった。以下の証明は、この例です。証明ステップ「use n + 1」（完全にモデルによって生成）では、「n + 1」をソリューションとして使用することを提案し、残りの正式な証明では、それが実際に機能することを確認するために「ring _ exp」戦略に依存しています。

研究者らはまた、モデルと検索プロセスが複数の重要な推論ステップを結び付ける証明を生成できることも観察した。以下の証明では、モデルはまず対偶を使用して存在命題 (∃ (x : ℝ), fx ≠ a * x + b) を導きます。次に、use (0 : ℝ) を使用してその証拠を生成し、 norm _ num 戦略を活用して証明を完了します。

このモデルは、ステートメントカリキュラム学習を使用してトレーニングされており、トレーニング教材のさまざまな問題、AMC12、AIME、およびIMOから適応された2つの問題を解くことができます。以下に、関連する 3 つの例を示します。

形式数学には、純粋な強化学習アプリケーションが成功する可能性を低くする 2 つの大きな課題があります。

1. 無限のアクション空間: 形式数学には、巨大な探索空間 (囲碁など) だけでなく、無限のアクション空間もあります。証明の探索の各ステップで、モデルの選択は、適切に動作するアクションの有限セットではなく、生成する必要がある外生的な数学的用語を含む複雑で無限の戦略セットです（たとえば、証人として機能する数学的命題の生成）。

2. 自己対戦の欠如: 2 人対戦ゲームとは対照的に、証明者は対戦相手と対戦するのではなく、証明する一連の命題と対戦します。非常に難しい命題に直面した場合、証明者が最初に扱いやすい中間ステートメントを生成できるようにする明らかなリファクタリングは存在しません。この非対称性により、2 人用ゲームでは成功する自己プレイ アルゴリズムを単純に適用できなくなります。

この研究では、研究者は言語モデルからアクションをサンプリングすることで、無限アクション空間の問題に対処します。言語モデルは、通常パラメータとして必要とされる元の数学用語だけでなく、ポリシー呼び出しも生成できます。自己プレイの欠如に関して、彼らは、2人用ゲームにおける自己プレイの重要な役割は、監督なしのカリキュラムを提供することであると観察しました。そのため、彼らは、この教師なしのカリキュラムを、さまざまな難易度の補助的な問題命題のセット（証明は不要）に置き換えることを提案しています。実験結果によると、これらの補助問題の難易度が十分に変化すると、トレーニング手順によって、難易度が増す一連の問題を解決でき、最終的には関心のある問題のセットに一般化できることがわかりました。

これらの結果は、ディープラーニング モデルが形式システムと対話する際に重要な数学的推論を実行できることを示しているため非常に興味深いものですが、証明器は依然としてコンテストで最高の学生のパフォーマンスからは程遠いものです。研究者らは、自分たちの研究がこの分野の研究、特にIMOに関する研究を促進することを期待しており、提案したステートメントカリキュラム学習法が自動推論の研究の進歩を加速させることができることを期待していると述べた。

まとめ

両機関の最新の研究成果が紹介され、その効果についてネット上でもレビューが散見される。

例えば、ある AI 研究者は、AlphaCode が人間のレベルに到達するには数年かかるだろう、Codeforce でのランキングは高校生や大学生の参加者が多いなど制限がある、AlphaCode によって生成されるプログラムの大半は間違っている、AlphaCode が実際に特定の問題を解決できるのはフィルタリングにサンプルテストを使用しているためである、などと長文のツイートを投稿しました。

一部の研究者は、これはアルファスターの多大な努力の結果であるようだとも述べた。

国内の AI 実践者は、休暇を利用してこれら 2 つの研究を研究し、独自の意見を表明することができます。