# ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

> ITPEVAL, the first four-way cross-ITP benchmark, shows library mismatches—not logical foundations—dominate translation difficulty, with type-checking alone overestimating semantic fidelity by nearly half.

- **Source:** [arXiv](https://arxiv.org/abs/2607.19407)
- **Published:** 2026-10-24
- **Permalink:** https://picx.dev/p/z2KH1R
- **Whiteboard:** https://picx.dev/p/z2KH1R/image

## Summary

# 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

| Work | Systems | Gap |
|------|---------|-----|
| Formalizing 100 Theorems / 1000+ Theorems | Many ITPs | Overlap catalogues only, no benchmark |
| Dedukti / Logipedia / EuroProofNet | Many logics | Proof exchange infrastructure, no evaluation |
| Babel-formal | Lean, Rocq only | Limited to 14 aligned files, two provers |
| MiniF2F in Rocq | Lean, Isabelle, Rocq | Statement port only |
| ProofWala / KELPS | Two provers | Proof search, not balanced translation |

**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):

| Prover | Backend | Reuse | Isolation | Cold (s) | Warm (s) |
|--------|---------|-------|-----------|----------|----------|
| Lean 4 | pool/server | compiler workers | fresh file | 15.1 | 3.7 |
| Rocq | REPL pool | persistent proc. | Reset Initial. | 4.3 | 0.5 |
| Isabelle | server batch | persistent session | temp. theories | 472.2 | 6.9 |
| HOL Light | forkserver | preloaded OCaml | child exit | 527.4 | 149.0 |

### 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):

| Model | Overall Pass@1 |
|-------|---------------|
| GPT-5.5 | 29.1% |
| DeepSeek-V4-Pro | 27.1% |
| Gemini 3.1 Pro | 14.0% |
| Qwen3-235B-A22B | 9.7% |
| Claude Sonnet 4.6 | 4.0% |

**By benchmark**:

| Model | Babel (A, 192) | Formalizing 100 Theorems (B, 696) | miniF2F (B, 3792) |
|-------|---------------|-----------------------------------|-------------------|
| GPT-5.5 | 91 (47.4%) | 106 (15.2%) | 1163 (30.7%) |
| Gemini 3.1 | 63 (32.8%) | 97 (13.9%) | 496 (13.1%) |
| Claude 4.6 | 21 (10.9%) | 32 (4.6%) | 134 (3.5%) |
| DeepSeek-V4 | 33 (17.2%) | 46 (6.6%) | 1190 (31.4%) |
| Qwen3-235B | 18 (9.4%) | 10 (1.4%) | 424 (11.2%) |

**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**:

| Model | Overall (888) | Babel (A, 192) | Formalizing 100 Theorems (B, 696) |
|-------|--------------|----------------|-----------------------------------|
| GPT-5.5 | 93 (10.5%) | 57 (29.7%) | 36 (5.2%) |
| Gemini 3.1 | 45 (5.1%) | 35 (18.2%) | 10 (1.4%) |
| Claude 4.6 | 13 (1.5%) | 11 (5.7%) | 2 (0.3%) |
| DeepSeek-V4 | 13 (1.5%) | 9 (4.7%) | 4 (0.6%) |
| Qwen3-235B | 5 (0.6%) | 3 (1.6%) | 2 (0.3%) |

**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:

| Target | Step 1 pass | Step 3 pass | Both pass |
|--------|------------|-------------|-----------|
| Lean 4 | 53/491 (10.8%) | 56/493 (11.4%) | 36 |
| Isabelle | 42/489 (8.6%) | 21/490 (4.3%) | 10 |
| Rocq | 152/465 (32.7%) | 146/460 (31.7%) | 101 |
| HOL Light | 144/460 (31.3%) | 147/454 (32.4%) | 103 |

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:

| Model | Verified | BEq Pass | Pass% | BEq Fail |
|-------|----------|----------|-------|----------|
| Claude Sonnet 4.6 | 74 | 62 | 83.8% | 12 |
| DeepSeek-V4-Pro | 84 | 37 | 44.0% | 47 |
| Gemini 3.1 Pro | 7 | 3 | 42.9% | 4 |
| GPT-5.5 | 29 | 10 | 34.5% | 19 |
| Qwen3-235B | 128 | 62 | 48.4% | 66 |
| **All models** | **322** | **174** | **54.0%** | **148** |

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

---

_Markdown view of https://picx.dev/p/z2KH1R, served by PicX — AI-generated visual whiteboard summaries of research papers._