推动AI用形式化系统做数学推理，提升可信科学发现能力
Formal Mathematical Reasoning: A New Frontier in AI
- 用证明助手构建可验证的数学推理框架
- 实现定理证明与代码硬件自动生成的可验证输出
- 适合追求高可信AI的科研与工程团队
人工智能在数学领域的应用不仅具有深远的智力价值，对科学、工程等领域的智能发现也至关重要。现有AI4Math研究多借鉴自然语言处理技术，通过在文本形式的数学数据集上训练大语言模型。作为互补但较少探索的方向，形式化数学推理基于如证明助手等形式系统，可验证推理正确性并提供自动反馈。本文主张发展形式化数学推理，认为这是推进AI4Math迈向新高度的关键。近年来，AI在定理证明、自动形式化等核心任务，以及可验证代码与硬件设计生成等新兴应用方面取得稳步进展。然而，要使AI真正掌握数学并产生广泛影响，仍面临重大挑战。本文总结现有进展，讨论开放问题，并提出衡量未来成功的里程碑。在此关键节点，呼吁研究界协同推进该领域变革性发展。
原文摘要 · Abstract (English)
AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. 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. In this position paper, we advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level. In recent years, we have seen steady progress in using AI to perform formal reasoning, including core tasks such as theorem proving and autoformalization, as well as emerging applications such as verifiable generation of code and hardware designs. However, significant challenges remain to be solved for AI to truly master mathematics and achieve broader impact. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success. At this inflection point for formal mathematical reasoning, we call on the research community to come together to drive transformative advancements in this field.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。