Back

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

Kefan DongTengyu Ma

article2025ICML54 citations

Presents Self-play Theorem Prover, a dual-agent framework where a language model alternates between generating challenging mathematical conjectures and proving them, doubling previous training success rates on LeanWorkbook and achieving state-of-the-art results on competitive benchmarks like miniF2F.

Listen

Formal mathematical reasoning using large language models has become a central benchmark for artificial intelligence. However, standard reinforcement learning and expert iteration methods—which alternate between sampling proofs and retraining on correct ones—consistently plateau because correct proofs for challenging problems are exceedingly rare. As a result, massive amounts of compute are wasted generating incorrect proofs, leaving models unable to self-improve without continuous human-annotated data.

The article introduces the Self-play Theorem Prover, an automated framework designed to overcome this data scarcity by enabling continuous self-improvement. The study evaluates whether a dual-role self-play architecture can generate its own adaptive curriculum of mathematical conjectures and proofs to improve formal proving performance in systems like Lean and Isabelle.

The researchers designed an architecture where a single model simultaneously acts as a conjecturer, proposing new mathematical statements derived from existing seeds, and a prover, attempting to solve both dataset problems and newly generated conjectures. The conjecturer is iteratively trained on generated conjectures that are approachable yet challenging (where the prover succeeds with positive but low probability) and filtered for elegancy and diversity. The prover is trained on verified solutions. The method was evaluated using Lean 4 on the LeanWorkbook, miniF2F, ProofNet, and PutnamBench datasets, as well as an Isabelle-translated suite using the Llemma-7b base model.

The primary finding is that the Self-play Theorem Prover doubles existing performance benchmarks on training datasets, solving 28.5% of LeanWorkbook statements compared to the prior best result of 13.1% achieved by standard expert iteration. Second, the generated conjectures provide dense training signals: at least 47% of generated conjectures yielded successful proofs during training, compared to standard iteration where fewer than 0.01% of proof attempts on unproven dataset statements succeeded. Third, the final model establishes state-of-the-art results for whole-proof generation methods across multiple benchmarks at 3,200 samples per problem, achieving 65.0% on miniF2F-test, 23.9% on ProofNet-test, and solving 8 out of 644 undergraduate-level competition problems in PutnamBench.

These results demonstrate that automated mathematical goal generation can prevent learning saturation and eliminate the need for ever-larger human-labeled formal datasets. By structuring an adaptive difficulty curve internally, organizations can significantly reduce wasted compute during model training while achieving higher performance on complex reasoning tasks.

For future development, the article recommends incorporating tree search algorithms alongside self-play generation to further expand proof-search capabilities. In addition, practitioners should curate cleaner formal datasets; manual auditing of unproven benchmark problems revealed that 13 out of 20 sampled unproven statements were mathematically flawed or unprovable due to translation errors, setting a natural ceiling on benchmark accuracy. Confidence in the core performance gains is high across both Lean and Isabelle environments, though users should account for the fact that benchmark pass rates are constrained by errors in automated statement formalization.

Stanford Universitytheorem proversdecision procedureproof systemself-play LLM theorem proversiterative conjecturingwhole-proof generation methods
arXiv: 2502.00212kfdong/STP
Cover for STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

Abstract

A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal verifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.1% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0%), ProofNet-test (23.9%) and PutnamBench (8/644) with pass@3200.

Topics

theorem proversdecision procedureproof system

Keywords

self-play LLM theorem proversiterative conjecturingwhole-proof generation methodsexpert iterationproof verificationformal proofsself-play training

