ITPEVAL: Benchmarking Formal Translation Across Interactive Theorem Provers

Summary (Overview)

• First four-way cross-ITP benchmark: ITPEVAL spans Lean 4, Rocq, Isabelle, and HOL Light, covering both dependent type theory (CIC) and higher-order logic (HOL) foundations, with 1,560 source files and 6,848 theorems organized into two tiers.
• Tiered design isolates difficulty sources: A controlled tier (64 axiomatized files, 660 lemmas) separates foundational translation issues from an ecosystem tier (232 Formalizing 100 Theorems files, 1,264 miniF2F statements) that exposes library API mismatches and proof-style differences.
• Unified verification infrastructure: The released itpeval tool provides state-isolated warm backends preserving native per-artifact checking semantics, achieving dramatic speedups (Isabelle: 472.2s → 6.9s; HOL Light: 527.4s → 149.0s).
• Key empirical findings: Statement translation peaks at 29.1% pass@1 (GPT-5.5); proof translation at 10.5%; controlled theorems reach 29.7% proof pass@1 versus 5.2% for ecosystem-level translations, identifying library mismatch as the dominant failure source.
• Semantic equivalence gap quantified: A deterministic Lean 4 BEq check establishes equivalence for only 54.0% of verified source→Lean 4 miniF2F statement translations, showing native type-checking alone substantially overestimates semantic fidelity.

Introduction and Theoretical Foundation

Background and Motivation

Formal mathematics has become a frontier domain for AI research, with large language models achieving strong results in automated theorem proving, autoformalization, and mathematical reasoning. However, the formal ecosystem remains fragmented: each interactive theorem prover (ITP) implements its own logical foundation, tactic language, and mathematical library. A theorem proved in Lean's Mathlib cannot be invoked in Isabelle's Archive of Formal Proofs, even when both encode the same mathematics.

The Translation Problem

Cross-ITP translation—converting formal proofs between systems while preserving correctness—addresses this fragmentation in two ways:

1. Result transfer: Enables verified results to transfer across ITP ecosystems, reducing duplicate formalization effort and expanding training data for learning-based provers.
2. Autoformalization insights: Informs both autoformalization and auto-informalization, since both require preserving theorem meaning across different surface languages and libraries.

Theoretical Foundations

ITPEVAL spans two major proof-assistant traditions:

• Lean 4 and Rocq: Based on the Calculus of Inductive Constructions (CIC)
• Isabelle/HOL and HOL Light: Based on Higher-Order Logic (HOL)

The paper argues that translation difficulty is not determined by foundation alone—tactic languages, proof idioms, libraries, automation, and naming conventions differ even within the same logical family.

Gaps in Prior Work

Key evaluation challenge: Type-checking alone has a high false-positive rate for semantic correctness, and code translation benchmarks apply only partially since ITP translation must navigate logical foundation differences, not just syntactic ones.

Methodology

Benchmark Design

The benchmark employs a four-way intersection requirement: every file must be formalized in all four ITPs, ensuring clean directional and foundation-pair comparisons without missing-data confounds.

Tier A: Controlled Files

Self-contained, axiomatized files including their own definitions and assumptions, avoiding dependence on prover-specific libraries. These isolate foundational and language-level translation issues (type theory, quantification, implicit arguments, universe conventions, proof syntax). Source: Extended Babel-formal (16 aligned items; 64 files; 660 lemmas).

Tier B: Ecosystem Files

Formalizations drawn from existing libraries reflecting real proof engineering practice—library lemmas, local helper definitions, tactic automation, naming conventions, and prover-specific mathematical structures. Sources:

• Formalizing 100 Theorems: 58 aligned items (232 files; 4,924 lemmas) from Wiedijk's list, aligned by canonical list number
• MiniF2F: 316 problems (1,264 single-theorem files, statements only) aligned by standardized problem identifier

Translation Tasks

1. Statement translation (stmts): Given a source file with proof bodies replaced by placeholders (sorry), produce the corresponding target file with placeholder proofs. Verification requires the entire file to type-check.

2. Proof translation (proofs): Given a complete proof file, produce a complete compilable file with no placeholders. Every lemma must be fully proved.

Verification Infrastructure

The itpeval client implements native target-prover checking—all labels are produced by the actual target ITP with exit code 0 required. Key mechanisms:

• State isolation: Every accelerated check is observationally equivalent to standalone verification
• Environment-keyed scheduling: Content-addressed caching and cost-aware scheduling
• Adaptive bisection: Recovers per-artifact labels after batch failures
• Append-only checkpoints: Make runs restartable

Backend throughput (16 Babel-formal statement files):

Semantic Equivalence Checking (BEq)

Adapted from Liu et al. (2025a), Bidirectional Extended Definitional Equivalence checks both entailments for a generated Lean statement $G$ and reference statement $R$:

$$G \vdash R \quad \text{and} \quad R \vdash G$$

A translation passes iff both directions succeed. The implementation uses a deterministic Lean tactic cascade (replacing LLM-sampled transformations) for reproducibility, testing whether verified translations preserve theorem meaning.

