VeriSoftBench: Lean 向けリポジトリ規模の形式検証ベンチマーク

本論文は、大規模言語モデル（LLM）を用いた対話型定理証明（Interactive Theorem Proving: ITP）の自動化において、既存の数学中心のベンチマークでは捉えきれない「ソフトウェア検証」特有の課題を評価するための新しいベンチマーク**「VeriSoftBench」**を提案したものです。

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

1. 問題設定と背景

既存ベンチマークの限界

現在の Lean における LLM ベースの証明自動化のベンチマーク（MiniF2F, ProofNet, LeanDojo, PutnamBench など）の多くは、Mathlib（Lean の標準数学ライブラリ）に依存した数学的な定理証明に焦点を当てています。これらの環境では、証明対象は広く共有された安定した抽象化（Mathlib の定義や補題）に基づいています。

しかし、ソフトウェア検証やプログラミング言語のメタ理論における証明は、状況が異なります。

• プロジェクト固有の抽象化: 検証対象（コンパイラ、プロトコル、ドメイン固有言語など）に合わせて、プロジェクト内で独自に定義されたデータ型、操作、不変条件が多用されます。
• リポジトリ規模の依存関係: 証明は単一のファイルに完結せず、複数のファイルにまたがる複雑な依存構造（クロスファイル依存）を持ちます。
• コンテキストの重要性: 証明を完了するには、プロジェクト固有の定義や、それらが連鎖的に依存する多数の補題を正しく検索・利用する必要があります。

核心的な問い: 「Mathlib 中心の数学タスクで高性能な証明器が、プロジェクト固有のライブラリや大規模なリポジトリ依存関係が存在する環境でも汎用化できるのか？」

2. 提案手法：VeriSoftBench

このギャップを埋めるため、著者らはVeriSoftBenchを開発しました。

データセットの構成

• 規模: 500 の Lean 4 証明義務（タスク）。
• ソース: 23 のオープンソース形式手法リポジトリ（コンパイラ正しさ、言語意味論、型システム、ゼロ知識回路など）から抽出。
• 特徴:
  • 元の Git コミットから抽出し、プロジェクト固有の抽象化やクロスファイル依存関係を維持したままパッケージ化。
  • 証明の正解スクリプト（Ground-truth）が存在し、かつ sorry（証明の穴）を含まないもののみを選択。
  • 単なる simp や omega などの標準自動化で解決できない、非自明なタスクに限定。

コンテキスト設定（評価条件）

証明器がリポジトリの文脈をどのように利用するかを分析するため、2 つの異なるコンテキスト設定で評価を行いました。

1. Curated Context（キュレーション済み文脈）:
   • 正解の証明に必要な依存関係（定義や補題）に焦点を当てた、最小限の依存集合を提供。
   • 証明の本体（proof body）は隠蔽し、宣言部分のみを提供（データリーク防止）。
   • 「必要な情報が既に特定されている」理想状態に近い設定。
2. Full Repository Context（フルリポジトリ文脈）:
   • タスクファイルだけでなく、リポジトリ内のすべてのファイル（定義、補題、定理の宣言）をコンテキストとして提供。
   • 実際の開発現場に近い「ノイズの多い」環境。
   • 一部のタスクではコンテキストが数百万トークンに達し、モデルのコンテキストウィンドウを超えないようトリミング処理も実施。

3. 主要な貢献

1. VeriSoftBench の提案: 500 の Lean 4 証明義務からなる、オープンソース形式手法リポジトリから抽出された初のベンチマーク。プロジェクト固有の定義とクロスファイル依存関係を維持したパッケージングを実現。
2. 包括的な評価: 最先端の汎用 LLM（GPT-5.2, Claude Opus 4.5, Gemini-3-Pro）と、専門的な定理証明器（Goedel-Prover, Aristotle）を対象に、上記 2 つのコンテキスト設定で評価を実施。
3. 依存構造と性能の相関分析: リポジトリ依存の構造的特徴（トランジティブ依存の深さや数）と証明成功確率の関係を定量的に分析。

4. 実験結果と分析

性能の概況

• 全体的な難易度: どのモデルも低い成功率にとどまりました。これは、ソフトウェア検証タスクの難易度が高いことを示しています。
  • Curated Contextでの最高成績：Gemini-3-Pro で 41.0%。
  • Full Repo Contextでの最高成績：Gemini-3-Pro で 34.8%。
  • 専門的な証明器（Goedel-Prover-v2）は、リポジトリ規模の設定では 0% の成功率でした（Mathlib 中心の数学タスクに特化しすぎているため）。

重要な発見

1. 数学特化モデルの転移性の低さ: Mathlib 中心のタスクで優れた性能を示す証明器は、プロジェクト固有のライブラリが存在する環境では性能が大幅に低下します。
2. トランジティブ依存の悪影響: 証明の成功は、トランジティブ依存（多段の依存関係）の深さと強く負の相関があります。
   • 直接的な依存数よりも、依存グラフの「深さ（nesting depth）」が課題となります。
   • 依存チェーンが長い場合（例：A が B に依存し、B が C に依存...）、モデルは中間的な抽象化をたどって論理を構築するのが困難になります。
   • 統計的に、トランジティブ依存数が多いほど成功率が低下する傾向（Spearman 相関係数 -0.359）が確認されました。
3. コンテキストの選別効果:
   • Curated Context の方が Full Repo Context よりも性能が良いですが、その差は予想より小さかった（Full Context でも関連するパターンが隠れたヒントとして機能している可能性）。
   • しかし、Curated Context であっても 41% 程度の成功率にとどまっており、「適切な文脈の検索」だけでは不十分であり、複雑な依存関係を推論する能力そのものが不足していることが示唆されました。

証明パターンの違い

• Verina（既存検証ベンチマーク）: unfold（定義展開） followed by simp（自動化）というパターンが多く、自動化依存度が高い。
• VeriSoftBench: 自動化への依存度が低く、**ケース分析（case analysis）**や分岐構造を多用する傾向があります。これは、プロジェクト固有の複雑な不変条件を扱うために、より構造的な推論が必要であることを示しています。

5. 意義と結論

VeriSoftBench は、LLM による定理証明の研究が、単なる「数学的なパズル」から「実世界のソフトウェア検証」へとシフトする必要性を浮き彫りにしました。

• 現状の課題: 既存のモデルは、大規模で多層的なプロジェクト固有の抽象化を横断する推論能力において未熟です。
• 今後の方向性:
  • 単にコンテキストを提示するだけでなく、多段の依存関係をたどる推論能力の向上。
  • 大規模リポジトリにおける文脈の適切な検索と統合メカニズムの開発。
  • Mathlib 中心の評価から脱却し、実用的な形式検証タスクに即したベンチマークの重要性。

本論文は、形式検証分野における LLM の実用化に向けた重要な基盤を提供し、今後の研究開発の指針となるものです。