形式数学推理：AI 的新前沿
人工智能
2024-12-23 v1 机器学习
计算机科学中的逻辑
摘要
AI for Mathematics (AI4Math) 不仅在智力上引人入胜，也是 AI 在科学、工程及更广泛领域驱动发现的关键。对 AI4Math 的广泛努力已镜像 NLP 的技术，特别是通过在精心策划的文本形式的数学数据集上进行大规模语言模型训练。作为一种补充且较少探索的途径，形式数学推理建立在诸如证明助理等形式系统之上，这些系统可以验证推理的正确性并提供自动反馈。在本位论文中，我们倡导形式数学推理，并论证它对于将 AI4Math 提升到下一水平至关重要。近年来，我们已看到在使用 AI 执行形式推理方面取得了稳步的进展，包括诸如定理证明和自动化形式化等核心任务，以及诸如可验证代码和硬件设计生成等新兴应用。然而，要让 AI 真正掌握数学并实现更广泛的影响，仍面临着显著的挑战。我们总结了现有的进展，讨论了开放性挑战，并设想了衡量未来成功的关键里程碑。在形式数学推理的这个分水岭上，我们呼吁研究社区团结起来，推动该领域实现变革性的进步。
引用
@article{arxiv.2412.16075,
title = {Formal Mathematical Reasoning: A New Frontier in AI},
author = {Kaiyu Yang and Gabriel Poesia and Jingxuan He and Wenda Li and Kristin Lauter and Swarat Chaudhuri and Dawn Song},
journal= {arXiv preprint arXiv:2412.16075},
year = {2024}
}