Table of Contents

  • 1. Introduction
  • 2. Additional Related Works
  • 3. Method
  • 3.1. Model initialization by supervised finetuning
  • 3.2. Self-play training
  • 3.3. Final re-training
  • 4. Experiments
  • 4.1. Implementation details
  • 4.2. Results with Lean
  • 4.3. Results with Isabelle
  • 4.4. Ablation study
  • 4.5. Analysis of generated conjectures
  • 4.6. Examples of generated conjectures
  • 5. Conclusion
  • Impact Statement
  • Acknowledgment
  • References
  • A. Additional Implementation Details
  • A.1. Examples of inputs and outputs of our model
  • A.2. Pseudo-code for selecting the conjecturer's inputs
  • A.3. Pseudo-code for preparing the conjecturer dataset.
  • A.4. Pre-processing LeanWorkbook
  • A.5. Re-weighting the conjecturing dataset
  • A.6. Implementation details for expert iteration.
  • A.7. Additional details for interacting with the Isabelle verifier
  • A.8. Additional details for interacting with the Lean4 verifier
  • A.9. Compute resources
  • B. Additional Experiment Results
  • B.1. Additional results with Lean
  • B.2. Additional results with Isabelle
  • B.3. Examples of unproved statements in LeanWorkbook
  • B.4. Most frequent shared lemmas in Lean

