技術要約：Visored：LLMが生成する数学のための制御自然言語プロバー

問題提起

大規模言語モデル（LLM）は数学的推論において高い能力を示しているが、依然として幻覚（ハルシネーション）に陥りやすい。その結果、AIが生成した証明の信頼性は、検証プロセスがいかに強力かに依存することになる。自動定理証明器（ATP）や、LeanやRocqを対象とした全証明モデル（whole-proof models）は、miniF2Fのようなベンチマークで高い合格率を達成しているが、これらは通常、既に形式化された命題を入力として必要とする。決定的なボトルネックは、自動形式化（autoformalization）、すなわち非形式的な数学の散文を、機械検証可能な形式へと翻訳するプロセスにある。

この翻訳は容易ではない。なぜなら、非形式的な数学は、共有された背景知識、暗黙的なサイド条件（例：$x \neq 0$）、および読者が自動的に補完する表記上の濫用（notational abuse）に依存しているからである。形式言語への直接的な翻訳には、ソーステキストには一切残らない特定のライブラリの補題、部分型（subtypes）、エッジケースの慣習、および強制（coercions）（例：$\mathbb{N}$ か $\mathbb{Z}$ か $\mathbb{R}$ か）へのコミットメントが求められる。これらの決定におけるエラーは、コンパイラエラーとして現れるのではなく、「静かな意味的ドリフト（silent semantic drift）」として現れる。つまり、文自体はコンパイル可能であるが、元の意図を反映していない状態である。

手法

Visoredは、LaTeXとLeanのような低レベルなプロバーの間に、**依存型中間表現（IR）**を導入することで、非形式的な数学の記述と形式検証の間の溝を埋めるために設計された研究用プロトタイプである。

コア・アーキテクチャ

システムは、以下のステージで構成されるパイプライン（図2参照）として動作する：

1. 制御自然言語（CNL）入力： Visoredは、LaTeXに埋め込まれた数学的英語の制御されたサブセットを受け入れる。語彙（「Let...」、「Assume...」、「Then...」といった文テンプレートやLaTeXコマンド）は、外部の .lpcsv 仕様ファイルによって定義されており、これにより、パーサーを修正することなく表面言語を拡張できる。
2. 構文と意味論： 入力は構文木へと解析され、その後、**型付きAST（sem AST）**へと精緻化（elaboration）される。この段階で、名前の解決、型と種の割り当てが行われ、**定義の妥当性（well-definedness）**が型チェック時に強制される。PVSの伝統に従い、部分関数（例：$1/x$, $\sqrt{x}$, $\log x$）は、式が受理される前に、暗黙の仮定引数（例：$x \neq 0$, $x \ge 0$）を伴う。
3. 中間レベルIR（MIR）： 型付きASTは、ソルバーの基盤となるVisored MIRへと低レベル化される。
4. コスト制限付きソルバー： ソルバーは、「Then...」による義務および定義の妥当性を、ルール駆動型のコスト制限付きエンジン（名称：「Miracle」）を用いて解消する。これは、数学者が通常省略する日常的なステップを閉じるために、後方および前方ルールのデータベース（ProofGraderに着想を得たもの）と、特化したタクティクス（例：代数的正規化器、チェインソルバー）を用いる。
5. オプションのLeanエミッション： 受理された証明は、Lean 4へとトランスパイル可能である。これは外部カーネル検証のためのオプションのダウンストリーム・ステージである。トランスパイル・プロセスには、正規化履歴の再生と、数体系間の強制の証拠（coercion witnesses）の管理が含まれる。

設計思想

Visoredは、主に2つの観察に基づいて構築されている：

1. LLMの流暢性： LLMは圧倒的に非形式的な数学で学習されている。CNLの表面表現は、LLMがすでに流暢である領域に近い状態を維持するため、モデルが低レベルなプロバーの構文（タクティクス、ライブラリの補題名など）をゼロから学習する必要を回避できる。
2. 実行可能性： 自然な推論と形式的な推論の架け橋を作ることは、完全な自動定理証明を行うよりも実行可能である。LLMにCNLによる証明の概要を提供させることで、ソルバーは小さな、明白なステップを閉じることだけに集中でき、これは現代のエージェント・エンジニアリングにとって十分に手の届く範囲のタスクである。

本システムは、「上方向」の意味解析（LaTeX $\to$ Visored）をLLMが扱う困難な問題とし、「下方向」の投影（Visored $\to$ Lean）を決定論的かつ機械的なプロセスとして扱う。

