Technical Summary: ProofWala

Problem Statement

Automated theorem proving using neural methods requires robust infrastructure to interface with Interactive Theorem Provers (ITPs), extract structured proof data, and execute proof search at scale. Existing tooling is often fragmented, assistant-specific, and oriented toward interactive, file-level execution via REPL (Read-Eval-Print Loop) interfaces. This architecture presents significant limitations:

• Scalability: It hinders repository-scale analysis and parallel experimentation.
• Data Extraction: It provides limited access to declaration-level metadata (e.g., inductive definitions, constants, namespaces) and makes constructing repository-wide dependency graphs difficult or infeasible.
• Cross-Assistant Gaps: The lack of unified tooling makes it challenging to exploit potential cross-lingual and cross-domain gains from training on multilingual formal corpora (e.g., Lean and Rocq).

Methodology

The authors present ProofWala, a multilingual proof engineering framework designed to unify interaction, data extraction, training, and search across different ITPs. The framework is built around three core components:

1. The Interface Module (itp-interface)

This is a reusable library for programmatic interaction with ITPs, providing a unified abstraction for Lean 4 and Rocq (multiple versions).

• Lean 4 Backend: Instead of relying on a REPL-based architecture, the authors implemented meta-programs that execute directly inside the Lean elaborator. This enables:
  • Semantically faithful tactic-level tracing.
  • Extraction of declaration-level metadata and construction of repository-wide dependency graphs.
  • Improved handling of nested tactic constructs (e.g., have blocks).
  • Environment Cloning: The ability to clone proof environments for parallel execution, which is difficult with standard REPL workflows.
  • Version Robustness: A thin compatibility layer ensures forward compatibility across Lean 4 versions starting from 4.15.0.
• Rocq Backend: Built upon coq_serapy, extending it to support systematic extraction of proof states and tactic traces, mapping them into the same unified format used for Lean.
• Unified State Model: Both assistants are mapped to a standardized state-transition system where a proof state is a set of obligations (goals and hypotheses), and tactics transition these states.

2. Data and Model Module

• Data Extraction: The framework extracts proof-state–tactic pairs from major repositories (CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory) by replaying tactic scripts inside the assistant's kernel.
• Unified Format: Extracted data is stored in a unified JSON format that abstracts over assistant-specific details while preserving semantic information. The prompt format for training is identical across Lean and Rocq, omitting assistant-specific tokens to facilitate cross-assistant training.
• Training: The authors fine-tuned a CodeT5-Base model (220M parameters) on three configurations:
  1. ProofWala-Rocq: Trained on Rocq repositories.
  2. ProofWala-Lean: Trained on Lean repositories.
  3. ProofWala-Multilingual: Trained jointly on both assistants.

3. Parallel Proof Search Module

• Environment Pooling: A key innovation is the environment pool, which maintains multiple cloned proof environments initialized to identical frontier states.
• Parallel Execution: Candidate tactics are executed concurrently across these cloned instances. This pool integrates with Ray for distributed execution, allowing scalable proof search and large-scale annotation.
• Search Algorithms: The module supports parallelized best-first and beam search. It maintains an annotated proof tree recording only valid, compilable state transitions, enabling fine-grained analysis of search dynamics.

Key Contributions

1. Standardized Framework and Engineering Library: ProofWala provides a unified framework for extracting and organizing tactic-level data and supporting tool development. It introduces a meta-programmed instrumentation pipeline for Lean that supports dependency-aware repository traversal and environment cloning, capabilities previously difficult to achieve via REPL.
2. Support for Parallel Proof Completion: The framework is the first open-source system to provide parallel proof search by explicitly supporting cloned proof environments and concurrent tactic evaluation within a unified multi-ITP interface.
3. Multilingual Datasets and Models: The authors release a multilingual dataset (~450K datapoints, 270M tokens) and trained models (Lean, Rocq, and Multilingual) that facilitate end-to-end proof search.

Results

The authors evaluated the models on test splits from CompCert, MathComp, GeoCoq, CategoryTheory, and Lean/Mathlib, as well as the MiniF2F benchmark.

• Cross-Lingual Transfer: The ProofWala-Multilingual model generally matches or improves upon monolingual baselines.
  • Statistically Significant Improvements: Observed on the largest benchmark (Lean/Mathlib) and in the CategoryTheory domain adaptation setting (where the multilingual model was fine-tuned on CategoryTheory data).
  • Trends: Other datasets showed consistent but not statistically significant trends favoring multilingual training.
• Domain Adaptation: In the CategoryTheory domain, the multilingual model achieved substantially higher pass-at-k scores after fine-tuning compared to the Rocq-only baseline, suggesting that pretraining on mixed-language data aids adaptation even when the target domain is represented in only one assistant.
• Search Dynamics: Analysis of proof trees revealed that multilingual models often produce larger trees with higher branching factors, indicating they propose a larger number of valid tactics per state.
• Scalability: Parallel execution via environment pools significantly improved throughput. Increasing CPU workers from 8 to 20 improved pass@5 on MiniF2F from 22.54% to 26.23% while reducing average proving time.

Significance and Claims

The paper claims that ProofWala represents a shift from fragmented, assistant-specific tooling to a unified, scalable infrastructure for neural theorem proving.

• Architectural Unification: By unifying execution, data collection, dependency analysis, and search, the framework enables systematic, reproducible, and fine-grained analysis of neural proof search across multiple ITPs.
• Evidence of Transfer: The work provides empirical evidence that multilingual training yields positive cross-lingual and cross-domain transfer in formal reasoning, particularly in high-data regimes and domain adaptation scenarios.
• Research Foundation: The authors position ProofWala not merely as a proof search system, but as a research framework that transforms proof search from a "black-box" evaluation into an analyzable pipeline. This allows researchers to study structural transfer, tree size, branching factors, and execution latency in ways previously difficult to obtain.

The authors note that while larger models and additional infrastructure (e.g., retrieval, verifiers) are likely needed for state-of-the-art performance on benchmarks, their primary contribution is the framework itself, which isolates the effects of multilingual training and parallel search strategies. They view the extension to document-oriented assistants (like Isabelle) as an engineering challenge rather than a conceptual limitation, leaving it for future work.