Knowls

  1. Knowl 1 — STP trains a conjecturer and prover through an adaptive self-play curriculum

    model/method

    Self-play Theorem Prover (STP) trains one language model to play two roles. The conjecturer receives a seed theorem, its proof, and a lemma used in that proof, then proposes a related formal conjecture. The prover attempts proofs for both generated conjectures and still-unproved statements from an existing dataset; a formal verifier checks the generated proofs. Verified proofs provide training examples for the prover, while a selected subset of generated conjectures provides supervision for the conjecturer. In each iteration, the prover’s sampling budget is split between dataset statements and conjectures, with the number of conjectures capped by the number of unproved dataset statements. By training the conjecturer on conjectures that the current prover can solve but does not solve reliably, STP creates an increasingly challenging curriculum without requiring additional human-authored theorem statements.

  2. Knowl 2 — Conjecturer training selects provable, lemma-related, nontrivial, and elegant conjectures

    model/method

    For a generated conjecture cc, STP estimates the current prover’s pass rate as P^(c)=s(c)/n(c)\hat P(c)=s(c)/n(c), where n(c)n(c) is the number of independently sampled proofs of cc and s(c)s(c) is the number verified as correct. A conjecture is eligible for conjecturer training only if 0<P^(c)≤1/40<\hat P(c)\leq 1/4, at least one generated proof is correct, and the lemma supplied with the seed theorem is used in that proof. Duplicate conjectures are removed. To discourage goals that are artificially hard because they require disproportionately long proofs, STP computes the shortest verified proof length divided by the conjecture length and removes eligible conjectures in the lowest 20% of this score. The remaining conjectures train the conjecturer using the seed theorem, its proof, and the lemma as input, with the conjecture as the target.

  3. Knowl 3 — STP improves Lean proof generation and benchmark performance

    empirical result

    Starting from DeepSeek-Prover-V1.5-SFT, the Lean STP run generated 3.6 million conjectures, 241 million proofs, and 51.3 billion tokens over 48 iterations. Its cumulative pass rate on LeanWorkbook reached 28.5%, compared with the prior expert-iteration result of 13.1%. On miniF2F-test and ProofNet-test, STP’s whole-proof generation results were:

    Method Proof samples per problem miniF2F-test ProofNet-test
    STP 128 61.2% ±\pm 0.6% 19.5% ±\pm 0.7%
    STP 3,200 65.0% ±\pm 0.5% 23.9% ±\pm 0.6%
    STP 25,600 67.6% 26.9%
    DeepSeek-Prover-V1.5-RL 128 51.6% ±\pm 0.5% 18.2% ±\pm 0.5%
    DeepSeek-Prover-V1.5-RL 3,200 54.9% ±\pm 0.7% 22.0% ±\pm 0.5%
    DeepSeek-Prover-V1.5-RL 25,600 58.4% ±\pm 0.6% 23.7%

    Pass@k is the fraction of benchmark statements for which at least one of kk independently sampled proofs succeeds. On PutnamBench, STP solved 7 of 644 problems with 128 proof samples per problem and 8 of 644 with 3,200 samples. These results establish the reported gains both on the LeanWorkbook training corpus and on formalized evaluation benchmarks.

  4. Knowl 4 — Wasserstein reweighting counters conjecture mode collapse

    model/method

    STP reweights eligible conjectures to make their distribution resemble the distribution of unproved statements, helping preserve topic diversity. Let XX be the eligible generated conjectures and let QQ be the uniform distribution on the unproved statements. The cost of matching conjecture x∈Xx\in X to statement yy is the negative cosine similarity of their embeddings; each embedding is the current model’s last-layer hidden states averaged over the sequence. STP seeks a distribution PP supported on XX that minimizes the Wasserstein transport cost to QQ. In the idealized transport solution, each statement’s mass is assigned to its closest conjecture, and conjecture weights are scaled so their total equals the number of generated conjectures.

    The practical procedure caps the weight of an individual conjecture. For each unproved statement, it assigns its matching mass to the kk closest conjectures, where kk is that statement’s matching weight, and updates a mask after a conjecture’s accumulated scaled weight exceeds 3. LeanWorkbook statements have matching weight 1; miniF2F-valid and ProofNet-valid statements have weight 1 for the first 24 Lean iterations and 128 thereafter. The authors report that this reweighting was introduced after observing conjecture topic collapse, such as algebraic conjectures dominating even when seed statements concerned other topics.

  5. Knowl 5 — Isabelle experiments show improved scaling and denser conjecture rewards

    empirical result

    With the math-focused Llemma-7b model, STP ran 58 Isabelle iterations and generated about 300 million proofs. LeanWorkbook statements were translated into Isabelle using few-shot prompting. The experiments disabled the CPU-intensive tactics sledgehammer, mason, smt, metis, and sos, and compared STP with expert iteration and parallel sampling from multiple STP checkpoints. STP achieved better cumulative pass-rate scaling than both baselines from checkpoints with different starting capabilities, and the model’s miniF2F performance improved during training.

    The contrast in available prover feedback illustrates why conjectures help: at a checkpoint with an 11.4% cumulative pass rate on the Isabelle translation of LeanWorkbook, only 131 of 2.5 million proofs sampled for 79,000 unproved dataset statements were correct. By contrast, at least 47% of the generated conjectures during STP training were successfully proved. In a late Lean checkpoint, 51.1% of correct conjecture proofs shared at least one lemma with the seed theorem’s proof; 17 of the 20 most frequent lemmas in conjecture proofs also appeared among the 20 most frequent lemmas in LeanWorkbook proofs.

  6. Knowl 6 — The prover trains on verified nontrivial proofs from recent iterations

    model/method

    In each STP iteration, the prover samples K=32K=32 independent proofs for each statement or conjecture under consideration. Prover training retains only verified proofs whose target has empirical pass rate below 1/21/2; the paper treats correct proofs for targets at or above that rate as trivial training examples. Retained proofs are deduplicated by exact match. The prover is trained from a replay buffer containing retained proofs from the last three iterations, rather than from the full history at every update. Generated conjectures are sampled in a number no greater than the remaining unproved statements, so the proof-sampling compute is divided equally between conjectures and dataset statements.

  7. Knowl 7 — Supervised initialization teaches both formal proving and conjecturing

    model/method

    STP initializes its two roles by supervised fine-tuning a general language model on formal proof-library data. Prover examples consist of a system prompt, a theorem statement, and its human-written proof; next-token loss is computed on the proof, not on the prompt or statement. Conjecturer examples are ordered triples (lemma,theorem X,theorem Y)(\text{lemma},\text{theorem X},\text{theorem Y}) extracted from a proof-library file when the lemma occurs before both theorems and is used in proofs of both. The conjecturer receives the lemma and theorem X with its proof and is trained to generate theorem Y. A fixed trivial lemma is also allowed so the model can generate conjectures without being directed by a particular proof lemma.

  8. Knowl 8 — Training weights favor simpler proofs and final retraining consolidates verified data

    model/method

    STP uses weighted cross-entropy on generated proof or conjecture targets, excluding the input tokens from the loss. For proof examples, the weight is inversely proportional to the number of verified proofs for the corresponding statement or conjecture, and a length penalty γL\gamma^L favors shorter proofs, where LL is proof length and γ=exp⁡(−0.001)\gamma=\exp(-0.001). In Lean, a verification-time penalty βT\beta^T is also applied, where TT is Lean execution time and β=exp⁡(−0.01)\beta=\exp(-0.01). STP training uses Adam with batch size 2,048 and learning rate 5×10−55\times10^{-5}; supervised initialization and final retraining use learning rate 10−410^{-4}.

    To reduce instability from the changing self-play data distribution, the final model is retrained from the base checkpoint before supervised fine-tuning, on the combination of the supervised fine-tuning data and correct proofs generated during self-play for targets with empirical pass rate at most 1/41/4. At most 16 distinct proofs are kept per target.

  9. Knowl 9 — Including generated conjecture proofs improves downstream retraining results

    empirical result

    The authors compared final retraining with and without verified proofs of generated conjectures, while retaining the successfully proved LeanWorkbook statements. At 128 inference samples per problem, including conjecture proofs increased miniF2F-test pass rate from 58.3%±0.7%58.3\%\pm0.7\% to 61.2%±0.6%61.2\%\pm0.6\%, and ProofNet-test pass rate from 17.4%±0.4%17.4\%\pm0.4\% to 19.5%±0.7%19.5\%\pm0.7\%. The reported result shows that the value of generated conjectures is not confined to improving the pass rate on the self-play training corpus: their proofs also provide useful data for final-model performance on these benchmarks.

  10. Knowl 10 — LeanWorkbook contains unprovable or incorrectly formalized targets

    limitation

    The authors manually assessed 20 randomly selected LeanWorkbook statements that remained unproved during STP training. Sixteen of the 20 formalizations accurately represented their associated natural-language statements, but only 7 formal statements were judged correct and provable; the other 13 were unprovable, for example because assumptions were missing from the source problem. This sample indicates that the attainable pass rate on LeanWorkbook can be substantially below 100%, so failure to prove a dataset statement does not necessarily indicate prover failure.