主な貢献

• 自動形式化のための依存型IR： Visoredは、LaTeXの表面には痕跡を残さないあらゆる決定（部分型、ライブラリの補題、エッジケースの慣習、キャスト）を明示的に扱う、意味的に豊かなIRを導入している。
• 仕様駆動の拡張性： CNLの表面はハードコードされたパーサーではなく、外部設定ファイルによって定義されているため、システムを再コンパイルすることなく、特定の数学的慣習（教科書、競技数学、研究）に合わせて語彙を調整できる。
• 局所的な診断： 全体のLeanコンパイル後に単一のaccept/rejectの判定を下すシステムとは異なり、Visoredは精緻化または求解の段階で局所的な診断を提供する。これにより、LLMが特定のエラーを特定して修正できる「検証および修正（verify-and-revise）」のループが可能になる。
• 定義の妥当性の強制： システムは、ターゲットとなるプロバーの全単射化（totalization）の慣習に頼るのではなく、ソルバーによって解消される暗黙の仮定引数を通じて、定義の妥当性（例：$1/x$ の前に $x \neq 0$ であることの保証）を強制する。
• 既存の学派の統合： Visoredは、Mizar/Naproche（CNL表面）、PVS（型チェック時の定義の妥当性）、Lean/Rocq（依存型）、およびProofGrader（コスト予算付きのルール駆動型求解）の要素を、単一のLLM向けパイプラインへと統合している。

実験結果

著者らは、開発および評価セットの両方として使用した miniF2F-valid 分割（244問）に関するカバレッジ調査を報告している。

• パフォーマンス： CNL表面を記述したスキルドキュメントに導かれたLLMコーディングエージェント（Claude）は、**244問中222問（91%）**のVisored検証済み証明を生成した。
• 内訳：
  • 帰納法（Induction）: 100% (8/8)
  • 代数学（Algebra）: 98% (86/88)
  • 数論（Number Theory）: 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (オリンピアード数学): 35% (7/20)
• 失敗分析： 未解決の問題は、LLMの証明戦略を見つける能力の欠如ではなく、Visoredのルールデータベースの欠落（例：相加相乗平均（AM-GM）不等式の欠如、有限体の型の欠如、三角関数の恒等式など）や、プロトタイプの退行に起因するとされている。著者は、エージェントがこれらを解けなかったのは、必要な「仕組み（machinery）」がまだシステムに実装されていなかったためであると明言している。
• トランスパイル・コスト： 現在の疎なエミッション方式は、非常に冗長なLean出力を生成し、手書きのLean証明と比較して中央値で $\approx 250\times$、最大で $\approx 25,000\times$ の行数比となる。これは、正規化ステップと強制の証拠の再生によるものである。

意義と主張

本論文は、Visoredを競争力のある自動定理証明器としてではなく、AIが生成する非形式的な数学を検証し整理するための**新しいインフラストラクチャの概念実証（PoC）**として位置づけている。

• 控えめな主張： 著者らは、競争力のある自動定理証明を主張しているわけではなく、また、保持されたテスト分割（held-out test splits）へ結果を外挿することもしていない。91%のカバレッジは、設計が表現できる能力の下限として提示されており、調整された合格率ではない。
• ボトルネックの転換： 本研究は、AI数学における制約が、「アイデアの生成」から「それらをスケールして検証し、整理すること」へと移行しているという見解を支持している。
• ユーティリティ・モード： Visoredは以下の4つのモードで機能するように設計されている：
  1. 推論時の検証器： LLM出力のリアルタイムチェッカー。
  2. 自動形式化ループ： 局所的な診断に基づいてLLMが証明を書き換えるためのメカニズム。
  3. 高密度な報酬信号： 強化学習（RL）のためのステップごとのフィードバック提供。
  4. CNLデータジェネレータ： 再生可能な、形式的に検証された、自然に読める証明のコーパスの作成。

結論として、CNLの表面、依存型IR、およびルール駆動型ソルバーの組み合わせは、失敗が局所化され、かつ実行可能なアクションにつながるパイプラインを構築しており、現在の直接的な自動形式化アプローチよりも、非形式的な散文からカーネル検証された証明へのより信頼できる経路を提供している。未解決の問題は、設計の根本的な限界ではなく、不足しているルールや仕組みのバックログを表している。