无需标注数据，用强化学习提升数学证明自动形式化效果
FormaRL: Enhancing Autoformalization with no Labeled Data
- 用大模型和Lean检查器做奖励信号，通过强化学习训练形式化模型
- 仅需859条无标签数据，准确率提升4到6倍，最高达26.15%
- 适合想做数学证明自动化但缺标注数据的研究者
自动形式化是形式化验证的核心任务，但受限于数据稀缺和方法效率不足。本文提出FormaRL，一种仅需少量无标签数据的强化学习框架。它结合Lean编译器的语法检查和大语言模型的一致性检查来计算奖励，并采用GRPO算法更新形式化器。我们还从本科生数学材料中构建了名为uproof的证明问题数据集，以促进高级数学证明研究。实验表明，FormaRL可将Qwen2.5-Coder-7B-Instruct在ProofNet上pass@1准确率从4.04%提升至26.15%，在uproof上从2.4%提升至9.6%，提升4~6倍。在uproof上，其对分布外样本的表现也显著优于现有开源先进方法：pass@1从6.2%提升至9.6%，pass@16从24.4%提升至33.6%。FormaRL训练代码已开源。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。