TLDR: FormaRL is a new reinforcement learning framework that significantly improves autoformalization accuracy by translating natural language math into formal languages like Lean. It achieves this with minimal unlabeled data (859 statements) by using a novel reward system combining Lean compiler syntax checks and LLM-based consistency checks. FormaRL boosted the accuracy of models like Qwen2.5-Coder-7B-Instruct by 4-6x and introduced a new dataset, uproof, for advanced math evaluation, demonstrating strong out-of-distribution performance.
The field of formal verification, which aims to ensure the correctness of mathematical statements and proofs using computer systems, relies heavily on a process called autoformalization. This is the task of translating mathematical concepts expressed in natural language into precise, machine-readable formal languages like Lean, Isabelle, or Coq. Despite its importance, autoformalization has faced significant hurdles, primarily due to the scarcity of labeled training data and the complexity of advanced mathematical concepts.
A new research paper introduces FormaRL, a novel reinforcement learning framework designed to overcome these challenges. What makes FormaRL particularly innovative is its ability to enhance autoformalization using only a small amount of unlabeled data, a stark contrast to traditional methods that demand extensive, costly human-annotated datasets.
How FormaRL Works
FormaRL operates on a reinforcement learning principle, where a model learns by receiving feedback (rewards) on its actions. The core of its efficiency lies in its unique reward calculation system, which eliminates the need for manual annotations:
- Syntax Check (SC): The Lean compiler automatically validates whether the generated formal statement is syntactically correct and forms a valid Lean 4 code. This is the first line of defense, ensuring the output is at least well-formed.
- Consistency Check (CC): After passing the syntax check, a large language model (LLM) evaluates the semantic alignment of the formal statement with the original natural language problem. This step ensures that the translation accurately captures the meaning and conditions of the original problem.
A formalization receives a reward of “1.0” only if it passes both the syntax and consistency checks; otherwise, it gets “0.0”. This dual-validation approach ensures robust feedback for the model. The framework then uses a simplified Group Relative Policy Optimization (GRPO) algorithm to update the formalizer, guiding it to produce better translations over time.
Introducing the uproof Dataset
To facilitate the evaluation of autoformalization, especially for advanced mathematics, the researchers also curated a new dataset called “uproof”. This dataset comprises 5,273 proof problems extracted from 14 classical undergraduate-level math textbooks, covering a wide array of topics from analysis to topology. uproof is particularly valuable for assessing how well models generalize to out-of-distribution mathematical problems, which are often more complex than those found in elementary math benchmarks.
Impressive Results with Less Data
Experiments demonstrated FormaRL’s superior performance. For instance, it increased the pass@1 autoformalization accuracy of the Qwen2.5-Coder-7B-Instruct model by approximately 4 to 6 times (from 4.04% to 26.15% on ProofNet and 2.4% to 9.6% on uproof). These significant gains were achieved with merely 859 unlabeled data statements from miniF2F and ProofNet, a dramatically smaller amount compared to the tens or hundreds of thousands of labeled examples required by existing supervised fine-tuning (SFT) methods.
On the uproof dataset, FormaRL also showed strong improvements in out-of-distribution performance, boosting pass@1 accuracy from 6.2% to 9.6% and pass@16 accuracy from 24.4% to 33.6% compared to existing open-source state-of-the-art autoformalizers. Ablation studies further confirmed that both the syntax and consistency checks are crucial for the framework’s effectiveness, preventing the model from “reward hacking” by generating irrelevant but syntactically correct statements.
Also Read:
- Unlocking Reasoning in Small Language Models: A New Approach to Blending Learning Strategies
- Enhancing Large Language Model Reasoning Through Contrastive Learning and Reinforced Fine-Tuning
Looking Ahead
FormaRL represents a significant step forward in autoformalization, offering an efficient and data-light approach to training models for this complex task. The open-sourced training code is available at THUNLP-MT/FormaRL. The researchers are optimistic about integrating more advanced evaluation and sampling methods into FormaRL, potentially pushing the boundaries of automated theorem proving in advanced mathematics even further.
