- 数学者 Terence Tao は OpenAI の新しい GPT 系モデル o1 を研究数学の課題で試し、以前のモデルより有能だが最先端の研究問題にはまだ不十分だと評価
- 曖昧な数学的問いでは、関連する定理である Cramer’s theorem を見つけて満足のいく答えを出し、以前の GPT の幻覚的な回答より明確に改善
- 難しい複素解析の問題では、ヒントや誘導が多いときにのみ正しい解法に到達し、核心的アイデアの生成 は依然として弱いことが判明
- Lean の形式化実験では、問題分解そのものは妥当だったが、Lean と Mathlib の情報が古く、コードエラーとライブラリ呼び出しの信頼性の問題が残存
- Tao は、AI が退屈で検証可能な下位作業をまず埋め、形式証明支援器と結びつくとき、数学研究の生産性を大きく高められると見ている
GPT-o1に対する総合評価
- OpenAI の新しい GPT 系モデル GPT-o1 は、LLM の実行前に初期推論ステップを行う
- Tao が触れたのはプロトタイプ版で、その後の回答では現在 preview version と呼ばれるモデルを主に実験したと述べている
- 全体として以前の反復より有能だが、最先端の研究数学課題ではまだ苦戦している
実験1: 曖昧な数学的問いと Cramer’s theorem
- 最初の実験は、過去に行った実験を繰り返したもの
- 問いは、文献から適切な定理である Cramer’s theorem を見つけなければ解けない、曖昧に表現された数学の質問だった
- 以前の GPT は関連概念の一部に触れたが、詳細は幻覚に近い無意味な回答だった
- 新モデルは Cramer’s theorem を特定し、Tao の見立てでは完全に満足できる答えを提供した
実験2: 難しい複素解析の問題
- 2つ目の実験は、以前 GPT-4 に証明作成支援を依頼した 難しい複素解析の問題 を新モデルに与えたもの
- 結果は以前のモデルより良かったが、期待には届かなかった
- 多くのヒントや誘導を与えると、正しくよく書かれた解法に到達できた
- 核心となる概念的アイデアを自力で生成できなかった
- 自明でないミスも起こした
- Tao はこの体験を、「完全に無能ではない平凡な大学院生の静的シミュレーション」を指導するのに似ていると見ている
- 以前のモデルは「実際に無能な大学院生の静的シミュレーション」に近かったため、今回のモデルは改善された水準と評価される
- あと1〜2回性能が向上し、コンピュータ代数パッケージ や 証明支援器 のようなツールと統合されれば、「有能な大学院生の静的シミュレーション」の水準に達し得ると見ている
- その水準に至れば、研究レベルの課題でもかなり有用になり得る
実験3: Lean 形式化課題
- 3つ目の実験は、新モデルに Lean である形の素数定理を別の形の素数定理から導出する作業を始めさせたもの
- 要求されたのは証明そのものではなく、問題を下位補題に分け、その命題を形式化することだった
- 結果は有望だった
- モデルは課題をよく理解した
- 問題を妥当に初期分解した
- 制約も明確だった
- 学習データに最新の Lean および数学ライブラリの情報が不足している
- コードには複数のミスが含まれていた
- Tao は、この程度の能力を持つモデルが Lean と Mathlib に特化して微調整され、IDE に統合されれば、形式化プロジェクトで非常に有用になり得ると見ている
意味検索と創造的戦略生成の実験
- Tao は 2010 年に “multiplicative integral” の正しい用語を見つけられず、MathOverflow に質問し、人間の専門家から満足のいく回答を得たことがある
- 同じ質問を o1 に投げたところ、完璧な答えを返した
- ただし、その MathOverflow 投稿がモデルの学習データに含まれていた可能性があり、意味検索能力の正確な評価とは言えないかもしれない
- それでも一部の意味検索クエリでは、高品質な回答という点で質疑応答サイトと同等の水準を示した
- 別の実験では、Tao は最近のブログ記事の前半を与え、Erdos 問題の既存の部分的進展を完全な解法に変えるための欠落要素を見つけさせた
- この結果はやや期待外れだった
- モデルは、ブログ記事にすでに書き直されていた最新研究の戦略と同じ戦略を提案した
- その戦略の創造的な変形は提示できなかった
- Tao は、LLM ツールにはランダムに創造的戦略を生み出す能力が多少あるものの、この側面はまだ弱いと見ている
大学院生の比喩に関する訂正
- Tao は AI ツールの能力を評価する際、人間の大学院生を静的で一次元的な「能力」水準に分類できるかのような、誤っていて有害になり得る印象を与えたと訂正している
- 既存の研究プロジェクトに貢献する能力は、大学院教育の多くの側面の1つであり、比較的小さな部分にすぎないと見ている
- 創造性、自立性、好奇心、説明能力、直観、専門性、労働倫理、組織力、社会的スキルなどに優れた学生は、割り当てられた技術課題に長けた学生よりも、より成功し影響力のある数学者になり得る
- 人間の学生は学ぶあいだに成長し、最初は苦手だった分野でも数年後には熟達し得る
- 一方で現代の AI ツールは、応答にフィードバックをある程度反映できても、個々のモデルは長期的成長を実際には行えないため、静的な性能指標で評価するほうが妥当だとしている
- Tao は、人間の学生を固定的なマインドセットで判断する枠組みは適切でなかったと謝罪している
研究支援ツールとしての有用性とコスト比
- Tao の比較基準は、専門数学者が指揮する複雑な数学研究プロジェクトで下位課題を補助できる度合いである
- 有能な大学院生は、プロジェクトに適応させ監督するための純粋な労力以上の価値ある貢献をできる
- 最新ツールはまだ、有用な出力を得るための労力より、適切にプロンプトし検証する労力のほうが大きい
- Tao は現在の比率をおおよそ 2x~5x と表現している
- 今後数年でこの比率が 1x 未満 に下がる可能性を排除する理由はないと見ている
- 比率が 1x を下回れば、その分野でのツールのより広い採用を引き起こし得る
- 一部の特定の下位課題では、すでに比率が 1 未満だと見ている
-
意味検索
- データ形式変換
- 数学研究の探索を助ける数値計算コード生成
Lean と Mathlib における不足点
- Tao の実験では、形式化ツールとして有用になるために最も不足しているのは、出力を最新の Lean と Mathlib に接地させる方法である
- Lean と Mathlib は毎月進化し続けている
- モデルは1年以上前の複数バージョンの Lean と Mathlib で学習されたように見え、これらのバージョンは互いに 100% 互換ではないと見ている
- その結果、モデルが作る構文やライブラリ呼び出しは信頼しにくい
- しかし、現在の Lean と Mathlib の状態を知る人であれば、ほとんどの小さなエラーを手動で修正できる程度には近い
検証可能な自動化と形式証明支援器
- Tao が念頭に置く主要なユースケースは、数学者が原理的には多くの手作業で解ける問題を、より速く解くことにある
- AI がまず退屈なステップを埋め、専門家の人間が出力を確認する方式である
- この場合、AI が真に独創的な思考を示さなくても、生産性を大幅に高められる
- 現在可能なものより大規模な研究プロジェクトも可能になるかもしれないと見ている
- こうしたツールが 形式証明支援器 と統合されれば、数学的命題の証明を提示する必要がある課題の整合性を高い信頼度で自動評価できる
- Tao は、この種の課題が研究レベル課題のかなりの部分を占めると見ている
数学研究向け AI ツール生態系の展望
- Tao は、さまざまな研究課題を処理する AI ツール生態系 が登場することを期待している
- これには文献検索、証明形式化、短い下位問題の解決といった作業が含まれる
- 現在は非常に大規模な汎用の独占的 LLM が最も注目を集めているが、いずれは追加改善や特定用途向け微調整に必要なデータと計算の限界費用が過度に高くなる可能性がある
- 研究コミュニティが独自のニーズに合わせて開発した、より軽量でオープンソースのモデルやデータセットも重要な役割を果たし得る
- 汎用モデルは、より狭い特化ツール群を調整するユーザーフレンドリーなインターフェースの役割を果たし得ると見ている
1件のコメント
Hacker Newsの意見
GPTがPythonのようにLean証明支援系へさらに合わせてチューニングされれば、研究レベルの数学で有用性が高まりそう
OR関連分野で働いているが、ChatGPT 4oはOR文献を十分に吸収していて、さまざまな「問題の形」に対してかなり使える混合整数計画（MIP）定式化を出せる
例えば「スコアに応じてi個のアイテムをn個のバケットに入れ、各バケットを順番に埋めたい」といった論理問題を与えると、実際に使える数学的定式化を吐き出し、たいていは少し直すだけで済む
論理が破綻し得る弱い定式化についても警告してくれるので、落とし穴を避けるのに非常に役立つ
もちろんMIP最適化を理解していなければ、この用途でうまく使うのは難しいし、GPTが段階的に推論できるよう問題を小さく分解する必要はあるが、できる人にとっては月20ドルの価値は十分にある
HNで有料・高性能なLLM、つまりSonnet 3.5やGPT-4oが役に立たないと不満を言うケースは、たいていLLMの強みを生かす使い方を知らないか、誇大宣伝のせいでワンショットの魔法を期待しているか、本当に自分の分野に合っていない場合に見える
LLMの強みを活用し、誤りを検証できる人にとっては、仕事でかなりのレバレッジになる
HNやインターネット全体は、LLMは「役に立たない」という反射的なこき下ろしと雑談の海になっているが、現実にはここ数週間、自分でコードを1行も直接書いていない
欲しいものを段落で指定し、落とし穴の周辺を案内してもらい、単純な反復ループで動くコードを得ている
これは完全に習得されたスキルであり、モデル、とりわけその周辺ツールは必要なベースラインに到達した
腰を据えて学び、仕事の進め方を身につければ、はるかに生産的な世界になる
編集: https://aider.chat/ + 有料の3.5 Sonnet
もっともらしい答えとつかみどころのない数学的説明を出してくるが、方程式は機能せず、推論もかみ合っていない
まるで証明のおかしい数学の授業を受けながら、自分がバカなのかと思っていたら、実は教授が脱走した認知症患者で、そもそも支離滅裂だったと分かるような感じだ
昨日もo1に、最大フローでsからtまでvを通る単純パスがあるかを調べさせたが、非常に説得力がありそうに見えるアルゴリズムが根本的に壊れていた
私の解法はその失敗した試みから一部の手法を取り入れたが、何度ヒントを出しても動く答えを見つけられず、ずっとs→tのフローだけを探そうとしていて、v→{s,t}が核心だと気づかなかった
その推論を検証する作業も精神的にあまりに疲れる
微妙に間違った答えは明らかに間違った答えより検出・ペナルティ付けが難しいので、RLHFが推論を曇らせる方向を選んでいるのではないかと疑うほどだ
x!=yをどう扱うか、ナップサック問題をどう扱うかといった基本ブロックは出せたが、教科書の暗記ではない少しでも面白い質問を投げると、どのモデルも正しくなかったように思う
どうやってより良い答えを得ているのか気になる
もしかすると私は、答えが間違っているのを見た瞬間に捨てて自分で書くからかもしれない
実際、ついさっきx,yが{1..9}範囲の整数変数であるときx!=yを定式化して説明してみろと頼んだら、制約式は正しかったが説明は間違っていた
研究結果も似たようなもので、今年初めに出た大規模なサーベイ論文では、LLMは教科書的な問題には概ね正しいが、複雑さと新規性が増すほどどんどん役に立たなくなるとされていた
結果はよく言っても型通りで、細部の作業に入ると、むしろ誤解を招く巧妙な落とし穴になる
LLMに特定の制約が何をしているのかを尋ねたり、さらに悪いことに独自のCPLEX構文糖衣の数学モデルを説明させたりすると、数学、構文、説明のすべてを幻覚する
HNの一部は、しゃべる犬がCコードを書いたのに、バッファオーバーフローのエラーがあるからといって無視するような人たちだ
2019年に戻って、Alexaのようなものとやり取りする経験が「平凡だが完全に無能ではない大学院生に助言するのとおおむね似ていた」という文章を読む、と想像すればいい
5年での差としては驚くべき水準だ
特に優秀だがリモートで働く個人貢献者が危なそうで、このフォーラムには明らかな利益相反がある
平凡な理系大学院生、特に辞めずに卒業するタイプは、私たちの大半と比べれば非常に印象的な人だ
「私たち」にそのレベルの知能を一日中アシスタントとして使えるというのは、トークン費用さえ負担できるなら、とてつもない生活のアップグレードだ
JensenはAIがiPhone時代に到達したと言っていた
今後5〜10年以内に、人々がどんな定義を付けようとAGIやASIは来ないだろうが、AIを補助知能または拡張知能と呼ぶほうを好むことが多い
現在のコンピューターとスマートフォンの販売を少なくとも5〜10年、または3〜4回の買い替えサイクルにわたって押し上げるだけの価値は提供するだろう
平均的な人はまだそこまでできない
モデルへのプロンプトがうまくないこともあるし、そもそも生活上の問題がテキストベースではないからだ
o1モデルは本当に驚異的
高速ベクトル類似度プロジェクトで、すでに高度に最適化していたRustコードにかなりの速度向上を得られ、綿密なベンチマークと正確性検証で確認した
それだけでなく、Jensen-Shannonダイバージェンスに基づく新しい統計的依存性の尺度を再構想し、概念化するのを助けてくれ、非常にうまく機能している
正規化相互情報量の超高速実装も作ってくれた。これは元のライブラリに入れたかったものの、15,000次元以上のような大きなベクトルで十分高速な方法を見つけられなかった部分
最初からコンパイルできる完璧なRustコードを出してくれたわけではないが、VS Codeのコンパイラ警告を貼り付けると、もう一度試してすべてのバグを直した
一方でGPT-4oは、Rustの型エラーやライフタイム／借用エラーなどを直すのに何十回もかかることが多く、Claude 3.5 Sonnetは奇妙なことにRustに関しては単に鈍かった
性能最適化と比較的バグの少ないコードだけでなく、創造的な問題解決、膨大な中核的数学・アルゴリズム知識と最新研究成果の統合、そして私が達成しようとしていることを理解して実際にやり遂げる能力まで合わさっていて、本当にゲームチェンジャーのように感じる
コードファイル変更のdiffはこちら: https://github.com/Dicklesworthstone/fast_vector_similarity/...
それでも、小さなライブラリを最適化し、高速な関数を実装することは、どんなプログラマーの道具箱にとっても大きな改善になる
o1についての私の経験はかなり違っていて、私の基準では「優秀な学部生」レベルとも言えない
たとえばここでかなり単純な質問をしたのに、完全に混乱していた
https://moorier.com/math-chat-1.png
https://moorier.com/math-chat-2.png
https://moorier.com/math-chat-3.png
全体の会話はここにあるはず: https://chatgpt.com/share/66e5d2dd-0b08-8011-89c8-f6895f3217...
さらに悪いことに、より遅く、より冗長でもある
このモデルはマルチモーダルではないので、添付された図形からはまったく学習されていなかった可能性がある
人々が幾何学の問題セットと解析学の問題セットを確認して、違いを比較してみるとよいと思う
ここでの理想的な体験は短く簡潔な答えであって、長々しくへりくだった答えではない
私にとって新しかったのは、「経験は平凡だが完全に無能ではない大学院生に助言するのに似ていた」ということが、これほど多くの分野で成り立つ点
LLMで整理し理解することから大きな価値を得た
自分が非常によく知っている領域では、小さな雑務をものすごくたくさん処理してくれるので助かる
Terenceが3つ目の実験で指摘したように、問題を分解すれば、小さな空欄を埋める作業はかなり堅実にこなす
ただし概念的理解が必要で、プロンプト技術もある程度入ってくる
知らない領域に入るときは、プロンプトを積み上げていく必要がある
答えが知られているなら、小さく具体的なものから掘り下げて外へ広げ、外から内へ入るときも具体的で焦点を絞って始めるのがよい
まったく知らない非常に複雑なテーマの概念的な層を掘り進めたうえで、YouTubeの専門家・研究論文・信頼できる出典で概念を検証するために使ってみたが、驚くべきツールだ
LLMを、自分でやる余裕のない足を使った調査をしてくれるインターンやジュニアのように扱っている
監督し、助け、ミスを確認しなければならないが、最終的には有用な結果が得られる
姿勢の面では、インターンを監督したりジュニアをメンタリングしたことがある人のほうが、LLM、特に有料モデルから価値を引き出しやすいと思う
逆に、キャリア初期の私もそうだったように、人から価値を引き出す方法を知らない熟練の孤高の個人貢献者は、あまりうまく使えないかもしれない
「Terence Taoのような創造的な数学的飛躍ができなければならない」というのは、AIにとってかなり高い基準に見える
プログラミング面接で、面接官が自分のチームが数か月かけて解いた問題を説明したあと、Googleなしで40分以内にホワイトボードにその解法を書けないと失望する状況に似ている
何でも受け入れるし、必ずしも「彼らのレベル」である必要はない
彼の書いた内容を読み、自分の経験に照らすと、そうした描写は不正確だと思う
今年初めにIMOで彼が行った講演にもあったが、彼はいくつかの相互作用に感銘を受けつつも、依然として何らかの創造的なひらめきが欠けていると感じているのだ
彼が実際に言ったことは具体的だ。「ここでの結果はやや期待外れだった……本質的にモデルは、その問題に関する最新の研究ですでに特定されていた戦略、そして私がブログ記事で書き直した戦略と同じようなものを提案したが、その戦略の創造的な変形は提示しなかった」
重要なのは、そのブログ記事自体がChatGPTへの入力の一部だったという点だ
それ以外にも彼は、将来的にはもっと有用になると予想しつつ、現時点では参考文献形式の整理と簡単な「Hello World」スタイルのコード作成にだけAI/ChatGPTを使っていると明言してきた
オンラインには、彼が研究にChatGPTを常用しているという主張がいくつもあるが、コーディング用途を超える部分は事実ではないように思う
ただし「Terence Taoの研究を助けられる」というのは、実際に高い基準ではある
ChatGPTでチュートリアルコードより複雑なプログラムを書いたり、基本的なブログ記事を書いてみたりすると、創造性が不足していて、コード設計もひどい
現在生きている人の中で最もIQが高いと見なし得る人物が、コンピュータがノーベル賞級の数学的推論を出せないからといって、感心はしつつも完全には満足していないのだとしたら、それ自体が大きな指標だと思う
では数学博士課程1年目の人はどう考えるべきなのか
Taoは以前の記事で、事実上「o1は大学院生とほぼ同じくらいだ」と述べて、この点に遠回しに触れていたように思う
人間も思考の連鎖型の推論から利益を得られるという点が興味深い
実際、数学を学ぶすべての学生が、関連する定義や情報を使う前にまずすべて思い出すよう求められれば、能力は大きく伸びると思う
現実には教師や数学者まで含めてそうしていないが、それは想起には労力がかかり、私たちは問題を解くのに必要な以上の労力を使いたがらないからだ
想起に失敗すると情報を調べなければならず、さらに労力がかかるので、実際には単に「勘で押し切る」強い誘因が生まれる
AIには労力の無駄に対する感情的な壁がないため、生来の能力以上に優れた推論者になる
どちらも過程を段階ごとに分解させ、論理が保たれ、重要な段階を飛ばさないようにする
しかし解答過程を示すことは、正しい手順を証明することに近く、「思考の連鎖」推論は進めながら関連する定義や概念を思い出させ、より深い理解を保証する
どちらも勘で押し切るのを避ける目的だが、「思考の連鎖」は人間が避けがちな想起の側面をより深く掘り下げる
思考の連鎖がLLMに役立つという証拠をあれほど多く見てきたのに、自分自身にもっと使ってみようとは考えなかった
もちろんすでにある程度はやっているが、普通はLLMほどではまったくない
もしかすると、だからこそ文章を書くことが優れた思考法としてよく称賛されるのかもしれない
文章を書くことは、より少ない労力でより長い思考の連鎖を可能にする
学校数学ではなく、大学レベルの数学の話だ
教えるときも常に定義に立ち返らせていた
私は数学研究がものすごく得意だったわけではなく、博士号とポスドクを経てやめたが、経験上、研究とは問題を深く考え、何が起きているのかをつかみ、どうにか分解してみることであると同時に、その問題に関連して知っていることをすべて洗い出し、似た問題を探してアイデアを盗めないかを見ることだった
独立した好奇心にもとづく趣味として、近いうちに数学の勉強に戻るつもりなので、とても楽しみにしている
今回はLLMに頼って勉強できるので、すごく面白くなりそうだ
偶然にもTerence Taoのように、私も教科書を見ながらよりよく理解しようとして、複素解析の質問をLLMにしてきた
オープンな形の数学的質問を解釈し、有用で関連のある、離れた概念的つながりを素早く見つける能力は驚くべきものだ
Fields賞受賞者であるTao教授は当然、現在の数学LLMを「完全に無能ではない大学院生」程度として見下ろしているが、私の現在の能力レベルでは、それは見上げる対象だということになる
6か月前に印象的だった例として、Kleinの壺のような向き付け不可能多様体でも複素解析ができるようにするには、どの定義を緩められるのかと尋ねたことがある。長い間考えていた問題だったが、LLMは即座にCauchy-Riemann方程式が大域的に不整合になる点を見抜いた
ある意味では、CRの任意の符号規約が多様体上の向きを定義しており、多様体の向きを反転することはiを-iと入れ替えるのと同じだ
これはLLMがそのように見るよう提案したため、今では理解できている
もちろん、これがLLMの独創的な思考というわけではなく、どこかの非常に専門的な大学院向け教科書に書かれている数学なのだろう
しかし私にとっては重要ではない
どこから始めればよいのかほとんど分からないこの種の質問は、LLMか博士号レベルの分野専門家なしには答えることが絶対に不可能だ
このような意味レベル検索を利用可能にする他のツールはなく、非常に強力だがなじみのないツールをどう最大限活用するか、慎重に考えている
答えを見つけた正確な教科書の参考文献まで示してくれれば、さらに良い
ベンチマークは攻略されたり学習に入ったりするし、この種のクエリについてチャットボットアリーナに十分なシグナルがあるはずもない
数か月もすれば、平均的なユーザーは主要モデル間の性能差を見分けられなくなりそうだ
Terence Tao に全面的に同意
これは実際の進展だ
LLM が推論を模倣するよう学習できる適切なデータがあれば、性能を改善できるとずっと信じてきた
ただし依然として パターンマッチング であり、このアプローチが真の汎化を生み出すうえでそれほど効果的ではないのではないかと疑っている
だから o1 が一般公開されれば、強化学習の段階でモデルが学んだ「推論プログラム」や「推論パターン」を超える、十分に新しい、あるいは複雑な問題において、継続的な幻覚と誤った推論を見る可能性が高い
https://www.lycee.ai/blog/openai-o1-release-agi-reasoning
私にとって o1 モデル は、良いときと悪いときが分かれる
一方では、試した日には毎回 NYT Connections ゲーム[0]を解いた[1]し、Claude Sonnet 3.5 を含む他のモデルにはできなかった
その反面、GPT-4o のように重要な細部を見落とし、幻覚を起こす
正解にたどり着くには手取り足取り直してやる必要があることが多く、時には自分でやったほうが簡単だったのではと思う
今回は答えを待つのに 20〜60 秒かかるので、さらに悪い
o1 が得意な領域は、私があえて必要としていないものなのかもしれない
私は従来型の STEM ではなくソフトウェアエンジニアリング寄りで、o1 はまだ待ち時間を正当化できるほど大幅に優れてはいない
まだ試していない領域は、実装計画やアーキテクチャ変更計画に使うことだ
ここではより良さそうだが、適切な問題を投げてみる必要がある
[0] https://www.nytimes.com/games/connections
[1] https://chatgpt.com/share/66e40d64-6f70-8004-9fe5-83dd3653a5...