Coverage note — The paper’s individual generated-conjecture examples and lower-level verifier, hardware, and data-preprocessing details are omitted because they illustrate or implement the main contributions rather than add comparably significant standalone findings.

References

  1. 1.AlphaProof. Ai achieves silver-medal standard solving international mathematical olympiad problems. 2024. URL https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/.
  2. 2.Andrychowicz, M., Wolski, F., Ray, A., Schneider, J., Fong, R., Welinder, P., McGrew, B., Tobin, J., Pieter Abbeel, O., and Zaremba, W. Hindsight experience replay. Advances in neural information processing systems, 30, 2017.
  3. 3.Anthony, T., Tian, Z., and Barber, D. Thinking fast and slow with deep learning and tree search. Advances in neural information processing systems, 30, 2017.
  4. 4.Aygün, E., Anand, A., Orseau, L., Glorot, X., Mcaleer, S. M., Firoiu, V., Zhang, L. M., Precup, D., and Mourad, S. Proving theorems using incremental learning and hindsight experience replay. In International Conference on Machine Learning, pp. 1198–1210. PMLR, 2022.
  5. 5.Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023a.
  6. 6.Azerbayev, Z., Schoelkopf, H., Paster, K., Dos Santos, M., McAleer, S., Jiang, A., Deng, J., Biderman, S., and Welleck, S. Llemma: An open language model for mathematics. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023b.
  7. 7.Bibel, W. Automated theorem proving. Springer Science & Business Media, 2013.
  8. 8.Colas, C., Karch, T., Sigaud, O., and Oudeyer, P.-Y. Autotelic agents with intrinsically motivated goal-conditioned reinforcement learning: a short survey. Journal of Artificial Intelligence Research, 74:1159–1199, 2022.
  9. 9.Dong, K., Mahankali, A., and Ma, T. Formal theorem proving by rewarding llms to decompose proofs hierarchically. arXiv preprint arXiv:2411.01829, 2024.
  10. 10.Einarsdóttir, S. H., Alhessi, Y., First, E., and Johansson, M. On lemma conjecturing using neural, symbolic and neuro-symbolic approaches. 2024.
  11. 11.Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q., Ma, S., Wang, P., Bi, X., et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  12. 12.Haluptzok, P., Bowers, M., and Kalai, A. T. Language models can teach themselves to program better. arXiv preprint arXiv:2207.14502, 2022.
  13. 13.Jaech, A., Kalai, A., Lerer, A., Richardson, A., El-Kishky, A., Low, A., Helyar, A., Madry, A., Beutel, A., Carney, A., et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024.
  14. 14.Jiang, A. Q., Li, W., Han, J. M., and Wu, Y. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378–392, 2021.
  15. 15.Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłos, P., Wu, Y., and Jamnik, M. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:8360–8373, 2022a.
  16. 16.Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022b.
  17. 17.Jiang, A. Q., Li, W., and Jamnik, M. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023.
  18. 18.Johansson, M. and Smallbone, N. Exploring mathematical conjecturing with large language models. 2023.
  19. 19.Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
  20. 20.Kingma, D. P. and Ba, J. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
  21. 21.Kwon, W., Li, Z., Zhuang, S., Sheng, Y., Zheng, L., Yu, C. H., Gonzalez, J., Zhang, H., and Stoica, I. Efficient memory management for large language model serving with pagedattention. In Proceedings of the 29th Symposium on Operating Systems Principles, pp. 611–626, 2023.
  22. 22.Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349, 2022.
  23. 23.Li, R., Allal, L. B., Zi, Y., Muennighoff, N., Kocetkov, D., Mou, C., Marone, M., Akiki, C., Li, J., Chim, J., et al. Starcoder: may the source be with you! arXiv preprint arXiv:2305.06161, 2023.
  24. 24.Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024.
  25. 25.Loveland, D. W. Automated theorem proving: A logical basis. Elsevier, 2016.
  26. 26.Lu, J., Wan, Y., Liu, Z., Huang, Y., Xiong, J., Liu, C., Shen, J., Jin, H., Zhang, J., Wang, H., et al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.01940, 2024.
  27. 27.mathlib Community, T. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145/3372885.3373824.
  28. 28.Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pp. 625–635. Springer, 2021.
  29. 29.Nijkamp, E., Pang, B., Hayashi, H., Tu, L., Wang, H., Zhou, Y., Savarese, S., and Xiong, C. Codegen: An open large language model for code with multi-turn program synthesis. arXiv preprint arXiv:2203.13474, 2022.
  30. 30.Nipkow, T., Wenzel, M., and Paulson, L. C. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002.
  31. 31.Parker-Holder, J., Jiang, M., Dennis, M., Samvelyan, M., Foerster, J., Grefenstette, E., and Rocktäschel, T. Evolving curricula with regret-based environment design. In International Conference on Machine Learning, pp. 17473–17498. PMLR, 2022.
  32. 32.Plaat, A., Wong, A., Verberne, S., Broekens, J., van Stein, N., and Back, T. Reasoning with large language models, a survey. arXiv preprint arXiv:2407.11511, 2024.
  33. 33.Poesia, G., Broman, D., Haber, N., and Goodman, N. D. Learning formal mathematics from intrinsic motivation. arXiv preprint arXiv:2407.00695, 2024.
  34. 34.Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  35. 35.Portelas, R., Colas, C., Weng, L., Hofmann, K., and Oudeyer, P.-Y. Automatic curriculum learning for deep rl: A short survey. arXiv preprint arXiv:2003.04664, 2020.
  36. 36.Pourcel, G., Carta, T., Kovac, G., and Oudeyer, P.-Y. Autotelic llm-based exploration for goal-conditioned rl. In Intrinsically Motivated Open-ended Learning Workshop at NeurIPS 2024, 2024a.
  37. 37.Pourcel, J., Colas, C., Molinaro, G., Oudeyer, P.-Y., and Teodorescu, L. Aces: generating diverse programming puzzles with autotelic language models and semantic descriptors. Neurips, 2024b.
  38. 38.Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Zhang, M., Li, Y., Wu, Y., and Guo, D. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  39. 39.Shinn, N., Cassano, F., Labash, B., Gopinath, A., Narasimhan, K., and Yao, S. Reflexion: Language agents with verbal reinforcement learning.(2023). arXiv preprint cs.AI/2303.11366, 2023.
  40. 40.Silver, D., Huang, A., Maddison, C. J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T., Leach, M., Kavukcuoglu, K., Graepel, T., and Hassabis, D. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7676):484–503, 2016.
  41. 41.Teodorescu, L., Colas, C., Bowers, M., Carta, T., and Oudeyer, P.-Y. Codeplay: Autotelic learning through collaborative self-play in programming environments. In IMOL 2023-Intrinsically Motivated Open-ended Learning workshop at NeurIPS 2023, 2023.
  42. 42.Touvron, H., Martin, L., Stone, K., Albert, P., Almahairi, A., Babaei, Y., Bashlykov, N., Batra, S., Bhargava, P., Bhosale, S., et al. Llama 2: Open foundation and fine-tuned chat models. arXiv preprint arXiv:2307.09288, 2023.
  43. 43.Trinh, T. and Luong, T. Alphageometry: An olympiad-level ai system for geometry. Google DeepMind, 17, 2024.
  44. 44.Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jennings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. arXiv preprint arXiv:2407.11214, 2024.
  45. 45.Urban, J. and Jakubův, J. First neural conjecturing datasets and experiments. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pp. 315–323. Springer, 2020.
  46. 46.Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023.
  47. 47.Wang, M. and Deng, J. Learning to prove theorems by learning to generate theorems. In Proceedings of the 34th International Conference on Neural Information Processing Systems, pp. 18146–18157, 2020.
  48. 48.Wang, R., Zhang, J., Jia, Y., Pan, R., Diao, S., Pi, R., and Zhang, T. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024.
  49. 49.Wu, M., Norrish, M., Walder, C., and Dezfouli, A. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330–9342, 2021.
  50. 50.Wu, Y., Jiang, A. Q., Ba, J., and Grosse, R. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arXiv:2007.02924, 2020.
  51. 51.Wu, Z., Huang, S., Zhou, Z., Ying, H., Wang, J., Lin, D., and Chen, K. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024.
  52. 52.Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  53. 53.Xin, H., Ren, Z., Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., Du, Q., et al. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024b.
  54. 54.Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024a.
  55. 55.Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024b.
  56. 56.Yao, S., Zhao, J., Yu, D., Du, N., Shafran, I., Narasimhan, K., and Cao, Y. React: Synergizing reasoning and acting in language models. arXiv preprint arXiv:2210.03629, 2022.
  57. 57.Ye, Z., Agarwal, R., Liu, T., Joshi, R., Velury, S., Le, Q. V., Tan, Q., and Liu, Y. Evolving alignment via asymmetric self-play. arXiv preprint arXiv:2411.00062, 2024.
  58. 58.Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024.
  59. 59.Zhang, J., Lehman, J., Stanley, K., and Clune, J. Omni: Open-endedness via models of human notions of interestingness. arXiv preprint arXiv:2306.01711, 2023.
  60. 60.Zheng, C., Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806, 2023.
  61. 61.Zheng, K., Han, J. M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2021.

