OpenAIはナビエ・ストークス問題の証明で数学をコードに誤訳した

AI生成の証明は、形式化と呼ばれるプロセスでチェックされることが多い。Pixels Hunter/Shutterstock OpenAIは、ナビエ・ストークス問題の証明を発表する際に、微妙なエラーを犯した可能性があると、数学者チームが主張している。このエラーは、証明が間違っているとか、OpenAIが問題を正しく解決していないという意味ではないが、AIモデルによって生成された数学的結果が常に信頼できるかどうかという疑問を投げかける。「これらの大規模言語モデル生成証明すべてに対して行われなければならないのは、人間がそれらを読み取ることです。これは数学者にとって膨大な追加の負担を生み出します」と、ケンブリッジ大学のアンダース・ハンセンは述べている。9月8日、OpenAIは、数学における最も有名な未解決問題の一つであるナビエ・ストークス問題の解を見つけたと発表した。同社は証明を2つのバージョンで公開した――一つは人間が書くような英語と数学記号の組み合わせである「自然言語」で書かれたもの、もう一つはコンピュータコードであるLeanで書かれたものだ。Leanの証明は、自然言語バージョンの形式化を意図しており、コンピュータが論理的なステートメントがすべて真であることを機械的に検証できるようにするものだ。問題は、ハンセンとそのチームによると、それらが一致しないことだ。広告「この形式化プロセスは、ピアレビューに取って代わろうとしています」と、ケンブリッジ大学のチームメンバーであるファビアン・チルチェッリは述べている。「ピアレビューとは、人間の目が証明を見ることです。しかし、私たちがこの論文で示したのは、この種のAI自動形式化を使用しても、同じ目的を達成できないということです。」もっと読む OpenAIの722の新しい論文の中で最も興味深い数学的発見を明確にするために、研究者たちはOpenAIがナビエ・ストークス問題を解決できなかったと言っているわけではない。自然言語の証明とLeanの証明の両方が解決策を提供している可能性は十分にあり、ピタゴラスの定理の証明が何百もあるのと同じだ。むしろ、彼らの主張はより微妙なものだ：OpenAIのモデルがLeanに変換する際に「誤訳」したということだ。「自然言語の証明が間違っているとは言っていません」とハンセンは言う。「正しいとも言っていません。」問題は、OpenAIが2つの証明を同一のものとして提示しており、GitHub上で「このリポジトリには、[論文]『Finite time blowup for Navier–Stokes』で提示された結果のLean 4形式化が含まれています」と述べていることだ。この誤訳は、AIが「コンパイル」するLean証明を生成しなければならないため発生する。つまり、コンピュータコードは完全に自己整合性があり、エラーを生成しないということだとハンセンは言う。自動形式化の過程で、AIがコンパイルしない証明の一部を見つけた場合、たとえそれが自然言語で書かれた証明から逸脱することになったとしても、回避策を見つけようとするだろう。もっと読む OpenAIは722の数学論文を公開したが、今やその混乱を片付けなければならないチームの具体的な主張は、証明の一部であるLemma 8.6にかかっている。自然言語の証明では、この部分の数式は、mを整数とした場合に、ある値がm + 4未満であることを要求している。Leanの証明では、対応する値はm + 5未満であることが要求されており、これは数学的に弱い。なぜなら、x + 3 = 6という方程式を解くように求められ、その答えがx = 3であると想像すると理解しやすい。xが4未満でなければならないという証明を書くことは可能であり、またxが5未満でなければならないという証明も可能だ。どちらも完全に正しい数学的ステートメントだが、異なることを言っている。後者の証明はxの可能な解をより多く許容するため、数学的に弱い。OpenAIはNew Scientistに対し、自然言語の証明とLeanコードの間の不一致を認識しており、それがどちらかの証明が無効であることを意味するものではないと語った。同社は、自然言語の証明に見つかったエラーは修正し、今週公開された722の数学論文の形式化プロセスも継続すると述べている。これらの論文のうち、Lean証明が添付されているのは一部だけであり、それら自体も手作業でチェックされていない。証明の山の中の針を見つけるこの逸脱を見つけるには、ChatGPTに自然言語とLeanの証明の間の潜在的な不一致を探すように依頼し、その後手作業でチェックするという、ややシュールなプロセスが含まれた。ChatGPTが提案した不一致の多くは、検査の結果、結局は一致していることが判明した。「これらのことをすべて手動で調べるのは悪夢でした」とハンセンは言う。チームは、真の不一致を特定するのに約2週間かかった。一方、OpenAIのエージェントは証明の生成に88時間を費やしたと述べている。「OpenAIは、この結果をどれだけ早く生成できたかを自慢していますが、それはプロセスのほんの一部です」と、ロンドンキングス・カレッジのチームメンバーであるアレクサンダー・バストゥニスは述べている。AIモデルが数学を正確に自動形式化できるかどうかという問いに答えることは、数学者がこれらの結果を信頼するために不可欠だ。アンダースとそのチームは、ChatGPTが元の自然言語とは一致しない証明のLeanバージョンを生成することが可能であることを実証しており、AIはその過程で論理的な議論を静かに変更してエラーを隠蔽している。「それは私を助けようとしているのですが、そうすることによって、それは助けていないのです」とハンセンは言う。購読者限定ニュースレターLost in Space-Timeに登録するニュースレターに登録するもしこれが長くて複雑な証明で起こった場合、両方のバージョンを詳細に検査しない限り、誰かがそれに気づくのは非常に難しいだろう。この問題は、OpenAIが最近リリースした722本の論文のバッチによって、さらに喫緊のものとなっている。「このすべてが真実であり、私たちがしなければならないのは論文を読むことだけだ」と考えるなら、それは危険だとハンセンは言う。「科学を行う目的は、人類が世界の仕組みを理解し、教育的な意思決定ができるようにすることです。もしその理解を失ったら、私たちは何をしているのでしょうか？」インペリアル・カレッジ・ロンドンのケビン・バザードは、このような議論では、定理のステートメントとその証明を区別することが重要だと指摘している。例えば、有名なフェルマーの最終定理のステートメントは、正の整数a、b、c、nに対して、aⁿ + bⁿ = cⁿ が成り立つのはnが1または2の場合のみであるというものだ。これはLeanに変換するのが簡単で、簡単にチェックできる。Leanのステートメントが正しいと確信できれば、証明がコンパイルされれば、証明は真実であると確信できる。ハンセンとそのチームが指摘した問題は、PDFドキュメントとして公開された証明の自然言語バージョンについては何も教えてくれないということだ。「ナビエ・ストークス問題が正しく解決されたと確信しています」とバザードは言う。「PDFに記載されている証明が正しいかどうかについては、それほど確信が持てません。」ハンセンは、OpenAIがチームの仕事を「非常に真剣に」受け止め、堅牢な自動形式化技術の開発にさらに多くの作業が必要だと希望していると述べている。「解決策はありますか？まだありません。管理された方法で実行することは可能ですか？はい、それは可能になるでしょうが、最適な、そして究極の方法は完全に未知です。」ジャーナル参照: arXiv DOI: 10.48550/arXiv.2610.08144 トピック: 数学 テクノロジー AIまたは「超知能」？ トランプだけが混乱しているわけではない コメント 数学 OpenAIの722の新しい論文の中で最も興味深い数学的発見 ニュース スペース AIの時代に必要なゲートキーピングとは？ ニュース テクノロジー OpenAIは722の数学論文を公開したが、今やその混乱を片付けなければならない コメント