FormaRL: Enhancing Autoformalization with no Labeled Data

Many thanks for your constructive comments. Responses to the aforementioned questions are as follows. We sincerely hope them to resolve the concerns.

If I understand correctly, the reward signal in GRPO relies on LLM-based checking. However, this introduces a potential concern: the reward may not be entirely reliable and could be susceptible to reward hacking due to the inherent limitations of LLMs in rigorous evaluation. Can the authors suggest alternative strategies to mitigate this issue?

Reward hacking is one of our primary concern as well, although in our experiments we believe that in our experiments there is no evidence of reward hack. We have also done some manual reviews on the outputs of RAutoformalizer and Qwen2.5-Coder-7B-Instruct trained with FormaRL, to further ensure the quality of formalizations and eliminate reward hack. We then compared the consistency check pass rate after passing syntax check under manual review and LLM-based checks, the results are summarized as follows.

We can see that manual review is typically more strict than LLM-based consistency checks, while the latter might allow some incorrect samples to be accepted. These results also indicates that there is no evidence of reward hack in our experiments. Models trained with FormaRL do not exhibit significant higher CC pass rate under LLM-based check than manual review. Compared with that of RAutoformalizer, this difference is reasonable.

In fact, in our previous experiments, as shown in Table 6 in our paper, the best results were not achieved by training with the same model as evaluation for CC. And if we consider their CC pass rate after passing SC (by dividing the final pass rate by the SC pass rate), FormaRL_(w/ qwen) actually performs worse than FormaRL_(w/ deepseek) in passing CC check, even though these metrics were evaluated under qwen.

Here are some possible explanations about this phenomenon. Unlike reward models that directly provide a score according to some specific patterns, LLM will reason before making its judgement, and thus is harder to be hacked. And the existence of syntax check via Lean compiler further limits the output format of the formalizers. Although in our experiments reward hacking may not be an issue, an more accurate evaluation method would also help achieve better performance (i.e., FormaRL_(w/ deepseek) can achieve higher performance than FormaRL_(w/ qwen)).

Furthermore, a recent related work [1] introduces symbolic consistency checking as a more rigorous alternative for evaluating the quality of autoformalization. I am curious how the LLM-based consistency checking compares to these symbolic approaches in terms of accuracy and robustness. Can the authors comment on whether LLM-based checking is competitive, or if it could be combined with symbolic methods for improved performance?

LLM-based evaluation approaches can be competitive in certain cases. In another recent paper [1], researchers have done some experiments and compared different evaluation metrics for autoformalization. In their experiments, majority voting via DeepSeek-V2.5 have achieved an overall accuracy of 82.50% (without the help of syntax check), which only falls behind their newly proposed BEq metric. In our quality assessment, both the recall and specificity of LLM-based consistency checks are around 80%, while syntax check would help further filter out incorrect samples.

Another advantage of LLM-based CC lies in obviating the requirement for annotated datasets, so that it can be applied on new datasets as a filtering method.

Nevertheless, these symbolic methods do exhibit higher precision and accuracy than LLM-based checks, and the idea of symbolic equivalence is really innovative and inspiring. I believe that we can achieve improved performance by integrating them with FormaRL. And with the help of RL, these symbolic methods could be directly adopted to enhance autoformalization, rather than merely serve as an evaluation metric. We are glad that we are the first to explore RL for autoformalization, and we are also looking forward to further experiments in this area.

[1] Q. Liu, X. Zheng, X. Lu, Q. Cao, and J. Yan, “Rethinking and improving autoformalization: towards a faithful metric and a Dependency Retrieval-based approach,” in The Thirteenth International Conference on Learning Representations, 2025. [Online]. Available: https://openreview.net/forum?id=hUb2At2DsQ

Many thanks for your detailed and thoughtful review! Here we will respond to each comment point by point. I hope this could resolve some of your concerns.

Lines 226-229, you claim that FromalRL on top of SFT can help improve further, but results plateau. I dont see those results in the paper or appendix. FormalRL should complement both SFT and RFormalizer, and potentially improve upon them. Some discussion with results around this would be good to have.

Sorry for not providing a reference in this paragraph. In fact, the relevant experimental results are already summarized in Table 3, 5.2, along with our major experimental results. We can see that RAutoformalizer is an autoformalizer trained via large scale SFT, and after performing FormaRL on this model we also observed some performance gains. The performance of SFT baselines are also summarized in this table for comparison.

Can you expand a bit on Table 10, A.6. What was the ablation trying to achieve?

Thank you for taking the time to carefully read the content in the appendix. In fact this table consists of some in-distribution evaluation metrics of the same base model trained with three different approaches (SFT on Lean Workbook, FormaRL, RAutoformalizer). Results showed that our SFT method could achieve comparable performance with RAutoformalizer, while FormaRL outperformed both. Since in-distribution performance is not our primary focus, we placed these results in the appendix instead of main part.

I was a bit surprised to see the data efficiency of this method - 859 examples only. Are there any variance numbers available for the results in terms of hyper parameter sensitivity?

In our early experiments we have tried many hyper parameter settings, and this RL training tend to be stable as long as the learning rate is not too high. In fact, current reinforcement learning from verifiable rewards (RLVR) tend to be quite efficient in data requirement compared to previous SFT-based methods. Before the submission of this paper, LIMR [1] already successfully incentived strong reasoning ability of an LLM with around 1k samples. Recently some experiments even showed that training on a single example could be effective as well [2]. And even for industrial-grade Qwen3 series models, only approximately 4k mathematical problems were utilized in the reinforcement learning stage [3]. The data efficiency and stability of RLVR was widely recognized across many researches, and we have just verified this in autoformalization.