Citation

MLA
Dong, K., and T. Ma. “STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving”. arXiv, 2025, https://doi.org/10.48550/arxiv.2502.00212.
APA
Dong, K., & Ma, T. (2025). STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. arXiv. https://doi.org/10.48550/arxiv.2502.00212
Chicago
Dong, K., and T. Ma. 2025. “STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving”. Preprint, ArXiv. https://doi.org/10.48550/arxiv.2502.00212.
Harvard
Dong, K. and Ma, T. (2025) “STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving”. arXiv. Available at: https://doi.org/10.48550/arxiv.2502.00212.
Vancouver
1. Dong K, Ma T (2025) STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. https://doi.org/10.48550/arxiv.2502.00212

BibTeX

@misc{https://doi.org/10.48550/arxiv.2502.00212,
  doi = {10.48550/ARXIV.2502.00212},
  url = {https://arxiv.org/abs/2502.00212},
  author = {Dong, Kefan and Ma, Tengyu},
  keywords = {Machine Learning (cs.LG), Artificial Intelligence (cs.AI), Logic in Computer Science (cs.LO), FOS: Computer and information sciences, FOS: Computer and information sciences},
  title = {STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
  publisher = {arXiv},
  year = {2025},
  copyright = {Creative Commons Attribution Non Commercial No Derivatives 4.0 International}
}
Metadata:DOI registry

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF
License: https://creativecommons.org/licenses/by/4.0/