💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

本論文は、4つの主要な対話型定理証明器にわたる自動形式証明翻訳を評価するための初のベンチマークおよび統一されたインフラストラクチャであるITPEvalを紹介し、現在の大規模言語モデルがライブラリの不一致により証明の翻訳において著しく苦戦していること、およびネイティブの型チェックのみでは意味的な忠実度を過大評価してしまうことが多いことを明らかにしている。

原著者： Jiayi Wu, Robert Joseph George, Anima Anandkumar

公開日 2026-07-23

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Jiayi Wu, Robert Joseph George, Anima Anandkumar

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

数学者が4つの異なる言語を話しているものの、全員が全く同じパズルを解こうとしている世界を想像してみてください。「形式的定理証明（formal theorem proving）」という高リスクの舞台では、コンピュータが究極の審判として機能し、数学的証明のあらゆるステップをチェックして、それが100%正しいことを保証します。しかし、フランス語、日本語、スワヒリ語、アラビア語を話す人間と同じように、これらのコンピュータシステム（対話型定理証明器、またはITPと呼ばれる）もまた、独自の文法、語彙、そして事前に承認された事実のライブラリを持っています。あるシステムで完璧に書かれた証明は、他のシステムにとってはしばしば意味不明なものとなります。これは孤独な問題を生み出します。もし素晴らしい証明がある一つの言語で書かれていたとしても、それを他のシステムで簡単に利用したり検証したりすることができないからです。科学者たちは、この溝を埋めるための「万能翻訳機」を構築しようと試みてきました。人工知能（AI）がこれらの数学的証明を自動的に翻訳できるようになり、コミュニティ全体が成果を共有できるようにすることを期待してのことです。

ここで、大規模で厳格な言語試験として機能する新しい研究、ITPEVALが登場します。研究者たちは、今日の最もスマートなAIモデルが、4つの主要なシステム（Lean 4、Rocole、Isabelle、HOL Light）の間で、実際に形式的な数学的証明を翻訳できるかどうかを確かめたいと考えました。彼らは単にAIに推測させたのではありません。彼らは、1,500以上のソースファイルと7,000近い定理を備えた、特化したテスト環境を構築しました。テストは2つのレベルに分けられました。一つは、単純で自己完結的な数学の問題を用いた「制御（Controlled）」レベル（外部の参照がない語彙クイズのようなもの）、もう一つは、複雑でシステム固有のルールに依存する、実際の複雑なライブラリコードを用いた「エコシステム（Ecosystem）」レベル（スラングや文化的背景を含むフルバージョンの会話のようなもの）です。

結果は、「悪くはないが、依然として非常に困難である」という混合したものでした。AIが定理の「命題（what）」のみを翻訳しようとした場合、最高のモデルの正解率は約**29.1%でした。しかし、実際の「証明（how）」を翻訳するよう求められると、成功率はわずか10.5%**へと急落しました。研究によって明らかになった最大の障害は、数学そのものや論理的基盤の違いではなく、「エコシステム」でした。AIは、ターゲットとなるシステムの特定のライブラリ、命名規則、および自動化スタイルをナビゲートしなければならない時に、最も苦戦しました。それは、AIが「猫がマットの上に座った」という文章は理解できても、特定のブランドのマットと特定の種類の猫を使用しなければならない特定のダイアレクト（方言）への翻訳を求められると失敗するようなものです。

さらに、研究者たちは、コンピュータに単に「これは正しく見える」と言わせる（型チェック）だけでは不十分であることを発見しました。彼らがより深い「意味チェック」を行ったところ、AIの翻訳がコンピュータの基本的なテストを通過したとしても、その**46%**のケースにおいて、元の証明よりも数学的に弱かったり、あるいはわずかに異なっていたりすることが分かりました。この研究は、AIが基礎については習熟しつつあるものの、真の万能翻訳機になれる前に、各数学システムの独特な「文化」に適応する方法を学ぶ必要があることを示唆しています。著者らはまた、数学を自然言語に翻訳し、再び戻すという「ラウンドトリップ」テストについても調査し、その結果は使用されるシステムによって大きく異なることを発見しました。これは、複数のシステムを併用することが助けになる可能性を示唆していますが、まだ魔法の解決策にはなっていません。

技術要約：ITPEVAL – 対話型定理証明器間における形式的翻訳のベンチマーク化

1. 問題提起

