まだ必要な計算量についての情報はないけど、GoogleやOpenAIからこの成果を達成するために何が必要だったのか、詳しい内訳を見てみたいな。スレッドで熱く議論されたのは、OpenAIの結果に関してで、「Geminiには数学問題の高品質な解法のキュレーションされたコーパスへのアクセスを提供し、IMO問題に取り組むための一般的なヒントやコツを指示に追加しました。」ということ。一般的なモデルがそんなことができるかどうかの答えは、モデルが特にIMO問題に特化して訓練されたということのようで、これは多くの人が予想していたことだね。結果を否定するわけじゃないけど、データの質が出力の質に直結するなら、古典的な機械学習技術とあまり変わらない気もする。

昨年の専門的なLeanベースのシステムから、より汎用的なLLM + RLアプローチに移行したのは超興味深いね。これが数学コンペティション以外でもパフォーマンス向上につながると思う。どこまでこのフロンティアが進むのか、楽しみだな。記事によると、使われているシステムは、今夏に発表される一般的な「DeepThink」モデル/機能とはそれほど遠くないみたいだね。

「Gemini Deepthinkの“進化版”」って、違うモデルだったり、今後のGemini UltraサブスクリプションのDeepthinkよりもかなり多くの計算時間を使ったことを意味してると思う。OpenAIとGoogleが互角なのを見るのはやっぱりクールだね。

今、競技数学の世界では、Deep Blue対カスパロフの瞬間が起きてると思う。数年前からの大きな進歩だけど、まだまだ半分尊敬できるAI数学者には遠い気がする。生きている今が本当にワクワクする時代だね！

AlphaGeometryとAlphaProofは、まず専門家が自然言語からドメイン特化型言語（Leanなど）に問題を翻訳し、証明についても逆に行う必要があった。それには2〜3日かかる計算も必要だった。今年、私たちの進化したGeminiモデルは自然言語でエンドツーエンドで動作し、公式の問題記述から直接厳密な数学的証明を生成した。だから、問題は最初にLeanに翻訳されたわけじゃない。でも、モデルは内部の思考プロセスでLeanやインターネット検索、計算機、Python、その他のツールを使ったのかな？OpenAIはそれを使っていないと言ってたけど、これが同じ主張かどうかはわからない。ここについてもう少し明確にしてほしいな。両システムが使用した計算量の大まかな規模を、ドルで測定したい。できること自体はもちろんすごいけど、価格が高すぎるとまだ役に立たないからね。開示がない限り、価格は実際に高いと思っておくよ。 編集:「ツール使用なし、インターネットアクセスなし」が確認された: https://x.com/FredZhang0/status/1947364744412758305

スコアを見る限り、彼らも質問6には答えられなかったみたい？それって確認されたの？

OpenAIとGeminiの回答を比べると、Geminiの書き方の方がずっと分かりやすいね。もうちょっと見やすくできると思うけど、証明の流れは簡単に追えるよ。これのおかげで、OpenAIの回答よりもずっと短くなってるし、ちゃんとした文章になってる。

今年、私たちの高度なGeminiモデルは自然言語でエンドツーエンドで動作し、公式の問題説明から直接厳密な数学的証明を生成しました。ここでは少数派の意見かもしれないけど、彼らが形式的な手法から離れていくのがちょっと残念だな。もし本当に数学を「自動化」したり、機械規模でやりたいなら、例えば何千ページにも及ぶ証明を作成する場合、形式化する以外に進む道はないと思う。そうしないと、証明を理解して検証するために人間のレビューアが必要というボトルネックを超えられないから。

6問中5問解けた、スコアは42点中35点。比較のために言うと、OpenAIも数日前に35/42だったよ。

これってどれくらい大事なことなの？僕は計算障害があるから、2つの数字を足すのもほとんどできないし、数学の言葉にはあまり注意を払ってないんだけど、読む限りではこれは非常に難しい、または人間にはできないってこと？この特定の課題の次は何が来るの？ありがとう。