技術的概要：自動形式化のための参照不要な単調性向上リファインメント

1. 問題定義

大規模言語モデル（LLM）は数学的推論を進展させたものの、完全定理の自動形式化—すなわち、自然言語の定理とその付随する証明を、機械的に検証可能な完全な形式化された定理と証明へ変換すること—は依然として十分に研究されていない。既存のアプローチは、しばしば証明部分に「sorry」というプレースホルダーを依存させ、宣言の形式化のみに焦点を当てたり、宣言生成と定理証明を分離されたタスクとして扱ったりしている。

高品質な自動形式化の核心的な課題は、その多次元的な性質にある。成功する形式化は、同時に以下の条件を満たさなければならない：

1. 形式的妥当性（FV）： 定理証明器（例：Lean4）による構文の正しさと機械的検証。
2. 論理的保存（LP）： 元の自然言語表現の論理構造との意味的整合性。
3. 数学的一貫性（MC）： 数学的対象と演算の正確な表現。
4. 形式品質（FQ）： 構造的明瞭性、簡潔性、再利用性。

現在の反復的リファインメント手法は、これらの次元を共同で最適化するのに苦慮しており、ある側面（例：構文）を改善する代わりに他の側面（例：意味的整合性）を犠牲にすることが多い。さらに、既存の手法はしばしば真の形式化データ（グラウンドトゥルース）や人間の選択に依存しており、参照不要な設定での適用性を制限している。

2. 手法

著者は、グラウンドトゥルース形式化や人間の選択へのアクセスなしにテスト時に動作する、参照不要で反復的かつ単調な最適化プロセスを提案する。このフレームワークは、定理証明器からのフィードバックと LLM ベースのジャッジからのフィードバックを統合し、専門化された LLM のアンサンブルを導く。

2.1 目的関数

著者は、4 つの次元をバランスさせるためにマスク付き複合目的関数 $J_{OA}(x)$ を定義する。形式的妥当性（$\pi_{FV}$）はハード制約（マスク）として機能し、論理的保存（$\pi_{LP}$）、数学的一貫性（$\pi_{MC}$）、形式品質（$\pi_{FQ}$）はソフト次元として扱われる：
$$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$$
この定式化により、無効な形式化（$\pi_{FV}=0$ の場合）は、ソフトスコアが如何ほどであっても選択されないことが保証される。

2.2 LLM ジャッジと不確実性

ソフト次元は正確に計算することが困難であるため、このフレームワークはスコアを推定するためにLLM ジャッジを採用する。LLM に内在するノイズとバイアスを処理するため、著者は以下を仮定する：

• 漸近的安定性： 較正後、判断は安定する。
• 測定可能な不確実性： 真のスコアに対して片側**下限信頼区間（LCB）**を確立できる。
  目的関数は、LCB ベースの推定量を用いて最適化され、選択決定が保守的であり、評価ノイズに対して頑健であることを保証する。

2.3 生成器の役割と応答性

このフレームワークは、各次元ごとの期待される改善をモデル化する応答性マップによって導かれ、LLM の役割を 3 つのカテゴリに分解する：

1. ワンオフ生成器（OOGs）： 専門的な数学モデル（例：DeepSeek-Prover）など、ゼロから初期形式化を生成する。
2. FV 修復器（FVRs）： 形式的に無効な候補を特定し、修正する（例：反復的な証明修正が可能なモデル）。
3. 再帰的生成器（REGs）： 特定のソフト次元（LP、MC、または FQ）に関する LLM ジャッジからのフィードバックに基づき、現在の最良候補を洗練させる。

2.4 単調受諾ポリシー

このプロセスは、候補の生成と選択を反復する。保守的受諾ポリシーが適用される：新しい候補は、その推定目的スコア（LCB に基づく）が現在の最良のものより厳密に高い場合にのみ受諾される。これにより、認証された単調性向上が保証され、選択された形式化の品質は反復を通じて決して低下しないことが保証される。このプロセスは、特定の条件下で収束し、終了することが証明されている。

3. 主要な貢献

1. 形式的定義とフレームワーク： 本論文は、完全定理の自動形式化を統合されたタスクとして初めて形式的に定義し、それを解決するための参照不要で反復的な単調プロセスを提案する。
2. マスク付き複合目的関数： 形式的妥当性をハード制約として強制しつつ、複数のソフト次元（LP、MC、FQ）を同時に最適化する目的関数の導入。
3. 役割特化型アンサンブル： 自動形式化タスクを OOG、FVR、REG の役割に分解し、特定の品質次元に対して最も効果的な生成器を選択するために応答性マップを活用する。
4. 理論的保証： 認証された単調性、収束、およびプロセスの終了可能性に関する理論的証明の提供。これにより、現実的なジャッジのノイズ下でも進歩が非減少であることを保証する。
5. 実証的検証： このフレームワークが、専門化された LLM と汎用 LLM の強みを効果的に組み合わせ、標準ベンチマークで高品質な結果を達成することを示す。

4. 実験結果

本手法は、Lean4 を使用してminiF2F-TestおよびProofNet-Testで評価された。フレームワークには、DeepSeek-Prover-V2-7B、Goedel-Prover-V2-8B、Seed-Coder-8B、Qwen2.5-7B、およびジャッジとして GPT-4.1-mini を含むモデルのアンサンブルが採用された。

主要な性能指標：

• miniF2F： 100.00% の形式的妥当性と**90.27%**の総合スコアを達成。「完璧な」形式化（すべての次元でスコア 1）の割合は 49.18% に達した。
• ProofNet： 77.96% の形式的妥当性と**52.45%**の総合スコアを達成し、完璧な形式化は 17.74% であった。

比較的知見：

• 単調性対ベースライン： 単調プロセスは、Best-of-k（$k$個の出力をサンプリング）および受諾ポリシーなしの**反復自己リファインメント（ISR）**の両方を大幅に上回った。
• アンサンブル対単一モデル： 単一の強力なモデル（GPT-5.4）は改善を示したが、特定の役割に割り当てられたより小さく専門化されたモデルのアンサンブルは、特に形式的妥当性において優れた性能を達成した。
• 頑健性： 単調な傾向は、異なる LLM ジャッジファミリー（例：Qwen 対 GPT）や人間専門家によって評価された際にも維持され、改善がジャッジのバイアスによるアーティファクトではないことを示している。

5. 意義と主張

本論文は、この仕事が信頼性の高い自動形式化に向けた実用的かつ理論的根拠のある一歩を提供すると主張する。参照不要で動作するこのアプローチは、広範な形式ライブラリが存在しない分野でも適用可能であり、数学や科学の未研究領域の形式化を支援する可能性がある。

著者は、このフレームワークが AI 支援型自動形式化のための原理的な方法論を提供することを強調する：

• 大規模な形式検証パイプラインにおける人間の監視の必要性を軽減する。
• LCB 仮定を通じて判断における不確実性を明示的に定量化し、制御する。
• 相補的な LLM と形式検証器フィードバックを組み合わせることが、証明可能な非減少品質を持つ形式化を生み出すことを示す。

この研究は、計算コストが単一パス推論よりも高いものの、パフォーマンスと安定性の大幅な向上によってそのトレードオフが正当化されると結論づけており、安全で信頼性の高い AI 支援型形式推論に関する将来の研究への道を開く。