How well does this method generalize to other theorem solvers - Isabelle and Coq?

I believe this method could naturally generalize to other theorem provers, since we only leverages Lean compiler to conduct syntax check without depending on any other specific features of Lean. This training recipe can be easily adopted for other formal languages as well.

[1] X. Li, H. Zou, and P. Liu, “LIMR: Less is More for RL Scaling.” [Online]. Available: https://arxiv.org/abs/2502.11886

[2] Y. Wang et al., “Reinforcement Learning for Reasoning in Large Language Models with One Training Example.” [Online]. Available: https://arxiv.org/abs/2504.20571

[3] A. Yang et al., “Qwen3 Technical Report.” [Online]. Available: https://arxiv.org/abs/2505.09388

Thank you for your insightful review!

You have pointed out one of our most important problem in our experiments, which we have paid a lot of attention to as well. To finally assess the output quality of our formalizers and the alignment of our evaluation metric, we have done some manual reviews on 200 samples separately generated by RAutoformalizer and Qwen2.5-Coder-7B-Instruct trained with FormaRL. We evaluated the consistency check pass rate after passing syntax check under manual review and LLM-based checks, the results are summarized as follows.

We can see that manual review is typically more strict than LLM-based consistency checks, while the latter might allow some incorrect samples to be accepted. Nevertheless, the LLM-based CC check still exhibits similar trend as manual review, a higher CC pass rate under Qwen2.5-7B-Instruct typically corresponds to higher actual pass rate. So it could be acceptable to used this as an evaluation metric.

These results also indicates that there is no evidence of reward hack in our experiments. Models trained with FormaRL do not exhibit significant higher CC pass rate under LLM-based check than manual review. Compared to that of RAutoformalizer, this difference is reasonable.

In fact, in our previous experiments, as shown in Table 6 in our paper, the best results were not achieved by training with the same model as evaluation for CC. And if we consider their CC pass rate after passing SC (by dividing the final pass rate by the SC pass rate), FormaRL_(w/ qwen) actually performs worse than FormaRL_(w/ deepseek) in passing CC check, even though these metrics were evaluated under qwen. These results already eliminated reward hack, and I think a manual review would provide a more direct evidence. We believe that FormaRL does achieved some progress in autoformalization.

Nevertheless, the evaluation metric adopted in our experiments does contain some flaws. Both the recall and specificity of LLM-based CC check are only around 80%, SC tend to be more reliable and can help eliminate more incorrect samples. This might impact the evaluation accuracy, but this does not affect our key experimental findings. In fact, the evaluation metric of autoformalization is still an area under exploration. Recently many new approaches [1][2][3] are proposed to enable more accurate evaluation for this, and they showed some superior performance than vanilla LLM-based checks. FormaRL exhibits better data efficiency and performance than SFT-based methods, and we believe that integrate this RL based method with better evaluation metric will further enhance the performance of autoformalization.

I hope this could resolve some of your concerns!

[1] Q. Liu, X. Zheng, X. Lu, Q. Cao, and J. Yan, “Rethinking and improving autoformalization: towards a faithful metric and a Dependency Retrieval-based approach,” in The Thirteenth International Conference on Learning Representations, 2025. [Online]. Available: https://openreview.net/forum?id=hUb2At2DsQ

[2] Z. Li et al., “Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency.” [Online]. Available: https://arxiv.org/abs/2410.20936

[3] J. Lu, Y. Wan, Y. Huang, J. Xiong, Z. Liu, and Z. Guo, “FormalAlign: Automated Alignment Evaluation for Autoformalization.” [Online]. Available: https://arxiv.org/abs/2410.10135

Thank you for your review! Below we respond to each comment point-by-point.

A comparative discussion between uproof and ProofNet would also be helpful, as both datasets potentially contain overlapping undergraduate-level math problems.

uproof is a large unlabeled dataset covering a wide range of mathematical topics, while ProofNet is a small manual curated dataset sourced from 8 undergraduate-level textbooks and Putnum competition. There might be some overlapping math problems, but considering that ProofNet only consists 371 problems, this may not be a problem.

Line 168: To assess recall, is a language model used to perform consistency checks between the generated autoformalizations and the ground-truth formal statements?

Yes, in fact we directly passed the problems in natural language in ProofNet or miniF2F dataset and its ground truth formalizations to the large language models. The pass rate of these ground truth formalizations is just the recall of consistency check with different models.

Line 171: Could variations in the algorithm for generating incorrect translations—such as altering statements to different degrees—impact the estimation of specificity?

You are right. Unlike the assessment of recall where we can directly evaluate on the ground truth formalizations, the assessment of specificity tend to be less reliable. Different formalizers tend to make different mistakes in autoformalization, so it is hard to evaluate a global specificity of our system. However, the estimation of specificity already provides valuable guidance for our evaluation metric. To preserve specificity we only use pass@n for syntax check and always use pass@1 for consistency check.

For futther quality assessment we have done some manual reviews on 200 samples separately generated by RAutoformalizer and Qwen2.5-Coder-7B-Instruct trained with FormaRL. The estimated specificity of these samples are separately 83.5% for RAutoformalizer and 81.0% for our formalizer. These results are a little bit better than our initial simulated experiments though.

I hope this could resolve some of your concerns.