■ 1. OpenAIの数学解答公開と諮問グループ
- OpenAIの大量公開:
- 今週、世界有数の難問に対する数百件の解答とする成果をGitHubで公開
- 前回モデルが長年の未解決問題を解いた際の論争を避けるため、一流数学者の諮問グループに相談したと説明
- 基準未達の実態:
- OpenAIは数学者が示した基準に届いていない
- 特に数学的結果に対する人間の理解の必要性という点で不十分
- 100万ドル懸賞問題の解答で、自然言語版と形式化版の食い違いを指摘する論文も登場し、懸念が強まった
- AGMAIの概要:
- Institute for Advanced Studyが主催する「数学とAIに関する諮問グループ」
- 世界各地の機関に所属する著名な研究者9人で構成
- 9月末に、数学の問題に取り組むフロンティアラボ向けのガイドラインを公表
- AGMAIの声明:
- 推奨事項がどの程度守られたかは、最終的に数学界が判断すべき事柄とする立場
- TechCrunchによる詳細評価の依頼には回答なし
■ 2. ガイドラインとの照合
- 第一の要請への違反:
- AGMAIは、プロプライエタリモデルでの高度な数学問題のテスト中止を最初に求めた
- OpenAIは公開文書で、自社のプロプライエタリモデルを未解決問題で評価していると明言
- 守られた原則:
- 可能な限り早期の結果公開
- モデルが結論に至った過程に関する情報の添付
- 守られなかった原則:
- 思考の連鎖（chain of thought）を公開したのは719本の論文中わずか10本
- 理解困難な証明は形式化すべきとの提言に対し、形式化を経ていない証明は42%
- 自然言語版と形式化版を対応づける機械可読メタデータの添付要請にも未対応
- 人間の理解への責任:
- 公開時に「人間の理解が後に続くことへの責任」を負うというAGMAI原則を果たしているかは不明確
- AGMAIは、解答を実質的に意味あるものにする人間の数学者の研究資金をOpenAIが支援すべきと提案
■ 3. 数学界からの批判
- テレンス・タオの指摘:
- OpenAIの手法を批判してきた著名な数学者で、公開後にSNSで発言
- 分野自体に関心のないAIプロンプターが問題を自律的に解いている状況を問題視
- 彼らは「解決」後に分野への関心を失い、出力を理解していない
- その結果、質問への回答、講演、分野との交流ができない
- 人間による発見との違い:
- 人間は新しい結果に責任を持ち、論文や講演、セミナーで数学界と関わる
- その過程で解答の理解が深まり、他の問題に使える戦略が見つかる
- 新しい知見を実用分野へ応用することも可能になる
- メラニー・ウッドの見解:
- ハーバード大学の数学教授
- モデルが出した解答は公開時点で人間に理解されておらず、そこから作業が始まると指摘
■ 4. 自然言語証明と形式化の乖離
- AIによる証明の手順:
- まず自然言語で説明を作成
- 次にその結果をLeanで表現
- Leanはコードとしてコンパイルすることで証明の正しさを理論上確認できるプログラミング言語
- 「lost in translation」論文:
- ケンブリッジ大学とキングス・カレッジ・ロンドンの数学者が今週発表
- フロンティアラボの取り組み方に疑問を提起
- ナビエ・ストークス方程式に由来する問題へのOpenAIの解答で、自然言語証明とLeanコードの食い違いを少なくとも2つ記録
- 食い違いの意味:
- いずれかの解答を否定するものではない
- モデルに自らの解答の形式化を人間抜きで任せられるかに疑問を投げかける
- 論文の結論:
- 誤訳の現象があるため、OpenAIの自然言語証明や自動形式化されたLean証明を一見して信頼すべきではない
- 他の証明と同等の査読と精査が必要