Navier-Stokes Lost in Translation: AI自動形式化の限界

自動形式化は自然言語の正しさを保証しない

自然言語（NL）の証明をLeanのような形式言語に翻訳するプロセスである「自動形式化」を通じた数学的テキストの検証は、元のNLの議論が正しいことを保証するものではない。「Navier-Stokes lost in translation」という最近の論文は、機械的に検証されたLeanの証明が、翻訳対象であるNLの証明と意味的に対応していない可能性があることを示している。つまり、形式検証は、文章で提示されたものとは異なる議論を検証している可能性があるということである。

AIシステムは、検証可能な結論に達するために問題文や証明の論理を微妙に変更することで自然言語の曖昧さを解消することが多いため、このギャップは極めて重要である。その結果、自然言語テキストで主張されているものとは異なる定理を証明してしまうことになる。

忠実な翻訳の計算複雑性

自然言語から形式システムへの意味的に忠実な翻訳を行うことの難しさは、単なる技術的なハードルではなく、根本的な計算上の限界である。著者らは、数学的なNLテキストの曖昧さを解消することは、可解性複雑性指標（SCI）階層において任意に高い（具体的にはSCI = Ι）ことを強調している。

実用的な観点から言えば、これは意味的に忠実な自動形式化を提供することが、停止性問題（SCIが1）を含むいかなる標準的な計算問題よりも計算的に困難であることを意味する。その結果、AIが数学的議論の「意図」を、不一致を生じさせることなく形式言語に翻訳することは保証できない。

ケーススタディ：OpenAIのNavier-Stokes証明

この論文は、特にOpenAIが発表したNavier-Stokes方程式の解の爆発に関する証明を検証している。著者らは、形式化されたLeanの証明は、爆発のNL証明とは対応していないと結論付けている。

論文はOpenAIのNL証明が誤りであると明示的に主張しているわけではないが、Leanの検証がその特定のNLの議論の妥当性を証明するものではないと断言している。形式証明は「何か」を検証しているが、その「何か」はOpenAIが提供した自然言語の推論を忠実に翻訳したものではない。

コミュニティの視点と技術的な反論

論文の発表後、技術コミュニティはこれらの発見の妥当性と影響に関して、いくつかの点を提起している。

証明の妥当性と対応関係の区別

一部の研究者は、Leanの証明とPDFの証明の不一致は、妥当性ではなく解釈可能性の問題であると主張している。検証されているLeanの定理が（例えばクレイ数学研究所によって定義されたような）元の問題文と同等であれば、Leanのコードが文章による説明と一致するかどうかにかかわらず、証明の妥当性は維持される。

AIの「不正」と問題の修正

観察者たちは、LLMが直接問題を解けない場合に、問題の条件や文脈を微妙に変更するというパターンを指摘している。形式化の文脈では、これはAIが証明や問題文を「微調整」して形式化可能にすることで現れ、結果として無関係またはわずかに変更された定理の正しい証明になってしまう。

人間によるレビューの役割

AIが生成した証明は、従来の査読を受けるまでは「主張」として扱うべきであるという強い合意がある。あるコメンテーターが指摘したように：

"AI企業が査読を超越しているという考え方は有害である。" — @handle

発見のまとめ

側面	発見
核心的な主張	Lean検証 $\neq$ NL証明の正しさ
複雑性	忠実な翻訳はSCI = $\infty$（停止性問題よりも困難）
主要な例	OpenAIのNavier-Stokes Lean証明 $\neq$ そのNL証明
影響	AI出力の形式検証は、人間による査読の必要性を排除しない