論文の概要: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
- arxiv url: http://arxiv.org/abs/2610.08144v1
- Date: Tue, 06 Oct 2026 10:58:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-08 02:58:29.946699
- Title: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
- Title（参考訳）: Navier-Stokesが翻訳で失われた: なぜAIの自動形式化のリーン検証は、正しい自然言語証明を保証しないのか
- Abstract要約: オートフォーマル化は数学のテキストの検証にますます利用されている。
このプロセスでは、AIシステムはテキストを自然言語(NL)からリーンのような形式言語に変換する。
この記事では、このプロセスが元のNL引数に信頼を与えない理由を示す。
- 参考スコア（独自算出の注目度）: 42.75912362270511
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully. In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy/arithmetical hierarchy (the SCI $= \infty$). Hence, informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem (which has SCI $= 1$). To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
- Abstract（参考訳）: OpenAIが発表したNavier-Stokes方程式に対する解の爆発の証明のように、AIによって生成されたものを含む数学的テキストを検証するために、自動形式化がますます使われている。
このプロセスでは、AIシステムがテキストを自然言語(NL)からリーンのような形式言語に変換する。
この翻訳が完了すると、形式言語で表現された議論は機械的に容易に検証できる。
本稿の目的は、翻訳を意味的に忠実に行うのに様々な困難があるため、このプロセスが元のNLの議論に不信感を与える可能性を実証することである。
特に、意味論的に忠実な翻訳を提供するために必要となる数学的NLテキストの曖昧さを解消する問題は、ソルビビリティ複雑度指数(SCI)階層/パラメータ階層(SCI$= \infty$)において任意に高い。
したがって、非公式に、意味的に忠実なAIオートフォーマル化を提供することは、ハルティング問題(SCI$=1$)を含むあらゆる計算問題よりも難しい。
この結果の効果を示すために、私たちは、AIによるNL文と証明をリーンに誤訳する例をいくつか提供します。
その中にはOpenAIが発表したNavier-Stokesの証明も含まれている。
特に、形式化されたリーン証明は、ナヴィエ・ストークス方程式に対する解の爆破のNL証明と一致しないことを示す。
関連論文リスト
- Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification [13.942115092285697]
リーンシグナルを推論プロセスに統合することで、非公式な推論と公式な推論のギャップを埋めます。
トレーニング不要のエージェントパイプラインであるMagentaを紹介します。これは、自然言語の問題のみを与えられた上で、回答を生成し、Lean 4ステートメントとして表現し、マシンチェックされた証明を構築します。
論文 参考訳（メタデータ） (2026-09-10T09:48:07Z) - Invariant Discovery for Networked Systems [42.16790126199371]
不変性は、検証からトラフィック生成、テレメトリ計算、入力検証に至るまでの応用の基盤となる。
自動採掘機は2つの面で不足するが、最も難しい入力(許容不変量の文法)が必要であり、正確な「難しい」ルールしか学ばない。
我々のキーとなる考え方は、不変探索問題をAIによる文法発見問題に分割し、次いで学習文法における統計駆動探索問題に分割することである。
論文 参考訳（メタデータ） (2026-07-24T23:07:31Z) - ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。
LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。
本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
論文 参考訳（メタデータ） (2026-04-07T19:33:54Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。
中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。
我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
論文 参考訳（メタデータ） (2025-10-17T14:20:50Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。
既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
論文 参考訳（メタデータ） (2024-12-20T17:19:24Z) - Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。
LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。
これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
論文 参考訳（メタデータ） (2024-03-26T22:01:13Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。