💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

This paper introduces ITPEval, the first benchmark and unified infrastructure for evaluating automated formal proof translation across four major interactive theorem provers, revealing that current large language models struggle significantly with proof translation due to library mismatches and that native type-checking alone often overestimates semantic fidelity.

Original authors: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Published 2026-07-23

📖 3 min read☕ Coffee break read

CC BY 4.0

Original authors: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a world where mathematicians speak four different languages, but they are all trying to solve the exact same puzzles. In the high-stakes arena of "formal theorem proving," computers act as the ultimate referees, checking every single step of a math proof to ensure it's 100% correct. However, just like humans who speak French, Japanese, Swahili, and Arabic, these computer systems (called Interactive Theorem Provers, or ITPs) have their own unique grammar, vocabulary, and libraries of pre-approved facts. A proof written perfectly in one system is often gibberish to the others. This creates a lonely problem: if a brilliant proof is written in one language, it can't be easily used or checked by the others. Scientists have been trying to build "universal translators" to bridge this gap, hoping that Artificial Intelligence (AI) could learn to translate these mathematical proofs automatically, allowing the whole community to share their work.

Enter ITPEVAL, a new study that acts like a massive, rigorous language exam for AI. The researchers wanted to see if today's smartest AI models could actually translate formal math proofs between four major systems: Lean 4, Rocq, Isabelle, and HOL Light. They didn't just ask the AI to guess; they built a specialized testing ground with over 1,500 source files and nearly 7,000 theorems. They split the test into two levels: a "Controlled" level with simple, self-contained math problems (like a vocabulary quiz with no outside references), and an "Ecosystem" level using real, messy library code that relies on complex, system-specific rules (like a full conversation with slang and cultural references).

The results were a mix of "not bad" and "still very hard." When the AI tried to translate just the statements of the theorems (the "what"), the best models got about 29.1% right. But when asked to translate the actual proofs (the "how"), the success rate plummeted to just 10.5%. The study found that the biggest hurdle wasn't the math itself or the different logical foundations; it was the "ecosystem." The AI struggled most when it had to navigate the specific libraries, naming conventions, and automation styles of the target system. It's like the AI could understand the sentence "The cat sat on the mat," but failed when asked to translate it into a specific dialect that required using a specific brand of mat and a specific type of cat.

Furthermore, the researchers discovered that simply getting a computer to say "This looks correct" (a type-check) isn't enough. They ran a deeper "meaning check" and found that even when the AI's translation passed the computer's basic test, it was often mathematically weaker or slightly different from the original in 46% of the cases. The study suggests that while AI is getting better at the basics, it still needs to learn how to adapt to the unique "culture" of each math system before it can truly be a universal translator. The authors also explored a "round-trip" test, where they translated math to natural language and back, finding that the results varied wildly depending on which system was used, hinting that using multiple systems together might help, but it's not a magic fix yet.

Technical Summary: ITPEVAL – Benchmarking Formal Translation Across Interactive Theorem Provers

1. Problem Statement

The formal theorem proving ecosystem is currently fragmented. While large language models (LLMs) have achieved significant success in automated theorem proving and autoformalization, verified results remain siloed within incompatible Interactive Theorem Provers (ITPs). Each system (e.g., Lean 4, Rocq, Isabelle, HOL Light) implements its own logical foundation, tactic language, and mathematical libraries. Consequently, a theorem proved in one system cannot be directly invoked in another, leading to duplicated formalization efforts and limiting the training data available for learning-based provers.

Cross-ITP translation—the task of converting formal proofs between systems while preserving correctness—has received little systematic study. Existing efforts, such as "Formalizing 100 Theorems" catalogs or interoperability frameworks like Dedukti, focus on tracking coverage or enabling proof exchange via intermediate representations but lack standardized benchmarks for evaluating translation quality. Furthermore, existing evaluation methodologies are insufficient; simple type-checking often yields high false-positive rates for semantic correctness, and code translation benchmarks do not account for the deep logical foundation differences inherent to ITPs.

2. Methodology and Benchmark Design

The authors present ITPEVAL, the first benchmark designed to evaluate automated formal proof translation across four major ITPs: Lean 4, Rocq (formerly Coq), Isabelle, and HOL Light. The benchmark spans two distinct logical foundations: the Calculus of Inductive Constructions (CIC) and Higher-Order Logic (HOL).

2.1. Data Structure

The benchmark comprises 1,560 source files and 6,848 theorems, organized into two distinct tiers to isolate sources of difficulty:

Tier A (Controlled): Contains 64 self-contained, axiomatized files (660 lemmas) derived from the Babel-formal benchmark. These files include their own definitions and assumptions, avoiding dependence on prover-specific libraries. This tier isolates foundational translation issues (e.g., type theory, universe levels, implicit arguments).
Tier B (Ecosystem): Contains formalizations drawn from real community libraries, exposing API mismatches, naming conventions, and proof-style differences. This tier includes:
- 232 files from Formalizing 100 Theorems (4,924 lemmas), aligned across all four systems.
- 1,264 single-theorem files from miniF2F (statements only), providing diverse competition math content.

