从求解器到研究：大型语言模型驱动的前沿形式化数学
本文是一篇立场论文，系统回顾了人工智能数学（AI4Math）领域的最新进展，特别是大型语言模型（LLM）驱动的定理证明器在形式化证明生成方面取得的成功。然而，现有系统在应对前沿研究数学（如发现新定理或解决开放猜想）方面存在根本性限制。作者主张AI4Math系统应从预定义问题求解器转向能进行严格形式化数学推理的研究代理，并指出了现有系统在数据集、关系结构、数学探索、工具生态和人机协作等方面的核心局限性，为未来AI4Math的发展提出了战略路线图。
近年来，人工智能数学（AI4Math）领域取得了显著进展，尤其是大型语言模型（LLM）驱动的定理证明器在形式化证明生成方面表现突出。这些系统通过交互式定理证明（ITP）语言，能够为定义明确的数学问题自动生成形式化证明，标志着AI在数学推理领域的重大突破。然而，这些成就主要集中在已有明确求解路径的问题上，当面临前沿研究数学——如发现全新定理或解决悬而未决的猜想——时，现有系统往往力不从心。这类任务通常具有开放性、说明不充分、涉及多层次抽象的特点，远超当前系统的能力范围。
在一篇发表于arXiv的立场论文中，由Eric Jiang等19位作者组成的团队系统审视了AI4Math的现状，并提出了一个关键论点：AI4Math的下一次飞跃需要从预定义的问题求解器转向真正的研究代理，后者能够以前沿数学挑战为目标，进行严谨的形式化数学推理。论文首先回顾了该领域的三大核心组成部分：数据集、自动形式化和证明合成。数据集方面，现有基准如MiniF2F和ProofNet等主要针对已知竞赛或教科书问题，缺乏涵盖前沿研究的资源。自动形式化旨在将非形式化数学语句转化为机器可验证的ITP代码，但当前方法在复杂语境下可靠性不足。证明合成技术虽然借助LLM取得了进展，但生成的证明长度有限，难以处理需要深层探索的定理。
更关键的是，论文识别了现有系统在作为数学研究代理时的五大核心局限。第一，数据集问题：现有数据集规模小、领域窄，无法反映数学研究的多样性和深度。第二，关系结构缺失：数学知识以复杂的网络形式存在，但当前系统缺乏对定理间逻辑关系的结构化理解。第三，数学探索能力不足：研究过程包含大量试探性和创造性步骤，而现有系统仅能按预设路径搜索。第四，工具生态系统不完善：缺乏与现有数学软件（如计算机代数系统）及人类协作的科学工作流集成。第五，人机协作机制薄弱：AI应辅助而非替代数学家，但目前交互范式有限。
基于以上分析，作者勾勒了一个战略路线图，强调未来AI4Math系统需在数据构建（如创建大规模关系型数学知识库）、推理架构（如引入抽象与类比机制）、工具集成（如无缝对接证明助手与计算工具）以及交互设计（如自然语言与形式语言混合界面）等方面取得突破。这篇论文不仅是对现有技术的批评性总结，也为AI4Math领域指明了一个雄心勃勃的发展方向。