現在の形式的定理証明のエコシステムは断片化している。大規模言語モデル（LLM）は、自動定理証明やオートフォーマライゼーション（自動形式化）において顕著な成功を収めているが、検証された結果は互換性のない対話型定理証明器（ITP）の中に隔離されている。各システム（例：Lean 4, Rocq, Isabelle, HOL Light）は、独自の論理基盤、タクティク言語、および数学ライブラリを実装している。その結果、あるシステムで証明された定理を別のシステムで直接呼び出すことはできず、形式化の作業が重複し、学習ベースの証明器が利用可能な訓練データを制限することにつながっている。

クロスITP翻訳（正確性を維持しながら、形式的証明をシステム間で変換するタスク）については、体系的な研究がほとんど行われていない。既存の取り組み（例：「Formalizing 100 Theorems」カタログや、Deduktiのような相互運用性フレームワーク）は、カバレッジの追跡や中間表現を介した証明交換を可能にすることには焦点を当てているが、翻訳品質を評価するための標準化されたベンチマークは欠いている。さらに、既存の評価手法は不十分である。単純な型チェックだけでは意味的な正当性に関する偽陽性率が高くなり、コード翻訳のベンチマークは、ITPに固有の深い論理基盤の違いを考慮に入れていない。

2. メソドロジーとベンチマーク設計

著者らは、4つの主要なITP（Lean 4, Rocq（旧Coq）, Isabelle, HOL Light）間での自動形式的証明翻訳を評価するために設計された初のベンチマークであるITPEVALを提示する。このベンチマークは、2つの異なる論理基盤（帰納的構成の計算、および高階論理（HOL））にまたがっている。

2.1. データ構造

本ベンチマークは、困難の要因を分離するために2つの異なるティアに整理された、1,560個のソースファイルと6,848個の定理で構成されている。

Tier A (Controlled): Babel-formal ベンチマークから派生した、64個の自己完結型かつ公理化されたファイル（660個の補題）を含む。これらのファイルは独自の定義と仮定を含んでおり、証明器固有のライブラリへの依存を回避している。このティアは、基礎的な翻訳の問題（例：型理論、ユニバースレベル、暗黙の引数）を分離して検証する。
Tier B (Ecosystem): 実際のコミュニティライブラリから抽出された形式化を含み、APIの不一致、命名規則、および証明スタイルの違いを露呈させる。このティアには以下が含まれる：
- Formalizing 100 Theorems からの232個のファイル（4,924個の補題）。これらは全4つのシステム間で整合性が取れている。
- miniF2F からの1,264個の単一定理ファイル（記述のみ）。多様な競技数学のコンテンツを提供している。

設計においては、欠損データによる混乱を避けるため、すべてのファイルが4つのITPすべてで形式化されているという**「4方向の交差要件」**を強制している。

2.2. 翻訳タスク

ITPEVALは、主に2つのタスクを評価する：

記述（Statement）の翻訳: 証明本体がプレースホルダー（例：sorry）に置き換えられたターゲットITPコードを生成する。検証には、生成されたファイルがターゲットシステム内で型チェックを通ることが求められる。
証明（Proof）の翻訳: プレースホルダーのない、完全でコンパイル可能な証明ファイルを生成する。検証には、ファイル全体がターゲットとなる証明器で正常にコンパイルされることが求められる。

2.3. 検証インフラストラクチャ

本メソドロジーの重要な要素は、統一されたマルチITP検証インフラストラクチャであるitpevalである。ITPの実行モデルの異質性（例：IsabelleやHOL Lightの重い起動コスト）に対処するため、システムは以下を採用している：

状態分離されたウォームバックエンド: すべてのチェックが、新しい環境におけるアーティファクトの検証と観測的に等価であることを保証し、宣言のリークを防ぐ。
ネイティブなターゲット証明器によるチェック: すべてのラベルは、表面的なヒューリスティックではなく、実際のターゲットITPによって生成される。
適応型スケジューリング: パーシステントワーカー、セッションバッチング、およびフォークサーバーを使用して、ファイルごとのチェックのセマンティクスを維持しながらスループットを管理する。

2.4. 意味的等価性チェック

型チェックは必要条件ではあるが、意味的な忠実性のための十分条件ではないことを認識し、著者らはLean 4ターゲットに対して**双方向拡張定義等価性（BEq）**チェックを実装している。この決定論的なチェックは、制限された証明探索を用いて、生成された記述 $G$ と参照記述 $R$ が互いに含意し合うこと（ $G \vdash R$ かつ $R \vdash G$ ）を検証し、追加のモデル依存の分散を回避する。

3. 主な貢献

