ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

• URL: http://arxiv.org/abs/2607.19407v1
• Date: Tue, 07 Jul 2026 22:05:55 GMT
• Title: ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
• Abstract summary: ITPEval is the first benchmark for evaluating automated formal proof translation across four major ITPs.<n>We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends.
• Score: 77.95933562142014
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal theorem proving has emerged as a frontier challenge for machine learning, yet the ecosystem is fragmented: proofs remain siloed across incompatible systems, limiting both training data for learning-based provers and the portability of verified results. We present ITPEval, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations. Our benchmark comprises 1,560 source files and 6,848 theorems organized into a controlled tier of axiomatized files that isolates foundational translation difficulty, and an ecosystem tier drawn from real libraries that exposes API and proof-style mismatches. We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics. We evaluate both statement and proof translation across five frontier and open-weight LLMs on 12 directed translation pairs: statement translation peaks at 29.1% pass@1 and proof translation at 10.5%; controlled theorems reach 29.7% proof pass@1 versus 5.2% for ecosystem-level translations, confirming that library mismatch is the dominant bottleneck. In addition to pass@k evaluation, a deterministic Lean 4 BEq check establishes equivalence for 54.0% of verified source-to-Lean 4 miniF2F statement translations, showing that native type-checking alone can substantially overestimate semantic fidelity; in an autoformalization/auto-informalization round-trip study, Rocq and HOL Light are easier formalization targets than Lean 4 and Isabelle, while multi-ITP context improves pooled Lean 4 success from 4.8% to 10.6%. Our benchmark, verification infrastructure, and evaluation pipelines are publicly released.

Related papers

• Counterfactual Benchmarking and Training for Factuality Consistency and Order-Robust Grounded Reasoning in LLMs over Heterogeneous Knowledge [21.86609553205461]
  Large language models (LLMs) have increasingly supported response generation grounded in user-provided knowledge.<n>We introduce TKFQA, a factuality consistency benchmark comprising 10,130 question-answering (QA) pairs grounded in tables, texts, and knowledge graphs (KGs)<n>Each example is constructed from an explicit counterfactual reasoning chain, enabling the joint evaluation of answer correctness, reasoning-chain accuracy, and robustness to different input-order.
  arXiv  Detail & Related papers  (2026-08-08T00:46:32Z)
• Ontology-Amplified Distillation and Contextuality Auditing for Sovereign Enterprise Language Models: A Combined Proof-of-Mechanism and Negative-Results Method Study [0.0]
  This paper combines two related FAOS studies into one mechanism-and-control article.<n>First, it reports a reduced-power proof-of-mechanism study of ontology-amplified distillation.<n>Second, the paper consolidates a contextuality-audit method for enterprise-agent routing.
  arXiv  Detail & Related papers  (2026-07-11T15:42:40Z)
• Benchmarking Speech-to-Speech Translation Models [55.00303727199927]
  Speech-to-speech translation (S2ST) has advanced rapidly, but offline evaluation lacks a unified protocol.<n>We introduce a benchmarking framework integrating 46 metrics across eight dimensions.<n>We deploy it on 1,248 model-language configurations from FLEURS and CVSS.
  arXiv  Detail & Related papers  (2026-06-02T07:01:33Z)
• Incentivizing Parametric Knowledge via Reinforcement Learning with Verifiable Rewards for Cross-Cultural Entity Translation [68.85147984815778]
  We propose EA-RLVR (Entity-Anchored Reinforcement Learning with Verifiable Rewards) to incentivize the effective use of parametric knowledge.<n>EA-RLVR anchors supervision on a verifiable, entity-level reward signal and incorporates lightweight structural gates to stabilize optimization.<n>We evaluate EA-RLVR on XC-Translate and observe consistent improvements in both entity translation accuracy and out-of-domain generalization.
  arXiv  Detail & Related papers  (2026-04-18T07:15:43Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  We present ProofBridge, a framework for automatically translating entire NL theorems and proofs into Lean 4.<n>At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem-proof pairs in a shared semantic space.<n>Our training ensures NL-FL theorems are mapped close together in this space if and only if the NL-FL pairs are semantically equivalent.
  arXiv  Detail & Related papers  (2025-10-17T14:20:50Z)
• Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs [0.0]
  predicate availability boosts performance by 15-20%.<n>Models generalize to unseen logical arguments without specific training.<n>While structural logic translation proves robust, predicate extraction emerges as the main bottleneck.
  arXiv  Detail & Related papers  (2025-09-26T13:30:50Z)
• Document Attribution: Examining Citation Relationships using Large Language Models [62.46146670035751]
  We propose a zero-shot approach that frames attribution as a straightforward textual entailment task.<n>We also explore the role of the attention mechanism in enhancing the attribution process.
  arXiv  Detail & Related papers  (2025-05-09T04:40:11Z)
• RustRepoTrans: Repository-level Code Translation Benchmark Targeting Rust [50.65321080814249]
  RustRepoTrans is the first repository-level context code translation benchmark targeting incremental translation.<n>We evaluate seven representative LLMs, analyzing their errors to assess limitations in complex translation scenarios.
  arXiv  Detail & Related papers  (2024-11-21T10:00:52Z)
• Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
  This paper introduces a novel framework for translating the Mathlib4 corpus (a unified library of mathematics in formal language Lean 4) into natural language.<n>We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-based Translated Lean)<n>We also propose the Herald Translator, which is fine-tuned on Herald.
  arXiv  Detail & Related papers  (2024-10-09T10:11:24Z)
• Prosody in Cascade and Direct Speech-to-Text Translation: a case study on Korean Wh-Phrases [79.07111754406841]
  This work proposes using contrastive evaluation to measure the ability of direct S2TT systems to disambiguate utterances where prosody plays a crucial role. Our results clearly demonstrate the value of direct translation systems over cascade translation models.
  arXiv  Detail & Related papers  (2024-02-01T14:46:35Z)
• Leveraging Discourse Rewards for Document-Level Neural Machine Translation [46.006636555165414]
  We propose a training approach that explicitly optimize two established discourse metrics, lexical cohesion (LC) and coherence (COH) Our training approach has been able to achieve more cohesive and coherent document translations than other competitive approaches.
  arXiv  Detail & Related papers  (2020-10-08T02:26:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.