Position: Formal Mathematical Reasoning—A New Frontier in AI

Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, Dawn Song
Proceedings of the 42nd International Conference on Machine Learning, PMLR 267:82384-82398, 2025.

Abstract

AI for Mathematics (AI4Math) is intellectually intriguing and is crucial for AI-driven system design and verification. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large language models on carefully curated math datasets in text form. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. This position paper advocates formal mathematical reasoning as an indispensable component in future AI for math, formal verification, and verifiable generation. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.

Cite this Paper

BibTeX
@InProceedings{pmlr-v267-yang25az, title = {Position: Formal Mathematical Reasoning—A New Frontier in {AI}}, author = {Yang, Kaiyu and Poesia, Gabriel and He, Jingxuan and Li, Wenda and Lauter, Kristin E. and Chaudhuri, Swarat and Song, Dawn}, booktitle = {Proceedings of the 42nd International Conference on Machine Learning}, pages = {82384--82398}, year = {2025}, editor = {Singh, Aarti and Fazel, Maryam and Hsu, Daniel and Lacoste-Julien, Simon and Berkenkamp, Felix and Maharaj, Tegan and Wagstaff, Kiri and Zhu, Jerry}, volume = {267}, series = {Proceedings of Machine Learning Research}, month = {13--19 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v267/main/assets/yang25az/yang25az.pdf}, url = {https://proceedings.mlr.press/v267/yang25az.html}, abstract = {AI for Mathematics (AI4Math) is intellectually intriguing and is crucial for AI-driven system design and verification. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large language models on carefully curated math datasets in text form. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. This position paper advocates formal mathematical reasoning as an indispensable component in future AI for math, formal verification, and verifiable generation. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.} }
Endnote
%0 Conference Paper %T Position: Formal Mathematical Reasoning—A New Frontier in AI %A Kaiyu Yang %A Gabriel Poesia %A Jingxuan He %A Wenda Li %A Kristin E. Lauter %A Swarat Chaudhuri %A Dawn Song %B Proceedings of the 42nd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2025 %E Aarti Singh %E Maryam Fazel %E Daniel Hsu %E Simon Lacoste-Julien %E Felix Berkenkamp %E Tegan Maharaj %E Kiri Wagstaff %E Jerry Zhu %F pmlr-v267-yang25az %I PMLR %P 82384--82398 %U https://proceedings.mlr.press/v267/yang25az.html %V 267 %X AI for Mathematics (AI4Math) is intellectually intriguing and is crucial for AI-driven system design and verification. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large language models on carefully curated math datasets in text form. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. This position paper advocates formal mathematical reasoning as an indispensable component in future AI for math, formal verification, and verifiable generation. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
APA
Yang, K., Poesia, G., He, J., Li, W., Lauter, K.E., Chaudhuri, S. & Song, D.. (2025). Position: Formal Mathematical Reasoning—A New Frontier in AI. Proceedings of the 42nd International Conference on Machine Learning, in Proceedings of Machine Learning Research 267:82384-82398 Available from https://proceedings.mlr.press/v267/yang25az.html.

Related Material