Position: Formal Mathematical Reasoning—A New Frontier in AI
Meta FAIR · Stanford University · UC Berkeley · University of Edinburgh · Facebook · The University of Texas at Austin · University of California Berkeley
PDF 由论文原始站点提供，PaperCompass 不保存论文文件。
摘要
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.