Navier–Stokes方程式：翻訳の過程で失われた真意とは？

Navier–Stokes（ナビエ・ストークス）方程式の理論的背景や物理的解釈が、異なる言語や学術的コンテキストに移される過程で、いかに曖昧になり、あるいは誤解を招いているかについての議論。

Navier-Stokes（ナビエ・ストークス方程式）について、手っ取り早く復習したいならここがおすすめ：https://p.migdal.pl/equations-explained-colorfully/#navier-s... (https://p.migdal.pl/equations-explained-colorfully/#navier-stokes)

理解が正しければ、これって「自然言語による証明」と「Leanによる証明」の整合性を問うているだけで、Leanの証明そのものが間違っていると言っているわけではないよね？

AI関連のいつもの小競り合いはさておき、一番の爆弾発言はこれだね。

「具体的には、形式化されたLeanの証明は、ナビエ・ストークス方程式の解の爆発に関する自然言語（NL）の証明と対応していないことを示す」

つまり筆者たちは、OpenAIはナビエ・ストークス方程式を実際には証明できていないと主張しているみたいだ。もし解釈が合っていれば、LLMがナビエ・ストークスの元となる「自然言語」での考え方を正しく形式化できていない、と言っていることになる。これが事実なら、提示されたLeanの証明はナビエ・ストークスの証明ではなく、元の自然言語のアイデアを正しく翻訳できていない何らかの別のものになる。もしこれが正しければかなり大胆な主張だし、他の研究者がどう評価するのか見てみたい。

うーん、ざっと目を通したけど、OpenAIが「強制項付きのナビエ・ストークス爆発」の代わりに何を証明してしまったのか、という核心部分の記述が見当たらない。途中で使われている他の特定の命題については書かれているみたいだけど、メインの結果についてはどうなのかな。

例を見る限り、これは「翻訳ミス」というより、LLMが形式化の過程で証明を微調整してしまったっていうのが近そう。m+4をm+5に変えるのは、自然言語の数学的ステートメントを解析するときに起こるような曖昧さとは次元が違う。

いずれ「意味論の危機」に直面するんだろうか？

2つの失敗モードを想定すると：

• Leanのカーネルにバグがある可能性は常にある。
• 形式化された命題が、数学者が「実際に意図したもの」と一致していない可能性がある。

「証明にミスがあるという議論ができるとしても、解決策よりも問題文の方をチェックする方が明らかに簡単だろう」という議論は自然に思える。

（「素敵な性質」として、エージェントは必ずしも第2の基準に従って「副次的な議論」を正しく行う必要はない。自然言語の証明では形式的なものとは微妙に違う対象を作り出しているかもしれないが、全体としては整合が取れている、といったケースだ。もし「元の命題」が対応していることを保証できれば、残る可能性はLeanのカーネルだけになる。そうすれば無限後退には陥らない）

でも、「定義」ってやつは常に本当に奇妙なもので、うまく説明できる理論が存在しないんじゃないか？問いを表現するのに必要な記述力をどうやって定量化するんだろう？数学において難しいのは定義を正しく決めることであることが多いけど、定義そのものが複雑すぎて検証不可能になり、誰にも何と対応しているか分からなくなったらどうする？面白いことに、歴史の長い数学の問題の多くは「比較的」単純な問題文を持っていて、Leanで簡単に形式化できる場合が多い。でもLeanが特効薬になるのか、それとも底なし沼なのかは確信が持てない。

まあ、AIが「知能」というさらに一般的な性質で爆進し続けている限り、たぶん重要ではないんだろうけど、それでも考えるのは興味深いね。

（まあ、この辺りがAIT（Algorithmic Information Theory）の面白いところなんだけど、それでも一般的な意味論の理論とは言えないと思う。）

論文は、Leanの証明とPDFの文章による証明が完全に一致していないことを示している。でも、Leanが受理した定理がクレイ数学研究所が公開している元の問題文と同等であれば、この不一致は証明自体の正当性には影響しない。ただし「同等であれば」というのは自明ではない。問題を正確に記述することは、往々にして証明することと同じくらい難しいからね。検証作業は、Leanの定理がクレイ数学研究所が公開したものと同等かどうかに集中すべきだ。

とはいえ、Leanの証明とPDFとの間にギャップがあるのは解釈性の面で困るし、解釈性を求めるのは妥当な目的だけど、それは証明の有効性とは別の話だ。

この論文は中身がほとんどない。まず、自然言語はLeanほど正確ではないから、NLの議論をLeanに翻訳する方法は複数存在しうる。図1を見ればわかる通り、LLMは根に関する議論を簡潔に翻訳するという点では、まあまあ良い仕事をしている。

さらに論文では、ナビエ・ストークスのNLでの議論の方がLeanでの議論より強力だと主張している。僕の理解では、翻訳担当のLLMがサボって、それ以上の強力な主張を含めずに定理を満たす最小限のコードを書いただけなんじゃないかな。

数学の論文で「ちなみに、これは実際には[より強力な主張]を証明している」と言うのはよくあることだけど、正確に翻訳することを目標とするAIなら、そんなことは絶対にしない。AIの目的は証明の翻訳であって、数学の質を上げることではないからね。

論文のこの免責事項は知っておく価値があるよ。

「免責事項：我々はOpenAIのNL証明の正当性について主張するものではなく、Leanへの翻訳ミスについてのみ言及している。」