Elamur Research
☰
home / papers / 2022 / Formal Mathematics Statement Curriculum Learning

Formal Mathematics Statement Curriculum Learning

Written for the Research library (claude-opus-5-5) from the paper text, in our own words: the license "arXiv — non-exclusive licence to distribute" does not allow redistributing the text itself. Original — arxiv.org/pdf/2202.01344v1

Summary

Neural theorem provers for formal mathematics lack the self-play mechanism that drives progress in two-player games. A prover faces fixed theorems rather than an adapting opponent, so it has no natural way to create easier intermediate tasks. The authors treat self-play mainly as a source of curriculum. Their replacement is a collection of auxiliary formal statements of varied difficulty, supplied without proofs. They pair this with expert iteration: proof search alternating with retraining on the proofs the model itself found.

The system is GPT-f applied to Lean through lean-gym, a new REPL interface. It is a 774M-parameter decoder-only Transformer, pre-trained on web and math text and fine-tuned on mathlib tactic data. Proof search is guided by a proofsize objective that estimates how many steps remain.

At equal compute, expert iteration clearly beats search alone. Using synthetic inequalities and hand-curated competition statements, the model gradually solves harder problems and reaches state-of-the-art on miniF2F. The broader implication is that formalizing statements, which is far cheaper than formalizing proofs, could fuel continued self-improvement of provers.

Key points

  • Benchmark and results: miniF2F has 244 validation and 244 test statements from math competitions. The fully expert-iterated model θ9 full reaches 47.3% on miniF2F-valid and 36.6% on miniF2F-test (pass@64). For comparison, PACT reported 23.9% and 24.6% pass@1 on these splits.
  • Problems solved: The models solved 26 AMC12, 6 AIME and 2 IMO-adapted problems. Several of these, including aime_1984_p1 and imo_1964_p2, were solved only by expert-iterated models.
  • Model and training: The model has 36 layers and 774M parameters. It was pre-trained on CommonCrawl (300B tokens) and then WebMath (72B tokens). Proof sizes are mapped to 11 buckets encoded as tokens 'A'–'K', which provide a value estimate without a separate value head.
  • mathlib and cost: Pass@64 exceeds 75% on both mathlib-valid and mathlib-test. A full expert iteration run cost about 2000 A100 days.
  • Limitations and code: The models seldom chain more than 2–3 non-trivial reasoning steps, and the cuts they generate tend to be shallow. lean-gym is released at github.com/openai/lean-gym.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Fields: Mathematics & statistics

Cited by

108 papers of our library cite it (of the 140673 whose bibliographies we read); 11 of them have a page here, 97 not yet.

Cite

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2202.01344 · arXiv 2202.01344

@misc{polu2022formal,
  title = {{Formal Mathematics Statement Curriculum Learning}},
  author = {Polu, Stanislas and Han, Jesse Michael and Zheng, Kunhao and Baksys, Mantas and Babuschkin, Igor and Sutskever, Ilya},
  year = {2022},
  doi = {10.48550/arxiv.2202.01344},
  eprint = {2202.01344},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2202.01344}
}

References

