{"id":"546b4c9b-7eda-4f48-9ccf-e68785caab17","arxiv_id":"2508.18914","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.","lead":"FormaRL trains an AI to convert math problems into Lean formal statements using only unlabeled problems, combining Lean compiler checks with LLM semantic checks as rewards. It reports up to 6x accuracy gains on benchmarks and introduces a new undergraduate-level dataset, uproof.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"LLM consistency-check is both reward and evaluation metric; its low specificity and manual-review gap leave the reported 4–6× pass@1 gains unverified against ground truth.","rationale":"The reader's weakest assumption is exactly the evaluation/reward overlap: an LLM consistency check is used both as the RL reward and as the final metric. I agree, while crediting the paper for including a manual review and cross-judge checks. Those are partial mitigations but not sufficient to settle the concern, because the manual sample is small and does not recompute the headline pass@1 numbers, and the cross-judge checks still use LLM judges rather than ground truth. The core claim is the accuracy gain, and all reported gains funnel through CC; Section 4.3's specificity analysis and Table 7's manual-vs-LLM gap demonstrate a real false-positive risk. No internal contradiction or reproducibility problem was found: the training code is open-sourced, hyperparameters are detailed, and the paper explicitly acknowledges the reward-hacking possibility. Therefore the conditional verdict remains appropriate: the method is promising, but the quantitative headline needs external validation with a ground-truth equivalence check before full acceptance.","tokens_in":20797,"tokens_out":6008,"duration_ms":56482,"concrete_test":"On ProofNet, run the FormaRL-trained and SFT-baseline models at pass@1, keep only the first SC-pass candidate per problem, and replace the Qwen CC with automated equivalence checking against the dataset's ground-truth Lean statements, e.g., using bidirectional extended definitional equivalence (BEq, Liu et al. 2025) or a proof-checked equivalence between the generated and ground-truth statements. Recompute final pass@1 from these ground-truth labels. If FormaRL's true pass@1 does not exceed the SFT baseline by a substantial margin, the headlined 4–6× gain is an artifact of CC leniency; if the margin persists, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reported pass@1 numbers are computed with the same LLM consistency check (CC) that serves as the RL reward. Section 4.3 reports CC specificity of only 16.25% on ProofNet under pass@8 sampling, and even for first-SC-pass evaluation, Qwen2.5-7B-Instruct's CC has only ~80% specificity on ProofNet. Table 7's manual review finds human acceptance is ~12 points lower than LLM acceptance (38.8% vs. 50.4% for the FormaRL model). Because the headline improvements (4.04%->26.15% on ProofNet; 2.4%->9.6% on uproof) are computed under this noisy and potentially gameable judge, the claimed gain may be partly an artifact of the model learning to satisfy the CC judge rather than to preserve mathematical meaning. The paper's manual spot-check is small (100 samples) and is not used to recompute Tables 3/4 pass rates; cross-judge results in Table 10 still use three LLM judges, not ground-truth semantic equivalence. Thus the central quantitative claim is not yet verified against a semantically faithful metric.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"FormaRL trains an autoformalizer with GRPO using a reward composed of a Lean compiler syntax check (SC) and an LLM-based consistency check (CC), requiring no labeled translation pairs. The method is evaluated on miniF2F, ProofNet, and a newly curated undergraduate-level dataset, uproof. The paper reports large pass@1 gains for Qwen2.5-Coder-7B-Instruct (4.04%→26.15% on ProofNet, 2.4%→9.6% on uproof) using only 859 unlabeled statements, and claims out-of-distribution improvements over RAutoformalizer on uproof. The central contribution is the RL recipe plus the uproof benchmark, with training code open-sourced. The stress-test concern is valid: the evaluation metric is the same SC+CC pipeline used as the training reward, and the paper's own data show that CC has low specificity on advanced mathematics and that manual acceptance lags LLM acceptance by about 12 points.","tokens_in":21178,"tokens_out":6312,"duration_ms":56953,"significance":"If the reported gains are real, FormaRL would substantially reduce the data and annotation cost of training autoformalizers, which is an important result for the theorem-proving community. The paper also provides a useful new benchmark, uproof, and an open-source training pipeline. The ablation showing that both SC and CC are necessary to avoid degenerate solutions is a genuine strength, as is the use of a machine-checkable component (Lean compiler) in the reward. However, the headline quantitative claims are not yet verified against ground-truth semantic equivalence because the same noisy CC judge is both reward and evaluation metric. The significance of the contribution therefore hinges on whether the reported improvements survive an independent or human-based evaluation.","major_comments":[{"comment":"The headline pass@1 numbers are computed with the same SC+CC pipeline that serves as the RL reward (§4.1). The paper itself reports that CC specificity on ProofNet is only 79.68% for the evaluation model and drops to 16.25% under pass@8 sampling (§4.3), and Table 7 shows a 12-point gap between manual acceptance and Qwen2.5-7B acceptance (38.8% vs. 50.4%) for the FormaRL model. Because the RL objective directly optimizes SC+CC pass rate, the reported gains (4.04%→26.15% on ProofNet, 2.4%→9.6% on uproof) may substantially overstate improvement in semantically correct formalizations. Please recompute the key results with human-verified acceptance on a sufficiently large sample, or with an independent semantic-equivalence metric such as BEq (Liu et al., 2025), and report human-accepted pass@1/pass@k for FormaRL and baselines.","section":"§4.3, Tables 3–4, abstract"},{"comment":"The statement that “there is no evidence of reward hack” is not supported by the presented evidence. The manual review shows FormaRL’s human acceptance is 38.8% while the LLM judge accepts 50.4%, which is direct evidence that the evaluation metric overestimates correctness. The manual review is limited to 100 samples, is conducted post hoc, and is not used to recalibrate Tables 3/4. Table 10 substitutes other LLM judges, all sharing the same fundamental failure mode. To rule out reward overoptimization, the paper should compare human-accepted versus rejected outputs before and after RL and report whether the claimed improvement over SFT survives under manual labels.","section":"§5.3, Table 7"},{"comment":"The GRPO objective omits the KL regularization term (β = 0.0), as stated in §4.2 and Appendix A.5. With a noisy, false-positive-prone reward, the absence of a trust-region constraint increases the risk that the policy drifts toward outputs that exploit the CC judge. Current experiments do not measure this drift. Please include at least one training run with standard KL regularization or an explicit overoptimization analysis (e.g., human-accepted pass rate versus training step) to demonstrate that the reported gains are not an artifact of this design choice.","section":"§4.2, Eq. (1), Appendix A.5"}],"minor_comments":[{"comment":"The statement that “subsequent experiments rely solely on SC for selection” conflicts with §4.1, where reward requires both SC and CC, and with the SC/CC pass rates in Tables 3–4. Please clarify the exact evaluation protocol (e.g., first SC-pass candidate then CC) and how it applies to pass@8/pass@16.","section":"§4.3 vs. §4.1"},{"comment":"The uproof dataset is described but no download link or release plan is provided; only training code is open-sourced. Please make the dataset available or state its license and access conditions, as reproducibility of the benchmark is central.","section":"§5.1, Appendix A.3"},{"comment":"The row labels are ambiguous: it is not always clear which base model and method correspond to each row (e.g., the lone “FormaRL” rows vs. those after SFT). Add explicit model and method columns for every row.","section":"Tables 3 and 4"},{"comment":"Typos and minor errors: “GPRO” in Figure 1 should be “GRPO”; “promissing” in §5.3; “¯sorry” in §3; “wetcher” in the CC prompt (Appendix A.4); “FormaRL+R” in Table 11 is not defined.","section":"Throughout"},{"comment":"The claim that Lean Workbook is “in-distribution for all formalizers evaluated” is imprecise, since RAutoformalizer was trained on a different 243k corpus. This should be stated more carefully.","section":"§5.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is potentially interesting and the issue is fixable, but the central quantitative claim is not yet independently verified. I would not recommend acceptance before the authors recompute results with a human-verified or independent semantic-equivalence metric and address the reward-overoptimization concern explicitly. The uproof benchmark and open-source code are valuable, but the evaluation methodology is currently the bottleneck."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First: this is a real advance in the data-scarcity problem for autoformalization—training a 7B model on 859 unlabeled statements to beat SFT baselines trained on 25k+ pairs, with code and hyperparameters shipped, is worth taking seriously. Second: the exact size of the reported gains is not yet trustworthy. The same consistency check (CC) is the training reward and the evaluation metric, and the paper's own numbers show CC specificity at 16.25% on ProofNet under pass@8 and about 80% even for first-pass evaluation. When the judge is noisy and the model is optimizing that judge, some of the 4–6x improvement will be the model learning to satisfy the judge rather than to preserve meaning.\n\nWhat is solid. The GRPO-with-dual-reward recipe is a clean integration, and the ablation (w/o SC leads to trivial statements, w/o CC leads to non-formal natural language) demonstrates why both signals are needed. The uproof dataset, 5,273 problems from 14 textbooks, fills a real gap for OOD evaluation in advanced math. The paper is unusually candid: it reports the low specificity, reports a manual review showing human acceptance ~12 points lower than LLM acceptance, and provides cross-judge results with three LLM judges. None of that fully fixes the circularity, but it is more honest than most.\n\nWhere it is soft. The headline ProofNet number (4.04% -> 26.15%) is the weakest evidence because those statements were used for training (even if not their ground truth) and the metric is the reward. The uproof result is the most interesting because it is OOD, but even there the absolute numbers are modest and verified against an imperfect judge. The manual review is too small (100 samples) and is not applied to recompute the pass rates. Table 10 helps a little: FormaRL beats the baseline on ProofNet under all three judges, so the advantage is not an artifact of one judge; but the uproof gap between Qwen and the other two judges narrows considerably (8.6% vs 5.8%/5.4%). So the method looks genuinely better, but the magnitude is uncertain.\n\nBottom line: this deserves a serious referee. The central idea holds up at the qualitative level. What a referee should demand is an evaluation with ground-truth equivalence—e.g., using formal statement equivalence (BEq or similar) or a larger human-verified subsample—and a re-reporting of the headline numbers under that metric.\n\nFor you: read the uproof benchmark if you work on formalization; the method is worth citing for the recipe even before the judge problem is fixed.","headline":"A genuinely promising RL recipe for autoformalization whose headline numbers are probably inflated because the LLM judge is both the reward and the metric.","tokens_in":21574,"tokens_out":1995,"would_cite":true,"duration_ms":18220,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"FormaRL trains autoformalizers with no labeled pairs: Lean compiler syntax plus LLM consistency checks serve as the RL reward, lifting Qwen2.5-Coder-7B pass@1 from 4.04% to 26.15% on ProofNet and from 2.4% to 9.6% on the new uproof benchmar","keywords":["autoformalization","reinforcement learning","GRPO","Lean 4","consistency check","unlabeled data","theorem proving","benchmark"],"falsifier":"Have expert mathematicians (or a formal equivalence prover) judge a few hundred SC+CC-accepted FormaRL translations on ProofNet and uproof against their source problems: if the true equivalence rate falls far below the CC acceptance rate — consistent with the reported 16.25% specificity at pass@8 — the gains are partly judge permissiveness. Second probe: scan accepted outputs for degenerate statements ('False := sorry', dropped conditions); the paper's own no-CC ablation shows this collapse, so a nontrivial share would indicate reward hacking.","tokens_in":20765,"feed_emoji":"🧮","tokens_out":13439,"duration_ms":107813,"temperature":0.7,"pith_summary":"FormaRL is a reinforcement learning recipe for autoformalization — turning natural-language math problems into Lean 4 statements — that claims to need no labeled translation data at all. The training signal is a two-part automated reward: the Lean compiler verifies syntactic validity, and a large language model checks that the formal statement says the same thing as the original problem. With only 859 unlabeled statements from two existing benchmarks, FormaRL lifts pass@1 accuracy from 4.04% to 26.15% on ProofNet and from 2.4% to 9.6% on uproof, a new 5,273-problem benchmark the authors built from 14 undergraduate textbooks; it also beats the open-source state-of-the-art autoformalizer on out-of-distribution advanced math. If true, this removes the labeled-data bottleneck that has limited autoformalization and makes RL-with-compiler-feedback a viable path to formalizing advanced mathematics.","feed_headline":"859 unlabeled problems lift autoformalization accuracy 4-6x","feed_subtitle":"Compiler syntax plus LLM consistency checks as RL reward beat labeled-data training on advanced math.","key_machinery":"The reward function carries the argument: a formalization is rewarded 1.0 only when it survives both the Lean 4 compiler's syntax check (SC) and a judge LLM's consistency check (CC), which compares the formal statement with the original natural-language problem; every other output gets 0.0. At evaluation time only the first sampled candidate that passes SC proceeds to CC. The policy is updated with GRPO (Group Relative Policy Optimization), a group-relative-advantage RL algorithm, with the KL regularization term removed. The ablations show that a reward without either check is immediately gamed: without SC the model pastes natural language into its answer; without CC it emits a fixed trivial","core_discovery":"The central claim is that autoformalizers can be trained with no informal-formal translation pairs, using RL with a fully automated reward: a translation scores 1.0 only if it passes both the Lean 4 syntax check and an LLM consistency check for semantic equivalence to the source problem; anything else scores 0.0. With GRPO (no KL term) and only 859 unlabeled statements, this lifts Qwen2.5-Coder-7B from 4.04% to 26.15% pass@1 on ProofNet and from 2.4% to 9.6% on the new uproof benchmark, and beats the open-source state of the art out of distribution (6.2% → 9.6% pass@1; 24.4% → 33.6% pass@16). Ablations show both checks are required: without SC the model emits natural-language text; without C","pith_inferences":["The reported 16.25% CC specificity on ProofNet at pass@8 suggests the judge LLM, not the policy, is currently the ceiling; replacing the LLM with a formal equivalence check (e.g., bidirectional definitional equivalence) in the reward loop is the direct way to test how much headroom remains.","The same SC+CC reward scheme should extend to full proofs rather than statements by adding the prover's success or failure as a third check, which would make every reward component compiler-grounded.","Because the judge is itself an LLM, adversarial formalizations could in principle pass CC while being semantically wrong; the paper's multi-backend evaluation is a cheap canary for such gaming.","A testable variant: warm-start the policy with a small high-quality set of formalizations before RL — the paper's warm-up for DeepSeek-Math hints this could combine from-scratch headroom with faster convergence."],"forward_implications":["Autoformalization training can proceed from raw problem statements alone; the informal-formal pairs that SFT pipelines depend on are no longer required.","Data cost drops by roughly two orders of magnitude: 859 unlabeled statements replace the 25.2k-pair Lean Workbook set and the 243k-pair RAutoformalizer set used in these comparisons.","The gains transfer out-of-distribution to undergraduate-level advanced math: on uproof, FormaRL beats the open-source state of the art by 3.4 points at pass@1 and 9.2 points at pass@16.","The same recipe can be stacked on top of an SFT-trained formalizer for further gains, though improvement plateaus; the biggest lift comes from training from scratch.","Pipeline quality tracks the judge model: a weaker consistency-check backend erodes pass@8/pass@16 performance, though results still beat SFT baselines."],"supporting_citations":[{"why":"Supplies ProofNet, the advanced-math benchmark where the 4.04% to 26.15% gain is measured; its ground-truth formalizations are also used to measure CC recall.","marker":"(Azerbayev et al., 2023)"},{"why":"Supplies miniF2F, the elementary-math benchmark used as the second unlabeled training source and for in-distribution evaluation.","marker":"(Zheng et al., 2022)"},{"why":"Provides the SC+CC data-filtering method that FormaRL adapts as its reward, and the 25.2k-pair Lean Workbook set used to train SFT baselines.","marker":"(Ying et al., 2024)"},{"why":"The source of GRPO, the training algorithm, and of the DeepSeek-Math-7B base model tested in the paper.","marker":"(Shao et al., 2024)"},{"why":"The Qwen2.5-Coder-7B-Instruct base model that achieves the main reported improvements.","marker":"(Hui et al., 2024)"},{"why":"DeepSeek-V3, the judge model used for the consistency check during most training runs and evaluations.","marker":"(DeepSeek-AI et al., 2025b)"},{"why":"RAutoformalizer, the open-source state-of-the-art baseline that FormaRL outperforms on uproof.","marker":"(Liu et al., 2025)"},{"why":"DeepSeek-R1, the RL-at-scale precedent that motivates the GRPO-based training recipe.","marker":"(DeepSeek-AI et al., 2025a)"}],"fun_headline_variants":["No labeled data? RL autoformalizer jumps 4-6x accuracy","RL + Lean checks turn 859 unlabeled problems into 6x gain","Zero labeled data: compiler+LLM rewards boost autoformalization 6x","Lean syntax check as RL reward lifts autoformalization 4-6x"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The load-bearing premise is that the LLM consistency check reliably detects whether a formal statement means the same thing as the source problem; the paper itself reports (Section 4.3) that CC specificity drops to 16.25% on ProofNet under pass@8 sampling, and since the same check serves as both training reward and evaluation metric, a permissive judge could inflate both.","fun_headline_variants_meta":{"raw":{"variants":["No labeled data? RL autoformalizer jumps 4-6x accuracy","RL + Lean checks turn 859 unlabeled problems into 6x gain","Zero labeled data: compiler+LLM rewards boost autoformalization 6x","Lean syntax check as RL reward lifts autoformalization 4-6x"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000759,"raw_usage":{"total_tokens":3265,"prompt_tokens":860,"completion_tokens":2405,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":604,"completion_tokens_details":{"reasoning_tokens":2321}},"tokens_in":604,"tokens_out":2405,"duration_ms":16370,"temperature":1.0,"reasoning_tokens":2321,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T16:05:37.033318+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Have expert mathematicians (or a formal equivalence prover) judge a few hundred SC+CC-accepted FormaRL translations on ProofNet and uproof against their source problems: if the true equivalence rate falls far below the CC acceptance rate — consistent with the reported 16.25% specificity at pass@8 — the gains are partly judge permissiveness. Second probe: scan accepted outputs for degenerate statements ('False := sorry', dropped conditions); the paper's own no-CC ablation shows this collapse, so a nontrivial share would indicate reward hacking.","supporting_citations":[],"review_version":1}