ある10月2日のWorld Science Festivalインタビューで、数学者のTristan Buckmasterは、AIを使って得た結果について語りました。彼は正しいと考えていますが、他の数学者には読みにくいものです。この話は、最近のNavier–Stokes発表が提起した問いをより具体化します。読みやすい説明に追加の作業が必要なとき、研究者の共同体は形式的な論証をどう検証できるでしょうか。

BuckmasterはLevent Alpögeとの滑らかな外力を受ける三次元Euler方程式の研究について話していました。この結果は、9月8日のOpenAIの主張とは別のものです。その主張は滑らかな外力を受けるNavier–Stokes方程式に関するものです。Navier–Stokesには粘性がありますが、Eulerにはありません。OpenAIは、有限時間での特異性発生を主張する結果について、論文とLeanによる形式化を公開しました。Millennium Prizeを運営する機関は、賞を発表していません。

大きな変化

  • 何が変わったか：Buckmasterは、AI生成の論証とLeanを用いて別個の強制Euler結果を確立した経験と、そのような証明を数学者に説明するために残されている作業について、自らの言葉で語りました。
  • なぜ重要か：形式的な検証により、符号化された論証が指定された定義や依存関係から導かれることを確認できます。数学者は定理が何を述べているか、その考えがどう働くか、誰の先行研究を用いているかも理解する必要があります。
  • 今後の注目点：OpenAIのNavier–Stokes主張に対するClayの評価、読みやすい証明の説明、著者性とアクセスに関する公開の議論から、この結果がどう評価されるかが見えてきます。結果に対するBuckmasterの確信は専門家の見解であり、賞の決定ではありません。

検証された論証にも説明が必要

そのインタビューでではBuckmasterは、Eulerの結果についてAIが最初に生成した証明には、有用な着想に加え、無関係な計算や読みにくい文章も含まれていたと述べました。チームはまず他のエージェントを使って個々の段階を検討し、その後、論証をLeanに移して形式的に検証しました。提示が不十分だったものの、できあがった証明は正しかったと述べています。この話は彼のEuler研究についてのものであり、OpenAIによる別のNavier–Stokes論文のすべての部分を彼が独自に検証したという意味ではありません。

この区別は実務上重要です。Leanは、指定された証明環境で正確に形式化された命題を検証します。それだけで長い論証が、方法を再利用したい研究者にとって読みやすくなるわけではありません。BuckmasterはBrian Greeneに、他のAIシステムが自分にはほとんど読めない箇所を解析でき、AIに通常の数学的な言葉へ言い換えさせることも作業の一部になったと話しました。公開PDFは読みにくかったものの、Navier–Stokesの議論の考えは理解できたとも述べています。これは彼の評価であり、BIG CHANGEによる証明監査ではありません。Leanファイルを実行したり、いずれかの定理を査読したりはしていません。

NYU Courantの9月14日の報告は、BuckmasterとAlpögeの成果を、滑らかな外力と有限エネルギーの初期データを持つ強制三次元Eulerにおける有限時間での正則性喪失と説明しています。共同研究の3本の論文がLeanで形式化され、この結果はDiego CórdobaとLuis Martínez-Zoroaが始めた研究方針の中に位置づけられるとしています。貢献を帰属する際、こうした詳細は重要です。モデル生成の証明は、既存の数学的な道筋を発展させつつ、それを築いた人々の功績を消さずに済みます。

急速に進む一連の出来事の中の二つの結果

OpenAIによると、同社の内部エージェントシステムはまず外力のないEulerの結果を生み出し、その研究の流れを別のNavier–Stokes構成に用いました。同社の発表は、強制Eulerの結果についてBuckmasterとAlpögeの先行性を認める一方、自社の証明は独立に開発されたと述べています。Buckmasterはインタビューで、数学的な仕組みには関連があり、粘性に対処するためOpenAIが崩壊する渦の考えを加えたと説明しました。両者の説明は異なる方程式と証明手順を扱っている点で一致しますが、時系列や知的貢献に関するすべての疑問を解決するものではありません。

欧州のEuropean Mathematical Societyは発表を歓迎しつつ、先行研究を強調し、著者性、貢献の評価、内部モデルへのアクセスに注意を促しました。9月11日のClayの回答は、Navier–Stokes問題はどうやら解決したようだとしつつ、成果の評価と貢献の帰属を急がないと述べました。BuckmasterはGreeneに、OpenAIには解決策があると信じていると話しました。専門家の肯定的な見解と機関による継続的な評価は、同時に成り立ちます。

最近のOpenAIによる数学論文3本の追加撤回は別の出来事です。報告された符号の誤りは主張を個別に検討する理由になりますが、Navier–Stokesの証明にも同じ誤りがあることを示すものではありません。BIG CHANGEのリポジトリ確認ガイドは原稿の版や証明資料の探し方を説明し、査読能力についての見解は説明と確認に専用の支援が必要だと述べています。以前のNavier–Stokes記事は、この一連の出来事の始まりを記録しています。このインタビューは、AIシステムが論証を出した後に何が起こるかについて、現役数学者の説明を加えます。

これほど重大な主張について、次に有用なのは正確で人が読める説明、検証可能な形式的資料、独立した数学者の反応です。それぞれ役割が異なります。証明候補を作る速度が上がったことで、こうした仕事はより急務になります。一方、Clayが示した手続きには慎重に進める余地があります。

出典・参考資料