The design enforces a four-way intersection requirement: every file must be formalized in all four ITPs to ensure clean directional comparisons without missing-data confounds.

2.2. Translation Tasks

ITPEVAL evaluates two primary tasks:

Statement Translation: Generating target ITP code where proof bodies are replaced by placeholders (e.g., sorry). Verification requires the generated file to type-check in the target system.
Proof Translation: Generating complete, compilable proof files without placeholders. Verification requires the entire file to compile successfully in the target prover.

2.3. Verification Infrastructure

A critical component of the methodology is itpeval, a unified multi-ITP verification infrastructure. To address the heterogeneity of ITP execution models (e.g., heavy startup costs for Isabelle and HOL Light), the system employs:

State-isolated warm backends: Ensuring that every check is observationally equivalent to verifying an artifact in a fresh environment, preventing declaration leakage.
Native target-prover checking: All labels are produced by the actual target ITPs, not surface-level heuristics.
Adaptive scheduling: Using persistent workers, session batching, and fork servers to manage throughput while preserving per-file checking semantics.

2.4. Semantic Equivalence Checking

Recognizing that type-checking is necessary but insufficient for semantic fidelity, the authors implement a Bidirectional Extended Definitional Equivalence (BEq) check for Lean 4 targets. This deterministic check verifies if a generated statement $G$ and a reference statement $R$ entail each other ( $G \vdash R$ and $R \vdash G$ ) using restricted proof search, avoiding additional model-dependent variance.

3. Key Contributions

Four-Way Aligned Benchmark: A dataset of 1,560 files and 6,848 theorems across Lean 4, Rocq, Isabelle, and HOL Light, structured into controlled and ecosystem tiers to quantify the cost of library dependencies.
Unified Verification Infrastructure: A state-isolated client (itpeval) that enables scalable, reproducible evaluation across heterogeneous provers with native checking semantics.
Systematic LLM Evaluation: An evaluation of five frontier and open-weight models (GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B) on 12 directed translation pairs.
Semantic Fidelity Analysis: The application of BEq to demonstrate that native type-checking alone can substantially overestimate semantic correctness.
Exploratory Round-Trip Study: An investigation into autoformalization and auto-informalization loops to assess target-dependent verification patterns and the potential benefits of multi-ITP context.

4. Results

4.1. Translation Performance

Statement Translation: The best-performing model, GPT-5.5, achieved a 29.1% pass@1 rate overall. DeepSeek-V4-Pro followed at 27.1%. Performance dropped significantly for other models (Gemini at 14.0%, Qwen and Claude below 10%).
Proof Translation: Performance was substantially lower, with GPT-5.5 achieving only 10.5% pass@1 overall.
Tier Gap: The controlled tier (Tier A) was consistently easier than the ecosystem tier (Tier B). For proof translation, GPT-5.5 reached 29.7% on controlled files but only 5.2% on ecosystem files. This indicates that library mismatch (APIs, naming, automation) is the largest observed source of failure, rather than logical foundation differences.
Directional Asymmetry: Translation difficulty varies significantly by target. Isabelle and HOL Light are strong targets for statement translation, but Isabelle becomes the most difficult target for proof translation. Logical foundation similarity (e.g., CIC to CIC) does not guarantee higher success rates; target ecosystem conventions play a larger role.

4.2. Semantic Equivalence (BEq)

When applying the BEq check to verified Lean 4 statement translations from miniF2F:

Only 54.0% of verified translations passed the equivalence check.
Claude Sonnet 4.6 showed the highest BEq pass rate (83.8%) among verified translations, while others ranged from 34.5% to 48.4%.
This result demonstrates that a statement can be syntactically valid (type-checking) yet semantically weaker or shifted from the original theorem.

4.3. Round-Trip and Autoformalization

In a multi-ITP round-trip study (NL $\to$ Formal $\to$ NL $\to$ Formal), Rocq and HOL Light verified approximately one-third of outputs at both formalization steps, whereas Lean 4 hovered near 11% and Isabelle dropped to 4.3% at the final step. Multi-ITP context showed potential benefits for specific model-target combinations (e.g., improving Lean 4 step-1 pass rates from 4.8% to 10.6%), but results were not uniform across all systems.

5. Significance and Claims

The paper claims that ITPEVAL provides the first systematic, four-way benchmark for formal translation, revealing that the primary barrier to cross-ITP translation is not the logical foundation itself, but the ecosystem-level dependencies (libraries, APIs, and proof idioms).

The authors emphasize that:

Native verification is essential: Surface-level heuristics or type-checking alone are insufficient for evaluating semantic fidelity.
Infrastructure matters: Reliable cross-ITP evaluation requires state-isolated verification to prevent confounding factors like declaration leakage.
Future directions: The field must prioritize retrieval, library mapping, and API alignment over purely foundational translation. The paper also notes limitations, including the zero-shot evaluation setting, the restriction of BEq to Lean 4 targets, and the potential for training data contamination in public datasets like miniF2F.

The work establishes a foundation for measuring progress in formal translation, suggesting that future systems must address the "library mismatch" problem to achieve robust interoperability between formal proof ecosystems.