ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving

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 transfer between ITPs. We address this weakness with a multilingual proof framework, ${\rm P{\small ROOF}\rm 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}\rm 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}\rm W{\small ALA}}$ can lead to successful transfer across ITPs. Specifically, a model trained on a mix of ${\rm P{\small ROOF}\rm 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 our code, including code for the [${\rm P{\small ROOF}\rm W{\small ALA}}$ framework](https://anonymous.4open.science/r/proof-wala-CD44/README.md) and the [Multilingual ITP interaction framework](https://anonymous.4open.science/r/itp-interface-8F31/README.md).