LeanによるAI自動形式化は自然言語証明の正しさを保証しない

私の理解が正しければ、これは自然言語による証明とLean証明の等価性を疑問視しているのであって、Lean証明の正しさを疑問視しているのではないのか？

Navier-Stokesとは何かを一言で思い出すためのリンク：https://p.migdal.pl/equations-explained-colorfully/#navier-s...

この論文はほとんど何もない。まず、自然言語はLeanほど正確ではないので、自然言語の議論をLeanに翻訳する方法は複数ある。図1に示されているように、LLMは根に関する議論を簡潔な方法で翻訳するのにかなり良い仕事をした。

さらに、この論文はNavier-Stokesの自然言語による議論がLeanのものより強いと主張している。私の理解では、翻訳LLMが怠けて、余分なより強い主張を含めずに定理を満たす最小限のコードを書いたのだ。

数学の論文では「ちなみに、これは実際には[より強い主張]を証明している」と言うのはよくあることだが、翻訳という明確な目標を持つAIは決してそうしない。その目標は証明を翻訳することであり、質の高い数学をすることではないからだ。

この論文は、Lean証明と散文（PDF）証明が正確に一致しないことを示している。しかし、Leanが受け入れたLean定理がClay研究所が発表した元の問題文と等価であれば、この不一致は証明自体の妥当性には影響しない。これは些細な「もし」ではない：問題を正確に述べることは、しばしば証明と同じくらい難しい。検証の取り組みは、Lean定理がClay研究所の発表したものと等価であるかどうかに集中すべきだ。

とはいえ、Lean証明とPDFの間のギャップは解釈可能性にとって厄介であり、解釈は正当な目的だが、それは証明の妥当性には関係しない。

意味の理論の危機にいつか直面するのだろうか？

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

- Leanカーネルには常にバグがある可能性がある。

- 形式化された文が、数学者が「実際に望んだ」ものに対応しない可能性がある。

「たとえ証明に誤りがあり得るとしても、解よりも問題文をチェックする方が確かに簡単だ」という議論をするのは自然に思える。

（「良い性質」とは、エージェントが2番目の基準に従って「副議論を正しく」する必要すらないということだ - おそらく自然な証明では形式的なものとは微妙に異なる対象を発明するが、すべてチェックは通る。元の文が対応することを保証すれば、唯一の可能性はLeanカーネルだけだ。したがって、この場合は無限に再帰しない。）

しかし、「定義」は常に本当に奇妙なもので、良い理論があるとは思えない？質問を表現するのにどれだけの記述力が必要かをどう定量化するのか？数学ではしばしば難しいのは定義を正しくすることだが、定義自体が非常に複雑で検証不可能になり、誰もそれを何かに対応させられなくなったらどうなる？まあ、多くの興味深い長年の数学の問題は「比較的」単純な問題文を持っていて、簡単にLeanに形式化できるように思えるが、Leanに本当に特効薬があるのか、それとも亀がどこまでも続くのかはわからない。

AIが飛躍的に進歩し続ける限り、おそらく問題にはならない […]

例の高レベルな説明を考えると、これは「誤翻訳」というよりは、LLMが形式化する際に証明を微調整したものだと思う。m+4とm+5の間を行き来するのは、自然言語の数学的記述を解析する際に一般に生じるような曖昧さとはかなり違う。

うーん、ここを見ても、OpenAIが強制項付きのNavier-Stokes爆発の代わりに実際に何を証明したのかは述べられていないようだ。途中で使われる他の特定の文についてはそうしているが、主要な結果についてはそうではない。