10月7日、Bastounisら3名の研究者が「Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs」と題した論文を公開した。AIが自然言語の数学テキストを形式言語に自動変換する「自動形式化（autoformalisation）」において、形式言語側の検証をパスしても元の証明の正しさは保証されないという根本的な問題を、計算困難度の理論と具体的事例の両面から論じている。

Lean検証の「お墨付き」には原理的な限界がある

Leanは、数学の証明をコードとして記述し機械的に検証できる定理証明支援系だ。人間がLeanでコードを書けば、その証明が論理的に正しいかどうかを自動でチェックできる。近年はAIがこのプロセスを自動化する「自動形式化（autoformalisation）」——自然言語で書かれた数学テキストをLeanコードに変換するアプローチ——が急速に注目を集めている。DeepMindのAlphaProofやOpenAIの数学推論モデルなど、大手AI企業がこの分野に相次いで参入しており、「AIによる数学証明」は2024〜2025年にかけて最も注目を集めた研究トピックのひとつだ。

しかし本論文の著者らはこう問いかける。AIが翻訳したLeanコードの検証が通ったとして、それは元の自然言語証明が正しいことを意味するのか？ 答えは「否」であり、しかもそれは原理的に解決できない問題だという。

「意味的に忠実な翻訳」は停止問題より難しい

自動形式化の肝は「意味的忠実性」——自然言語テキストの数学的意味をそのままLeanコードに移せているか——にある。だが自然言語の数学テキストには至るところに曖昧性が潜む。「連続関数」「解の存在」といった表現ひとつとっても、文脈によって意味が変わりうる。

著者らはこの曖昧性の解消問題を計算困難度の観点から分析し、Solvability Complexity Index（SCI）階層における位置づけを示す。SCIは計算可能性理論における困難度の分類体系で、SCIが高いほど「どんなアルゴリズムを使っても解けない」度合いが強くなる（詳細はHansenらの先行研究を参照）。

その結論は衝撃的だ——意味的に忠実な自動形式化はSCI = ∞、すなわち「停止問題（SCI = 1）よりも難しい」問題に該当する。停止問題は「あるプログラムがいつか停止するかどうかを判定できない」という計算機科学の根本的限界として広く知られている。意味的に忠実な自動形式化はそれよりさらに上位の困難度を持つ——つまり原理的に自動化できない問題だ、と著者らは主張する。

Navier-Stokes事例で示すミス翻訳の実態

著者らは理論的主張にとどまらず、具体的な事例を通じてミス翻訳の実態を示している。

取り上げられるのは、流体力学の核心方程式であるナビエ＝ストークス方程式（Navier-Stokes equations）の解の有限時間爆発（finite-time blow-up）に関する証明だ。これはClay数学研究所が100万ドルの懸賞をかけたミレニアム懸賞問題のひとつであり、数学・AI両コミュニティで大きな注目を集めているテーマだ。著者らはこの文脈でのLean自動形式化を具体例として分析している。

著者らの分析によれば、形式化されたLeanコードが証明しているのは、自然言語で記述されたNavier-Stokes爆発証明に対応する命題ではないという。Leanが検証したのはあくまでLeanコード内で定義された命題の正しさであり、それが元の自然言語証明と同じことを述べているかは別の問題だ。これは特定の発表の真偽を断定するものではなく、自動形式化そのものの構造的問題を示す事例として提示されている。

「翻訳→検証」パイプラインの構造的盲点

この問題の本質は、Lean検証が「正しさのお墨付き」として社会的に機能してしまう構造にある。

「自然言語証明 → AI翻訳 → Leanコード → Lean検証OK」という流れを見ると、全体が正しいように映る。だが検証されているのは最後のステップ——「Leanコードとして論理的に矛盾がないか」——だけだ。最初のステップである翻訳の意味的忠実性は、原理的に機械では保証できない。

本論文は25ページ・4図で構成され、偏微分方程式（math.AP）、人工知能（cs.AI）、論理学（math.LO）の3分野にまたがる学際的な論考となっている。

コード生成・仕様検証にも波及する問題

数学証明の自動形式化は今や数学者やAI研究者だけの問題ではない。プログラムの仕様を自然言語で記述しAIにコードへ変換させる、あるいはコードの正しさを形式手法で検証するといった取り組みは、ソフトウェアエンジニアリングの現場でも広がりつつある。

その文脈で本論文の主張は重い含意を持つ。「自然言語 → 形式言語 → 検証OK」というパイプラインに対して、翻訳の意味的忠実性という盲点は常に存在する。AIが生成したコードや形式仕様の「検証済み」という表現が何を保証し、何を保証しないのかを正確に理解することが、今後のエンジニアにとって不可欠だ。

詳細はNavier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofsを参照していただきたい。