OpenAI、Navier-Stokes問題の証明で数学をコードに誤変換
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
OpenAIがNavier-Stokes問題の解決を発表した際、人間向けとコンピューター向けの2種類の証明を公開したが、両者が一致していないことが数学者チームの指摘で明らかになった。証明自体の正しさや問題解決の成否を否定するものではないが、AIモデルが生成した数学的成果をどこまで信頼できるかという疑問を投げかけている。Cambridge大学のAnders Hansen氏は、LLMが生成した証明はすべて人間が読む必要があり、数学者に膨大な負担がかかると警告する。
「これらの大規模言語モデルが生成した証明すべてに対して必要なのは、人間がそれを読むことです。そしてこれは数学者に膨大な追加負担を強いることになります」とCambridge大学のAnders Hansen氏は言う。
- krackers
- jey
この見出しは完全に間違っている。適切なコーディングのアナロジーはむしろこうだ。自然言語の論文はコード化する前の「設計書」であり、それをLean4の証明としてコード化していく過程で、細部が少しずれていることが判明し[1]、コードによる実装を機械検証可能な証明として書く中で修正された。これはここにいるほとんどの人にとって極めて共感できる状況だと確信している。ただし、論文すなわち「設計書」のほうは後から修正されなかった。
また、この「論文を書いてからコード」というアプローチは今や時代遅れだと思う。AI支援ワークフローにおける現代的なやり方は、まず「導出スケッチ <-> 機械検証可能な証明」を反復しながら、結果を漸進的に構築していくことだ。もちろん途中で `sorry` プレースホルダーを残しておいて後で埋めることもできるので、完全にボトムアップで進めなければならないわけではない。最後に、関心のあるトップレベルの命題(定理)について `sorry` のない証明が得られたら、そのLeanコードを基にLaTeXで解説を書き上げる作業に取りかかればよい。
1. 詳細は https://arxiv.org/abs/2610.08144 を参照。ただし彼らが挙げている例では、ある重要な評価に追加で5次の導関数が必要であり(Leanでもそのように記述されている)、論文はその評価が追加の4次導関数だけで成り立つと主張していた。