Pith. sign in

REVIEW 3 major objections 5 minor 3 cited by

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

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection A genuinely promising RL recipe for autoformalization whose headline numbers are probably inflated because the LLM judge is both the reward and the metric. the 3 major comments →

arxiv 2508.18914 v1 pith:3ZJ75KGX submitted 2025-08-26 cs.AI

FormaRL: Enhancing Autoformalization with no Labeled Data

Yanxing Huang , Xinling Jin , Sijie Liang , Peng Li , Yang Liu This is my paper
classification cs.AI
keywords autoformalizationreinforcement learningGRPOLean 4consistency checkunlabeled datatheorem provingbenchmark
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

Core claim

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

What carries the argument

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

Load-bearing premise

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.

What would settle it

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.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • 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.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

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.

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 (3)
  1. [§4.3, Tables 3–4, abstract] 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.
  2. [§5.3, Table 7] 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.
  3. [§4.2, Eq. (1), Appendix A.5] 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.
minor comments (5)
  1. [§4.3 vs. §4.1] 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.
  2. [§5.1, Appendix A.3] 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.
  3. [Tables 3 and 4] 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.
  4. [Throughout] 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.
  5. [§5.2] 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.

Circularity Check

1 steps flagged

The reported autoformalization accuracy is the SC+CC reward itself; the headline pass@1 gains measure the optimized objective, not an independent ground-truth metric.

specific steps
  1. fitted input called prediction [Section 4.1 (Reward design) and Section 5.2/Table 4 caption (evaluation metric)]
    "For each response from the translation model, a reward of “1.0” is assigned only when it passed both SC and CC, otherwise the reward will always be “0.0”.” ... “for each test, we report the SC pass rate and the final pass rate after SC and CC."

    The final pass rate used in Tables 3/4 — and in the abstract's 4.04%→26.15% and 2.4%→9.6% claims — is exactly the SC∧CC criterion that defines the GRPO reward. Thus the reported 'autoformalization accuracy' is the training objective itself: a successful RL run will raise it even if the formalizations only satisfy the LLM judge. The paper's own Table 7 shows the LLM judge accepts 50.4% of FormaRL samples vs 38.8% under manual review, and the manual review is not used to recompute the headline numbers. Cross-judge checks (Table 10) still use three LLM judges, not ground-truth equivalence. This makes the central quantitative claim partially a report of reward optimization rather than an independent accuracy measurement.

full rationale

The paper's training pipeline is self-contained and does not rest on self-citations or imported uniqueness theorems; the Lean syntax check is machine-checked and the CC quality is benchmarked against ground truth in Table 1. The main circularity concern is that the evaluation metric (SC+CC pass rate) is the same function used as the RL reward. The paper explicitly acknowledges this risk and attempts to rebut reward hacking with a 100-sample manual review; however, the manual review reveals ~12-point inflation in the LLM judge and is not used to correct Tables 3/4. The use of a different LLM for evaluation (Qwen2.5-7B) than for training (DeepSeek-V3) and the uproof OOD results give some independent content, so this is not a complete collapse. But the headline pass@1 improvements are measured with the same noisy, potentially gameable judge that the model was trained to satisfy. Score 6 reflects partial circularity: one central 'prediction' reduces to the optimized reward.

Axiom & Free-Parameter Ledger

5 free parameters · 4 axioms · 0 invented entities

The central claim rests on the reliability of the SC+CC reward as a measure of true autoformalization correctness. The CC is a learned model with imperfect specificity, and the paper's evaluation uses the same type of check, so the improvement could partly reflect reward optimization rather than genuine generalization.

free parameters (5)
  • learning_rate = 1e-6
    Set in Appendix A.5; not fitted to data.
  • grpo_beta = 0.0
    KL regularization omitted; chosen to reduce compute.
  • num_generations = 4
    GRPO group size.
  • train_epochs = 3
    Number of RL epochs.
  • reward_value = 1.0 for pass, 0.0 otherwise
    Binary reward chosen by design.
axioms (4)
  • domain assumption LLM-based consistency check is a reliable proxy for semantic equivalence.
    The whole method depends on CC accuracy; the paper tests recall/specificity but notes specificity drops sharply on ProofNet (Section 4.3).
  • standard math Lean compiler syntax check is a valid gate for well-formed statements.
    Assumed throughout; Lean is a widely used proof assistant.
  • domain assumption GRPO without KL penalty is stable and effective for this task.
    Cited from Meng et al. (2024) and Yu et al. (2025).
  • ad hoc to paper Automated extraction of problems from textbooks using GPT-4o yields correct and complete problems.
    The uproof construction uses GPT-4o for extraction and validation (Section 5.1, Appendix A.2). No manual verification reported.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of FormaRL: Enhancing Autoformalization with no Labeled Data." pith.science (2026). https://pith.science/paper/3ZJ75KGX