4方向整合ベンチマーク: Lean 4, Rocq, Isabelle, HOL Lightにわたる1,560個のファイルと6,848個の定理のデータセット。ライブラリ依存によるコストを定量化するために、制御されたティアとエコシステムティアに構造化されている。
統一検証インフラストラクチャ: ヘテロジニアスな証明器に対して、ネイティブなチェックのセマンティクスを備えた、スケーラブルで再現可能な評価を可能にする、状態分離されたクライアント（itpeval）。
体系的なLLM評価: 12の直接的な翻訳ペアにおいて、5つのフロンティアモデルおよびオープンウェイトモデル（GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B）を評価。
意味的忠実性の分析: BEqを適用することで、ネイティブの型チェックだけでは意味的な正当性を大幅に過大評価する可能性があることを示す。
探索的なラウンドトリップ研究: ターゲット依存の検証パターンと、マルチITPコンテキストの潜在的な利点を評価するための、オートフォーマライゼーションおよびオートインフォーマライゼーションのループに関する調査。

4. 結果

4.1. 翻訳パフォーマンス

記述の翻訳: 最も優れた性能を示したモデルはGPT-5.5であり、全体で29.1%のpass@1を達成した。DeepSeek-V4-Proが27.1%でこれに続いた。他のモデル（Geminiは14.0%、QwenとClaudeは10%未満）では性能が大幅に低下した。
証明の翻訳: パフォーマンスは大幅に低く、GPT-5.5でも全体でわずか10.5%のpass@1であった。
ティア間の格差: 制御されたティア（Tier A）は、エコシステム・ティア（Tier B）よりも一貫して容易であった。証明の翻訳において、GPT-5.5は制御されたファイルでは**29.7%に達したが、エコシステム・ファイルではわずか5.2%**であった。これは、ライブラリのミスマッチ（API、命名、自動化）が、論理基盤の違いよりも大きな失敗の原因であることを示している。
方向的な非対称性: 翻訳の難易度はターゲットによって大きく異なる。IsabelleとHOL Lightは記述の翻訳において強力なターゲットであるが、Isabelleは証明の翻訳において最も困難なターゲットとなる。論理基盤の類似性（例：CICからCICへ）は、成功率の向上を保証しない。ターゲットのエコシステムの慣習の方が大きな役割を果たす。

4.2. 意味的等価性 (BEq)

miniF2F からの検証済み Lean 4 記述翻訳に BEq チェックを適用したところ：

検証された翻訳のうち、等価性チェックを通過したのはわずか**54.0%**であった。
Claude Sonnet 4.6 は、検証された翻訳の中で最高の BEq 通過率（83.8%）を示したが、他は34.5%から48.4%の範囲であった。
この結果は、記述が構文的に有効（型チェックを通過）であっても、意味的に弱くなっていたり、元の定理から逸脱したりする可能性があることを示している。

4.3. ラウンドトリップとオートフォーマライゼーション

マルチITPラウンドトリップ研究（自然言語 $\to$ 形式的記述 $\to$ 自然言語 $\to$ 形式的記述）において、Rocq と HOL Light は両方の形式化ステップで出力の約3分の1を検証したが、Lean 4 は11%付近、Isabelle は最終ステップで4.3%まで低下した。マルチITPコンテキストは、特定のモデルとターゲットの組み合わせ（例：Lean 4のステップ1のパス率を4.8%から10.6%に向上させるなど）において潜在的な利益を示したが、結果はすべてのシステムで一様ではなかった。

5. 意義と主張

本論文は、ITPEVAL が形式的翻訳のための初の体系的な4方向ベンチマークを提供し、主要な障壁は論理基盤そのものではなく、エコシステムレベルの依存関係（ライブラリ、API、および証明のイディオム）であることを明らかにしていると主張している。

著者らは以下を強調している：

ネイティブな検証は不可欠である: 表面的なヒューリスティックや型チェックだけでは、意味的な忠実性を評価するには不十分である。
インフラストラクチャが重要である: 信頼できるクロスITP評価には、宣言のリークのような混乱要因を防ぐための、状態分離された検証が必要である。
今後の方向性: 今後の研究は、純粋な基礎的翻訳よりも、リトリーバル（検索）、ライブラリのマッピング、およびAPIの整合性に優先順位を置くべきである。また、本論文は、ゼロショット評価の設定、BEqのLean 4ターゲットへの限定、および miniF2F のような公開データセットにおける訓練データの汚染の可能性といった限界についても述べている。

本研究は、形式的翻訳の進歩を測定するための基礎を築き、将来のシステムが堅牢な相互運用性を実現するためには、「ライブラリのミスマッチ」問題に対処しなければならないことを示唆している。