論文「Towards Language Model Guided TLA+ Proof Automation」の技術的サマリー

本論文は、形式検証言語である TLA+ における定理証明の自動化を、大規模言語モデル（LLM）の推論能力と記号論理証明器（Symbolic Prover）の検証能力を組み合わせることで実現する新しいアプローチ「LMGPA (Language Model Guided Proof Automation)」を提案するものです。

以下に、問題定義、手法、主要な貢献、実験結果、および意義について詳細にまとめます。

1. 背景と問題定義

背景

TLA+ は、分散システムや並行アルゴリズムの仕様記述と検証に広く用いられている形式言語です（Amazon、Intel、Microsoft などが採用）。TLA+ の証明システム（TLAPS）は、モデル検査だけでなく、無限状態系を含む定理証明も可能ですが、証明の構築には高度な専門知識と多大な労力が必要です。

既存の課題

近年、Lean や Rocq（Coq）などの「戦術（tactic）ベース」の定理証明器において、LLM を用いた証明自動化が進展しています。しかし、TLA+ への直接適用には以下の重大な課題がありました。

1. 証明構造の根本的な違い:
   • Lean/Rocq: 証明状態を戦術（コマンド）の連続で変換していく「戦術ベース」のアプローチ。
   • TLA+: 複雑な主張（Claim）を、中間的なサブ主張（Sub-claims）の階層的な木構造として分解・構築する「階層的（Hierarchical）」アプローチ。
   • この構造の違いにより、戦術ベースで成功した LLM の手法をそのまま TLA+ に適用することは困難です。
2. 構文エラーの多発: 既存の LLM は、TLA+ の厳密な構文ルールに従わず、他の証明器（Isabelle など）の構文と混同した誤った証明を生成しがちです。
3. データ不足: Lean や Coq に比べて、TLA+ の形式化された証明データセットが不足しており、学習ベースのアプローチの構築が困難です。

2. 提案手法：LMGPA

著者らは、LLM の「推論・分解能力」と、TLAPS などの「厳密な検証能力」を組み合わせるハイブリッドアプローチを提案しました。

核心的なアイデア

LLM に「完全な証明」を生成させるのではなく、「正規化された主張の分解（Normalized Claim Decomposition）」のみを生成させることに制限を設けます。

• 階層的再帰分解: 複雑な証明義務（Proof Obligation）を、LLM がより単純なサブ主張（サブゴール）に分解します。
• 記号証明器による検証: 生成されたサブ主張が親主張を論理的に導くか、またサブ主張自体が TLAPS（Z3, Zenon, Isabelle などのバックエンド）によって検証可能かを確認します。
• 再帰的適用: 検証されたサブ主張に対して、同じプロセスを再帰的に適用し、最終的にすべてが「自動証明（OBVIOUS や BY DEF など）」で検証可能なレベルまで分解されるまで続けます。

システムの主要コンポーネント

1. LLM による主張分解 (Claim Decomposition):
   • LLM には、特定の正規化された形式（ASSUME-PROVE 構造、ASCII 記号のみの使用、自由変数の明示的な宣言など）に従ったサブ主張リストを生成させます。
   • これにより、TLA+ の構文エラーを大幅に削減します。
   • 検証失敗時には、エラーメッセージをフィードバックとして LLM に返し、分解の修正を促します。
2. 自動証明生成 (Symbolic Auto Proof Generation):
   • 単純な主張に対しては、LLM を使わず、TLA+ の指示（OBVIOUS や BY DEF）をヘuristic 的に生成し、TLAPS に直接検証させます。
3. 検証ループ:
   • 分解の妥当性（親主張がサブ主張から導かれるか）と、個々のサブ主張の証明可能性を TLAPS で確認します。

3. 主要な貢献

1. TLA+ 固有の証明構造に適合した LLM 活用手法の提案:
   • 戦術ベースの証明器とは異なる TLA+ の階層的構造に対応し、LLM に「完全な証明」ではなく「論理的な分解」のみを担わせることで、構文エラーと論理的破綻を同時に抑制しました。
2. 大規模ベンチマークの構築:
   • 数学定理（miniF2F, ProofNet から 93 件）と、分散プロトコルの帰納的不変量証明（26 件）を含む、合計 119 件の TLA+ 定理からなるベンチマークスイートを構築しました。
   • これらの定理は、他の形式言語から手動で TLA+ に翻訳・適応されました。
3. 高い証明成功率の実証:
   • 複数の最先端 LLM（Claude 3.7, GPT-5, o3-mini など）を用いた実験において、既存の手法（直接 LLM 生成や単純な記号証明）を凌駕する性能を示しました。

4. 実験結果

ベンチマーク（分散プロトコル 26 件、数学定理 93 件）を用いた評価結果は以下の通りです。

• 証明成功率:
  • LMGPAは、すべてのテストされた LLM において、ベースライン（単純な TLAPS 実行や直接 LLM 生成）を上回る成功率を達成しました。
  • 例：Claude 3.7 Sonnet を使用した場合、分散プロトコルベンチマークで 42.3%、数学ベンチマークで 53.8% の証明に成功しました。
  • 対照的に、直接 LLM に証明を生成させる手法（DLPG）は、構文エラーにより成功率が極めて低く（例：Claude で分散プロトコル 15.4%、数学 17.2%）、多くの失敗が構文エラーに起因することが示されました。
• 構文の正当性:
  • LMGPA が生成する「分解（サブ主張）」の構文正当性は 65%〜86% であり、直接証明生成（DLPG）の 0.2%〜20% に比べて劇的に改善されました。これは、正規化された形式への制約が有効であることを示しています。
• 効率性:
  • 完全な証明を生成するよりも、分解のみを生成する方が LLM のトークン消費や処理時間が抑えられ、全体としての処理時間が短縮される傾向がありました。

5. 意義と将来展望

意義

• 形式検証の民主化: TLA+ 証明の構築における専門知識の壁を下げ、より多くのエンジニアが形式検証を利用できる可能性を開きました。
• LLM と記号論理の協調: LLM の「創造的・分解的」な能力と、記号証明器の「厳密な検証」能力を、それぞれの得意分野で組み合わせる有効なパターンを示しました。
• 構文エラーの克服: 生成 AI が形式言語で直面する最大の障壁の一つである構文エラーを、出力形式の制約（正規化）によって効果的に回避する手法を確立しました。

限界と将来の課題

• 分解の質: 生成された証明は論理的に正しい場合もありますが、人間が書くような「簡潔で自然な」証明とは異なる場合があり、不要なサブ主張を生成する傾向が見られました。
• 証明器の限界: LLM が論理的に正しい分解を行っても、TLAPS が時間制限（タイムアウト）内で検証できないケースが存在します。
• 将来の方向性:
  • TLA+ 証明データセットでの LLM のファインチューニング。
  • 記号証明器の能力や限界を理解し、それに基づいた分解を誘導する高度なプロンプト戦略や検索強化生成（RAG）の適用。
  • 漏洩のない新しいベンチマークの構築。

総じて、本論文は TLA+ における LLM 支援証明自動化の現状を大きく前進させ、形式検証の実用化に向けた重要なステップを示すものです。