@misc{pith2026250818914,
  author       = {Pith},
  title        = {Pith review of: FormaRL: Enhancing Autoformalization with no Labeled Data},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3ZJ75KGX}},
  note         = {Machine review of arXiv:2508.18914}
}
Share X Bluesky LinkedIn Reddit HN
abstract

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.

Figures

Figures reproduced from arXiv: 2508.18914 by Peng Li, Sijie Liang, Xinling Jin, Yang Liu, Yanxing Huang.

Figure 1
Figure 1. Figure 1: Illustration of FormaRL training loop. We combined lean syntax check from [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization

    cs.LG 2026-04 unverdicted novelty 6.0

    Disjoint SFT and GRPO data for autoformalization yields up to 10.4pp semantic accuracy gains over full overlap, which renders the GRPO stage redundant.

  2. Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

    cs.AI 2025-10 conditional novelty 6.0

    A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.

  3. A Survey of Reinforcement Learning for Large Reasoning Models

    cs.CL 2025-09 accept novelty 3.0

    A survey compiling RL methods, challenges, data resources, and applications for enhancing reasoning in large language models and large reasoning models since DeepSeek-R1.

Reference graph

Works this paper leans on

46 extracted references · 8 canonical work pages · cited by 3 Pith papers · 2 internal anchors

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should not add it explicitly Type <Return> for now, but then later remove the command n...

  3. [3]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@first@sw \@firstoftwo \@ifundefined NAT@b*@#2 \@firstoftwo @num @NAT@ctr \@secondoft...

  4. [4]

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibsetup #1 @NAT@ctr @ @openbib .11em \@plus.33em \@minus.07em 4000 4000 `\.\@m @bibit...

    work page

  5. [5]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet : Autoformalizing and formally proving undergraduate-level mathematics, 2023. URL https://arxiv.org/abs/2302.12433v1

    Pith/arXiv arXiv 2023

  6. [6]

    Deepmind hits milestone in solving maths problems—AI’s next grand challenge

    Davide Castelvecchi. Deepmind hits milestone in solving maths problems—AI’s next grand challenge . Nature, 632 0 (8024): 0 236--237, 2024

    work page 2024

  7. [7]

    Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

    Garett Cunningham, Razvan C. Bunescu, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs, 2023. URL http://arxiv.org/abs/2301.02195

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  8. [8]

    DeepSeek - AI , Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Dama...

    Pith/arXiv arXiv 2025

  9. [9]

    Zhang, Han Bao, Hanwei Xu, Haocheng Wang, Haowei Zhang, Honghui Ding, Huajian Xin, Huazuo Gao, Hui Li, Hui Qu, J

    DeepSeek - AI , Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Daya Guo, Dejian Yang, Deli Chen, Dongjie Ji, Erhang Li, Fangyun Lin, Fucong Dai, Fuli Luo, Guangbo Hao, Guanting Chen, Guowei Li, H. Zhang, Han Bao, Hanwei Xu, Haocheng Wang, Haowei Zhang, Honghui Ding, H...

    Pith/arXiv arXiv 2025

  10. [10]

    Qwen2.5-coder technical report, 2024

    Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jiajun Zhang, Bowen Yu, Keming Lu, Kai Dang, Yang Fan, Yichang Zhang, An Yang, Rui Men, Fei Huang, Bo Zheng, Yibo Miao, Shanghaoran Quan, Yunlong Feng, Xingzhang Ren, Xuancheng Ren, Jingren Zhou, and Junyang Lin. Qwen2.5-coder technical report, 2024. URL http://arxiv.org/ab...

    Pith/arXiv arXiv 2024

  11. [11]

    Jiang, Wenda Li, and Mateja Jamnik

    Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. URL http://arxiv.org/abs/2311.03755

    Pith/arXiv arXiv

  12. [12]

    Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample

    Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs, 2023. URL http://arxiv.org/abs/2210.12283

    Pith/arXiv arXiv 2023

  13. [13]

    LIMR : Less is more for RL scaling, 2025

    Xuefeng Li, Haoyang Zou, and Pengfei Liu. LIMR : Less is more for RL scaling, 2025. URL http://arxiv.org/abs/2502.11886

    Pith/arXiv arXiv 2025

  14. [14]

    HUNYUANPROVER : A scalable data synthesis framework and guided tree search for automated theorem proving, 2024 a

    Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. HUNYUANPROVER : A scalable data synthesis framework and guided tree search for automated theorem proving, 2024 a . URL http://arxiv.org/abs/2412.20735

    Pith/arXiv arXiv 2024

  15. [15]

    A survey on deep learning for theorem proving, 2024 b

    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, 2024 b . URL http://arxiv.org/abs/2404.09939

    Pith/arXiv arXiv 2024

  16. [16]

    Let's verify step by step, 2023

    Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step, 2023. URL http://arxiv.org/abs/2305.20050

    Pith/arXiv arXiv 2023

  17. [17]

    Goedel-prover: A frontier model for open-source automated theorem proving, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL http://arxiv.org/abs/2502.07640. version: 1

    Pith/arXiv arXiv 2025

  18. [18]

    Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach

    Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=hUb2At2DsQ

    work page 2025

  19. [19]

    SimPO : Simple preference optimization with a reference-free reward, 2024

    Yu Meng, Mengzhou Xia, and Danqi Chen. SimPO : Simple preference optimization with a reference-free reward, 2024. URL http://arxiv.org/abs/2405.14734

    Pith/arXiv arXiv 2024

  20. [20]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Andr \'e Platzer and Geoff Sutcliffe (eds.), Automated Deduction -- CADE 28, pp.\ 625--635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5

    work page 2021

  21. [21]

    Autoformalizing euclidean geometry, 2024

    Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry, 2024. URL http://arxiv.org/abs/2405.17216

    Pith/arXiv arXiv 2024

  22. [22]

    Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, A

    OpenAI , Aaron Hurst, Adam Lerer, Adam P. Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, A. J. Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, Aleksander Mądry, Alex Baker-Whitcomb, Alex Beutel, Alex Borzunov, Alex Carney, Alex Chow, Alex Kirillov, Alex Nichol, Alex Paino, Alex Renzin, Alex Tachard Passos, Alexander Kirillov, Alexi Christakis, Ale...

    Pith/arXiv arXiv 2024

  23. [23]

    OpenAI , Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, Ally Bennett, Ananya Kumar, Andre Saraiva, Andrea Vallone, Andrew Duberstein, Andrew Kondrich...

    Pith/arXiv arXiv 2024

  24. [24]

    Long Ouyang, Jeff Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul Christiano, Jan Leike, and Ryan Lowe. Training language models to follow instructions with human feedback,...

    Pith/arXiv arXiv 2022

  25. [25]

    A New Approach Towards Autoformalization

    Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization. URL http://arxiv.org/abs/2310.07957

    work page internal anchor Pith review Pith/arXiv arXiv

  26. [26]

    Improving autoformalization using type checking, 2024

    Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformalization using type checking, 2024. URL http://arxiv.org/abs/2406.07222

    arXiv 2024

  27. [27]

    Qwen2.5 technical report, 2024

    Qwen, An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, Huan Lin, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jingren Zhou, Junyang Lin, Kai Dang, Keming Lu, Keqin Bao, Kexin Yang, Le Yu, Mei Li, Mingfeng Xue, Pei Zhang, Qin Zhu, Rui Men, Runji Lin, Tianhao Li, Ti...

    Pith/arXiv arXiv 2024

  28. [28]

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. DeepSeekMath : Pushing the limits of mathematical reasoning in open language models, 2024. URL http://arxiv.org/abs/2402.03300

    Pith/arXiv arXiv 2024

  29. [29]

    Kimi Team, Angang Du, Bofei Gao, Bowei Xing, Changjiu Jiang, Cheng Chen, Cheng Li, Chenjun Xiao, Chenzhuang Du, Chonghua Liao, Chuning Tang, Congcong Wang, Dehao Zhang, Enming Yuan, Enzhe Lu, Fengxiang Tang, Flood Sung, Guangda Wei, Guokun Lai, Haiqing Guo, Han Zhu, Hao Ding, Hao Hu, Hao Yang, Hao Zhang, Haotian Yao, Haotian Zhao, Haoyu Lu, Haoze Li, Haoz...

    Pith/arXiv arXiv 2025

  30. [30]

    Paulson Tobias Nipkow, Markus Wenzel

    Lawrence C. Paulson Tobias Nipkow, Markus Wenzel. Isabelle/hol: A proof assistant for higher-order logic. Springer Berlin, Heidelberg, 2002

    work page 2002

  31. [31]

    Trl: Transformer reinforcement learning

    Leandro von Werra, Younes Belkada, Lewis Tunstall, Edward Beeching, Tristan Thrush, Nathan Lambert, Shengyi Huang, Kashif Rasul, and Quentin Gallouédec. Trl: Transformer reinforcement learning. https://github.com/huggingface/trl, 2020

    2020

  32. [32]

    NaturalProofs : Mathematical theorem proving in natural language, 2021

    Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. NaturalProofs : Mathematical theorem proving in natural language, 2021. URL http://arxiv.org/abs/2104.01112

    Pith/arXiv arXiv 2021

  33. [33]

    Jiang, Wenda Li, Markus N

    Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022. URL http://arxiv.org/abs/2205.12615

    Pith/arXiv arXiv 2022

  34. [34]

    InternLM 2.5- StepProver : Advancing automated theorem proving via expert iteration on large-scale LEAN problems, 2024

    Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. InternLM 2.5- StepProver : Advancing automated theorem proving via expert iteration on large-scale LEAN problems, 2024. URL http://arxiv.org/abs/2410.15700

    arXiv 2024

  35. [35]

    DeepSeek -prover: Advancing theorem proving in LLMs through large-scale synthetic data, 2024 a

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek -prover: Advancing theorem proving in LLMs through large-scale synthetic data, 2024 a . URL http://arxiv.org/abs/2405.14333

    Pith/arXiv arXiv 2024

  36. [36]

    Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. DeepSeek -prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search, 2024 b . URL http://arxiv.org/abs/2408.08152

    Pith/arXiv arXiv 2024

  37. [37]

    BFS -prover: Scalable best-first tree search for LLM -based automatic theorem proving, 2025

    Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. BFS -prover: Scalable best-first tree search for LLM -based automatic theorem proving, 2025. URL http://arxiv.org/abs/2502.03438

    arXiv 2025

  38. [38]

    Qwen2 technical report, 2024 a

    An Yang, Baosong Yang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Zhou, Chengpeng Li, Chengyuan Li, Dayiheng Liu, Fei Huang, Guanting Dong, Haoran Wei, Huan Lin, Jialong Tang, Jialin Wang, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Ma, Jianxin Yang, Jin Xu, Jingren Zhou, Jinze Bai, Jinzheng He, Junyang Lin, Kai Dang, Keming Lu, Keqin Chen, Kexin Yang, Mei...

    Pith/arXiv arXiv 2024

  39. [39]

    Formal mathematical reasoning: A new frontier in AI , 2024 b

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI , 2024 b . URL http://arxiv.org/abs/2412.16075

    Pith/arXiv arXiv 2024

  40. [40]

    Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024. URL http://arxiv.org/abs/2406.03847

    Pith/arXiv arXiv 2024

  41. [41]

    DAPO : An open-source LLM reinforcement learning system at scale, 2025

    Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Tiantian Fan, Gaohong Liu, Lingjun Liu, Xin Liu, Haibin Lin, Zhiqi Lin, Bole Ma, Guangming Sheng, Yuxuan Tong, Chi Zhang, Mofan Zhang, Wang Zhang, Hang Zhu, Jinhua Zhu, Jiaze Chen, Jiangjie Chen, Chengyi Wang, Hongli Yu, Weinan Dai, Yuxuan Song, Xiangpeng Wei, Hao Zhou, Jingjing Liu, W...

    Pith/arXiv arXiv 2025

  42. [42]

    Interactive theorem proving and program development

    Pierre Castéran Yves Bertot. Interactive theorem proving and program development. Springer Berlin, Heidelberg, 2013

    work page 2013

  43. [43]

    7b model and 8k examples: Emerging reasoning with reinforcement learning is both effective and efficient

    Weihao Zeng, Yuzhen Huang, Wei Liu, Keqing He, Qian Liu, Zejun Ma, and Junxian He. 7b model and 8k examples: Emerging reasoning with reinforcement learning is both effective and efficient. https://hkust-nlp.notion.site/simplerl-reason, 2025. Notion Blog

    2025

  44. [44]

    Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving, 2023

    Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving, 2023. URL http://arxiv.org/abs/2305.16366

    Pith/arXiv arXiv 2023

  45. [45]

    MiniF 2f: a cross-system benchmark for formal olympiad-level mathematics, 2022

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF 2f: a cross-system benchmark for formal olympiad-level mathematics, 2022. URL http://arxiv.org/abs/2109.00110

    Pith/arXiv arXiv 2022

  46. [46]

    Ziegler, Nisan Stiennon, Jeffrey Wu, Tom B

    Daniel M. Ziegler, Nisan Stiennon, Jeffrey Wu, Tom B. Brown, Alec Radford, Dario Amodei, Paul Christiano, and Geoffrey Irving. Fine-tuning language models from human preferences, 2020. URL http://arxiv.org/abs/1909.08593

    Pith/arXiv arXiv 2020

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.