Models Evaluated

Five zero-shot, greedy-decoded models ($T = 0$): GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro Preview, DeepSeek-V4-Pro, and Qwen3-235B-A22B.

Empirical Validation / Results

Statement Translation

Overall pass@1 (4,680 directed pairs per model):

By benchmark:

Direction asymmetry: Isabelle and HOL Light have highest target-side verification rates (e.g., HOL Light→Isabelle: 25.8%; Lean 4→Isabelle: 17.6%), while Isabelle→Lean 4 reaches only 4.3%. CIC→CIC directions are not consistently easier than cross-foundation directions.

Proof Translation

Pass@1 on 888 directed pairs:

Direction reversal: Isabelle becomes the lowest proof target (1.9–3.2%) despite high statement verification rates; HOL Light remains comparatively strong (4.3–5.7%).

Statements vs. Proofs

McNemar test on matched instances: $\chi^2 = 249.19$, $p < 0.0001$. Asymmetry: 417 instances pass only in statement mode, 69 pass only in proof mode. Statement success is a near necessary condition for proof success (32 theorems pass statements but never proofs; no theorem passes proofs without statement success).

Aggregate Logistic Regression

Fit over 27,840 evaluation records ($pseudo\text{-}R^2 = 0.25$):

• Target prover and benchmark identity: Strongest predictors
• Proof translation: Large negative effect ($-1.05$)
• Shared logical foundation: Weak positive effect ($+0.19$, $p = 0.001$)
• Source complexity: Longer files harder in proof mode ($-0.54$, $p < 0.001$); successful translations have shorter sources (median 1,978 vs. 3,992 characters)

Autoformalization/Auto-informalization Round-Trip

Three-step protocol: NL→formal→NL→formal. Target effects are pronounced:

Multi-ITP context improves pooled Lean 4 verification (step 1: 4.8%→10.6%), but benefits are model- and target-dependent.

Semantic Equivalence (BEq) Results

Applied to all 322 verified source→Lean 4 statement translations on miniF2F:

BEq failures are mostly neither-direction failures (132/322); all asymmetric failures are backward-only (16/322), consistent with semantic weakening. Source direction effects: Rocq→Lean 52.4%, Isabelle→Lean 47.5%, HOL Light→Lean 61.5%.

Theoretical and Practical Implications

Library Mismatch Dominates Over Foundation Differences

The largest performance gap is between controlled and ecosystem files, not between same-foundation and cross-foundation pairs. This parallels programming language translation findings where library-centric errors dominate over core language failures. Future translation systems should prioritize:

• Retrieval and library mapping
• API alignment
• Proof-style adaptation

Target-Asymmetry Insights

If logical-foundation similarity were the main factor, Lean 4↔Rocq would have uniformly high verification rates. Instead, rates vary substantially by target: Isabelle and HOL Light are strong statement targets; Isabelle becomes the lowest-verification proof target; HOL Light remains relatively strong for proofs. Isabelle's structured Isar style helps well-formed declarations, while HOL Light's compact OCaml tactic style appears more uniform for current models.

Type-Checking is Necessary but Insufficient

The BEq results demonstrate that target-prover type checking is a weak semantic metric. A Lean-accepted generated statement is often syntactically valid but not established equivalent to the reference. This has implications for:

• Benchmark design: Equivalence-aware evaluation is needed alongside executable acceptance signals
• Model evaluation: Different models trade off verification rate versus semantic fidelity differently (e.g., Claude has lowest verification but highest BEq pass rate among verified)

Infrastructure as Part of the Benchmark

Cross-ITP results are only reliable when verifier state is isolated, labels are recovered per artifact, and backend provenance is recorded. The unified state-isolated client fixes the unit of measurement to one generated artifact while making large-scale target-prover checking reproducible and auditable.

Conclusion

Main Takeaways

1. ITPEVAL provides the first four-way aligned cross-ITP benchmark spanning two logical foundations, with tiered design separating foundational translation from ecosystem complexity.
2. Statement translation remains challenging (peak 29.1% pass@1) and proof translation is much harder (peak 10.5%).
3. Library dependencies are the strongest measured source of difficulty, not logical foundation differences.
4. Type-checking alone substantially overestimates semantic fidelity: only 54.0% of verified translations pass BEq equivalence checking.
5. Target-dependent effects persist in autoformalization round-trips, with multi-ITP context showing hypothesis-generating benefits.

Limitations

• Zero-shot pass@1 evaluation only (not pass@k or agentic systems)
• BEq coverage limited to Lean 4 targets
• Potential training-data contamination from public benchmarks (miniF2F, Formalizing 100 Theorems, Babel-formal)
• Round-trip study is exploratory with limited scale

Future Directions

• Add retrieval and repair mechanisms for translation systems
• Deploy BEq beyond Lean 4 targets
• Scale aligned corpora across more ITPs
• Create private or newly authored splits for out-of-distribution evaluation
• Study semantic fidelity of proof strategies (not just statements)
• Scale round-trip studies for robust multi-ITP context conclusions