FormaRL：在无标注数据下增强自动形式化
人工智能
2025-08-27 v1
摘要
自动形式化是形式化验证中的核心任务之一，但其进展仍因数据稀缺和缺乏高效方法而受阻。在这项工作中，我们提出了FormaRL，一个简单而高效的用于自动形式化的强化学习框架，该框架仅需少量无标注数据。FormaRL 整合了来自 Lean 编译器的语法检查和来自大语言模型的一致性检查来计算奖励，并采用 GRPO 算法来更新形式化器。我们还从本科水平的数学材料中整理了一个名为 uproof 的证明问题数据集，希望能促进对高等数学中自动形式化和定理证明的探索。实验表明，仅使用 859 条无标注数据，FormaRL 就能将 Qwen2.5-Coder-7B-Instruct 的 pass@1 自动形式化准确率提高 4 到 6 倍（在 ProofNet 上从 4.04% 提高到 26.15%，在 uproof 上从 2.4% 提高到 9.6%）。在 uproof 上，与现有的开源最先进自动形式化器相比，我们的方法在分布外性能上也取得了显著提升，无论是 pass@1 准确率（6.2% 提高到 9.6%）还是 pass@16 准确率（24.4% 提高到 33.6%）。FormaRL 的训练代码已在 https://github.com/THUNLP-MT/FormaRL 开源。
引用
@article{arxiv.2508.18914,
title = {FormaRL: Enhancing Autoformalization with no Labeled Data},
author = {Yanxing Huang and Xinling Jin and Sijie Liang and Peng Li and Yang Liu},
journal= {arXiv preprint arXiv:2508.18914},
year = {2025}
}
备注
Conference paper at COLM2025