35 references, 7 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Lean theorem prover. github.io/about/. https://leanprover. Bansal, K., Loos, S., Rabe, M., Szegedy, C., and Wilcox, S. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454–463, 2019a. find
  2. Bansal, K., Loos, S. M., Rabe, M. N., and Szegedy, C. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501, 2019b. find
  3. Berner, C., Brockman, G., Chan, B., Cheung, V., D˛ebiak, P., Dennison, C., Farhi, D., Fischer, Q., Hashme, S., Hesse, C., et al. Dota 2 with large scale deep reinforcement learning. arXiv preprint arXiv:1912.06680, 2019. find
  4. Brown, T. B., Mann, B., Ryder, N., Subbiah, M., Kaplan, J., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. Language models are few-shot learners. arXiv preprint arXiv:2005.14165, 2020. find
  5. Browne, C. B., Powley, E., Whitehouse, D., Lucas, S. M., Cowling, P. I., Rohlfshagen, P., Tavener, S., Perez, D., Samothrakis, S., and Colton, S. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in games, 4(1):1–43, 2012. find
  6. Buzzard, K., Commelin, J., and Massot, P. Lean perfectoid spaces. https://leanprover-community. github.io/lean-perfectoid-spaces/, 2019. find
  7. Carbone, A. and Semmes, S. Making proofs without modus ponens: An introduction to the combinatorics and complexity of cut elimination. Bulletin of the American Mathematical Society, 34:131–159, 1996. find
  8. Czechowski, K., Odrzygóźdź, T., Zbysiński, M., Zawalski, M., Olejnik, K., Wu, Y., Kucinski, L., and Miłoś, P. Subgoal search for complex reasoning tasks. Advances in Neural Information Processing Systems, 34, 2021. de Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. The lean th… find
  9. Devlin, J., Chang, M.-W., Lee, K., and Toutanova, K. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805, 2018. find
  10. Firoiu, V., Aygun, E., Anand, A., Ahmed, Z., Glorot, X., Orseau, L., Zhang, L., Precup, D., and Mourad, S. Training a first-order theorem prover from synthetic data. arXiv preprint arXiv:2103.03798, 2021. — [arXiv:2103.03798](https://arxiv.org/abs/2103.03798) find
  11. Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Polu, S. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021. find
  12. Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021. find our card
  13. Huang, D., Dhariwal, P., Song, D., and Sutskever, I. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608, 2018. find
  14. Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F., and Urban, J. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235–2243, 2016. find
  15. Kaplan, J., McCandlish, S., Henighan, T., Brown, T. B., Chess, B., Child, R., Gray, S., Radford, A., Wu, J., and Amodei, D. Scaling laws for neural language models. arXiv preprint arXiv:2001.08361, 2020. find
  16. Karras, T., Laine, S., and Aila, T. A style-based generator architecture for generative adversarial networks. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 4401–4410, 2019. find
  17. Lehoczky, S. and Rusczyk, R. The Art of Problem Solving, Volume 1: the Basics, a. ISBN:978-0-9773045-6-1. Lehoczky, S. and Rusczyk, R. The Art of Problem Solving, Volume 2: and Beyond, b. ISBN:978-0-9773045-8-5. Li, W., Yu, L., Wu, Y., and Paulson, L. C. Modelling high-level mathematical reasoning i… find
  18. Loos, S., Irving, G., Szegedy, C., and Kaliszyk, C. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017. find
  19. Megill, N. D. and Wheeler, D. A. Metamath: A Computer Language for Pure Mathematics, 2019. URL http://us.metamath.org/downloads/metamath.pdf. ↗
  20. Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. find our card
  21. Rabe, M. N., Lee, D., Bansal, K., and Szegedy, C. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757, 2020. find
  22. Radford, A., Kim, J. W., Hallacy, C., Ramesh, A., Goh, G., Agarwal, S., Sastry, G., Askell, A., Mishkin, P., Clark, J., et al. Learning transferable visual models from natural language supervision. arXiv preprint arXiv:2103.00020, 2021. find our card
  23. Ramesh, A., Pavlov, M., Goh, G., Gray, S., Voss, C., Radford, A., Chen, M., and Sutskever, I. Zero-shot text-to-image generation. arXiv preprint arXiv:2102.12092, 2021. find our card
  24. Scholze, P. Liquid tensor experiment. https: //xenaproject.wordpress.com/2020/ 12/05/liquid-tensor-experiment/, 2020. find
  25. Selsam, D., Lamm, M., Bünz, B., Liang, P., de Moura, L., and Dill, D. L. Learning a sat solver from single-bit supervision. arXiv preprint arXiv:1802.03685, 2018. find
  26. Silver, D., Huang, A., Maddison, C. J., Guez, A., Sifre, L., Van Den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484–489, 2016. find
  27. Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., et al. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. arXiv preprint arXiv:1712.01815, 2017. find our card
  28. Tan, M. and Le, Q. Efficientnet: Rethinking model scaling for convolutional neural networks. In International Conference on Machine Learning, pp. 6105–6114. PMLR, 2019. find our card
  29. Urban, J. and Jakubův, J. First neural conjecturing datasets and experiments. arXiv preprint arXiv:2005.14664, 2020. find
  30. Vinyals, O., Babuschkin, I., Czarnecki, W. M., Mathieu, M., Dudzik, A., Chung, J., Choi, D. H., Powell, R., Ewalds, T., Georgiev, P., et al. Grandmaster level in starcraft ii using multi-agent reinforcement learning. Nature, 575 (7782):350–354, 2019. find
  31. Wang, M., Tang, Y., Wang, J., and Deng, J. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pp. 2786–2796, 2017. find
  32. Wu, Y., Schuster, M., Chen, Z., Le, Q. V., Norouzi, M., Macherey, W., Krikun, M., Cao, Y., Gao, Q., Macherey, K., et al. Google’s neural machine translation system: Bridging the gap between human and machine translation. arXiv preprint arXiv:1609.08144, 2016. find
  33. 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. find
  34. Yang, K. and Deng, J. Learning to prove theorems via interacting with proof assistants. arXiv preprint arXiv:1905.09381, 2019. find
  35. Zheng, K., Han, J. M., and Polu, S. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. find our card