LLM驱动形式数学：从解题跨越至前沿研究

背景

近年来，人工智能与数学的交汇领域（AI for Mathematics, AI4Math）取得了显著进展，尤其是大型语言模型（Large Language Model, LLM）驱动的定理证明器。这些系统通过交互式定理证明（Interactive Theorem Proving, ITP）语言，能够为定义清晰、封闭的数学问题自动生成形式化证明，在竞赛题、标准定理等场景中表现卓越。然而，当前系统在处理前沿研究数学时暴露出根本性局限——这类问题（如发现新定理、解决开放猜想）通常是开放式的、定义模糊的，并且涉及多层次抽象。本文是一篇立场论文（position paper），旨在系统梳理领域现状，并明确指出：AI4Math 的下一阶段突破需要从“预定义求解器”决然转向“研究智能体”，后者能够以前沿数学挑战为目标，进行严谨的形式化数学推理。

核心内容

本文对 AI4Math 领域进行了系统性综述，覆盖三大核心方向：数据集、自动形式化（auto-formalization）以及证明合成（proof synthesis）。在此基础上，文章重点剖析了现有系统在充当数学研究智能体时的关键缺陷，并从五个维度展开讨论：

• 数据集问题：当前数据集多基于已知定理和人工整理的形式化证明，缺乏对未解决猜想、开放性问题以及数学探索过程的覆盖；数据分布与真实研究场景差距大。
• 关系结构：现有形式化证明通常以线性或树形结构组织，难以捕捉数学概念之间复杂的关联、抽象层次以及不同证明路径的等价关系。
• 数学探索：现有系统依赖明确的目标（如“证明命题 P”），缺乏自主提出新问题、构造反例、尝试不同策略的探索能力；而数学研究常涉及试错与直觉驱动。
• 工具生态：虽然已有 Lean、Coq、Isabelle 等成熟的 ITP 工具，但 LLM 与这些工具的接口、自动补全、错误反馈循环仍不够顺畅，缺乏适用于研究场景的集成开发环境。
• 人机协作：当前系统多采用“全自动求解”范式，忽略了人类数学家作为决策者和指导者的角色；高效的研究智能体应能支持交互式建议、假设检验以及结果讨论。

文章最后概述了面向未来的战略路线图，强调需要构建包含自动形式化、探索式证明搜索、自适应学习以及人机协同的工作流，从而推动 AI4Math 进入研究前沿。

关键要点

• 基本论断：当前 LLM 驱动的定理证明器虽然擅长解决封闭式、形式化定义的数学问题，但在开放、未定义的前沿研究问题上存在根本局限。
• 核心转变：AI4Math 系统必须从“求解器”（solver）升级为“研究智能体”（research agent），即具备自主探索、假设生成、容错推理能力的形式化推理系统。
• 覆盖领域：综述涵盖数据集、自动形式化（将非形式化数学表述转化为形式化代码）与证明合成三大支柱。
• 关键局限：现有系统的缺陷体现在数据集过时且覆盖窄、关系结构单一、缺乏数学探索能力、工具生态不完善、人机协作模式不成熟。
• 未来路线图：文章呼吁构建整合性平台，支持自动形式化、探索式搜索、自适应学习以及深度人机协作，以实现 AI4Math 对前沿数学研究的实质性贡献。

意义与影响

本文的意义在于首次从“研究智能体”的高度系统反思 AI4Math 的发展方向。以往工作多聚焦于提升特定基准上的正确率，而本文指出：若想真正推动数学发现，系统必须具备处理不确定性与抽象性的能力。这一观点为领域指明了新的研究范式——从求解已知问题转向协助人类探索未知定理。此外，文章对五类局限的诊断具有实践指导价值，有助于研究者有针对性地改进模型设计、工具建设与数据收集策略。长远来看，若路线图得以实现，AI 系统不仅可成为验证工具，更可能成为数学家的合作者，加速定理发现与猜想验证的进程。论文还通过 arXiv 平台发布，引用信息及配套工具（如 Bibliographic Explorer、alphaXiv 等）为后续复现和拓展提供了基础。