ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving

TL;DR

This paper introduces ProofWala, a multilingual framework for neural theorem-proving that enables cross-ITP transfer and improves proof success rates through multilingual training and standardized interaction protocols.

Contribution

ProofWala provides a novel multilingual proof data synthesis framework and standardized interaction interface for neural theorem-provers across Coq and Lean, facilitating transfer learning.

Findings

Multilingual training improves transfer performance across ITPs.

ProofWala enables systematic evaluation of neural provers on multiple ITPs.

Models trained on multilingual data outperform single-ITP models on proof success metrics.

Abstract

Neural networks have shown substantial promise at automatic theorem-proving in interactive proof assistants (ITPs) like Lean and Coq. However, most neural theorem-proving models are restricted to specific ITPs, leaving out opportunities for cross-lingual $\textit{transfer}$ between ITPs. We address this weakness with a multilingual proof framework, ${\rm P{\small ROOF}W{\small ALA}}$, that allows a standardized form of interaction between neural theorem-provers and two established ITPs (Coq and Lean). It enables the collection of multilingual proof step data -- data recording the result of proof actions on ITP states -- for training neural provers. ${\rm P{\small ROOF}W{\small ALA}}$ allows the systematic evaluation of a model's performance across different ITPs and problem domains via efficient parallel proof search algorithms. We show that multilingual training enabled by ${\rm P{\small ROOF}W{\small ALA}}$ can lead to successful transfer across ITPs. Specifically, a model trained on a mix of ${\rm P{\small ROOF}W{\small ALA}}$-generated Coq and Lean data outperforms Lean-only and Coq-only models on the standard prove-at-$k$ metric. We open source all code including code for the ${\rm P{\small ROOF}W{\small ALA}}$ Framework (https://github.com/trishullab/proof-wala), and the Multilingual ITP interaction framework (https://github.com/trishullab/itp-interface).