ハクソク

世界を動かす技術を、日本語で。

ナビエ–ストークスの翻訳の迷い

2026年10月8日原文(arxiv.org)

概要

  • AIによる数学テキストの自動形式化 の信頼性に関する検討
  • 自然言語から形式言語への翻訳 で生じる意味的忠実性の問題
  • Solvability Complexity Index (SCI) の観点からの困難性の指摘
  • AIによる誤訳実例 とその影響の紹介
  • OpenAIのNavier-Stokes証明 の事例分析

AIによる数学テキスト自動形式化の信頼性問題

  • AIシステム が自然言語（NL）で書かれた数学的議論を Lean などの形式言語へ翻訳する自動形式化プロセス
  • 形式言語に翻訳された後は、 機械的検証 が容易に実施可能
  • しかし、 自然言語の曖昧さ解消 および 意味的忠実性の保持 が大きな課題
  • 翻訳の意味的忠実性を保証するためには、 曖昧さの解消問題 を解決する必要
  • この曖昧さ解消は Solvability Complexity Index (SCI)階層 で極めて高い難易度（ SCI=∞）
  • 計算可能性理論 の観点では、これは Halting Problem（停止問題） （SCI=1）よりも困難
  • 結果として、 AIによる自動形式化 は原文NL議論の信頼性保証にはならない

AIによる誤訳の実例とその影響

  • AIが自然言語の数学的主張や証明をLeanへ誤訳 する事例の紹介
    • NL証明とLean検証結果 の不一致が発生
    • OpenAIによるNavier-Stokes方程式の解のblow-up証明 のケース分析
      • Leanで形式化された証明が NLでの証明と対応しない 実態
  • 他にも複数の 具体的な誤訳例 を提示
    • 数理論理、AI、偏微分方程式 分野での事例
    • 形式検証済み証明 でも、原文の意味を正確に反映していない場合がある

理論的背景と今後の課題

  • 曖昧性解消問題 は 算術階層/SCI階層 で最上位の困難性
  • AI autoformalisation の限界
    • 意味的忠実性の保証 が現状のAI技術・計算理論では不可能
    • 今後の 数学AI研究 や 自動証明支援システム開発 への示唆
  • 形式検証だけではNL議論の正しさを保証できない という認識の重要性

Hackerたちの意見

ナビエ-ストークスについて簡単に説明したいなら、こちらをどうぞ: https://p.migdal.pl/equations-explained-colorfully/#navier-s...

└

これ、めっちゃ素敵！数学を全部色分けできたらいいのにって心から思う！！

└

うーん。これは運動量密度輸送方程式のアイデアを全然説明してないと思う。

もし私の理解が正しければ、これは自然言語の証明とLeanの証明の同等性について疑問を呈しているだけで、Leanの証明の正しさについては言及していないんですよね？

└

Leanの証明が自然言語のものと一致しない場合（AIが問題を解くために生成したもの）、Leanの証明が意図した主張を検証していないってことになるのかな？論文からの引用ですが、「3つ目の可能性は、NL証明が正式証明が実際に確立するよりも強い主張を提供することで、（もちろん）異なる証明があるということです。後者はOpenAIが発表したナビエ-ストークス方程式の爆発の証明で起こります。」

└

Leanの証明が正しいかどうかは簡単に確認できるけど、私たちが気にしていることを証明しているかどうかはずっと難しいよね。コードがコンパイルできたとしても、バグがないとは限らないし。

└

そうそう、まさにその通り。AIには自然言語版の証明を正しくするための本当のプレッシャーはないし、自動的に判断する方法もないからね。

└

うん、そうだね。証明しやすい非同等の主張がたくさんあるから。だからLeanは何かを証明しているけど、その何かが実際に私たちが気にしていることなのか、もしくは似たようなもので、最終的には質問とは違うのかってことが問題なんだよね。

└

彼らもNL証明にエラーを見つけたわけではないみたいで、ただ違うだけってことなのかな？

└

確かに。自然言語の証明は間違ってるけど、Leanの証明は正しいね。人間も似たようなミスをすることがある。人間が物事の仕様を書いて、それをコードに翻訳するけど、コードがうまく動かなくて、最終的に人間がコードを修正するけど、元の仕様を直すのを忘れちゃうんだよね。

└

そうだね、自然言語の証明と形式的な証明が「対応する」かどうかは主観的な問題だよ。

AIについてのいつものもめごとを除けば、衝撃的な主張はこれだね。「特に、我々は形式化されたLeanの証明がナビエ-ストークス方程式の解の爆発に関するNL証明に対応していないことを示します。」だから、この著者たちはOpenAIがナビエ-ストークスを本当に証明していないと主張しているようだ。彼らの考えを正しく理解できていれば、LLMがナビエ-ストークスの元の「自然言語」のアイデアを正しく形式化していないと主張しているんだ。もしそれが本当なら、彼らの主張するLeanの証明はナビエ-ストークスの証明ではなく、元の自然言語のアイデアの間違った翻訳に過ぎないことになる。もし正しければ、これはかなり大胆な主張で、他の研究者たちがどう思うか見てみたいな。

Hacker Newsで議論の続きを見る