FormaRL: Enhancing Autoformalization with no Labeled Data

TL;DR

FormaRL introduces a reinforcement learning framework for autoformalization that requires minimal unlabeled data, significantly improving accuracy and out-of-distribution performance in formal verification tasks.

Contribution

It presents a novel reinforcement learning approach for autoformalization that leverages syntax and consistency checks, with a curated dataset to facilitate research.

Findings

Increases autoformalization accuracy by 4-6x on key datasets.

Achieves significant improvements in out-of-distribution performance.

Operates effectively with only 859 unlabeled data points.

Abstract

Autoformalization is one of the central tasks in formal verification, while its advancement remains hindered due to the data scarcity and the absence efficient methods. In this work we propose \textbf{FormaRL}, a simple yet efficient reinforcement learning framework for autoformalization which only requires a small amount of unlabeled data. FormaRL integrates syntax check from Lean compiler and consistency check from large language model to calculate the reward, and adopts GRPO algorithm to update the formalizer. We also curated a proof problem dataset from undergraduate-level math materials, named \textbf{uproof}, in the hope to facilitate the exploration of autoformalization and theorem proving in advanced math. Experiments show that FormaRL can increase the pass@1 autoformalization accuracy of Qwen2.5-Coder-7B-Instruct by 4 $\sim$ 6x (4.04\% $\to$ 26.15\% on ProofNet and 2.4\% $\to$ 9.6\% on uproof) with merely 859 unlabeled data. And on uproof our method also achieved a strong improvement in out-of-distribution performance compared to existing open-source state-of-the-art autoformalizers on both pass@1 accuracy (6.2\% $\to$ 9.6\%) and pass@16 accuracy (24.4\% $\to$ 33.6\%). Training code of FormaRL is open-sourced at https://github.com/THUNLP-MT/FormaRL.