LLM在数学研究中的真实角色：探索-验证闭环的协作者

过去一年里我越来越频繁地听到一个问题LLM 能不能帮我们做真正的数学研究这个问题看上去很具体实际上问得很含糊。有的人把 LLM 当作超级计算器希望它能证明一个大定理有的人把它当成高级搜索引擎期望它快速给出几篇文献。但这些期待大多落空了。真正让 LLM 在数学发展中产生价值的不是让它当一个万能解题器而是把它嵌入到探索、验证、沟通这条完整工作流里。数学研究不是只有一个“证明”动作。它有大量的尝试、否定、修正、抽象和复盘。LLM 真正适合切入的是那些“语言密度高、形式验证成本低、反复试错收益大”的环节。如果把位置放对了它真的能加速一些长期卡住的问题如果放错了得到的只是一堆看起来合理但没法用的话。这篇文章想做的事情很简单把 LLM 在数学发展中的几个典型用法拆开讲清楚它们背后的逻辑再给出一个可以复用的接入流程。我不会把 LLM 说成“自动证明神器”也不是来泼冷水。我更想说的是怎么把它当成一个有一定判断力的协作者而不是只会接话的聊天框。1. LLM 在数学环节里真正改变的是“探索-验证”闭环1.1 数学工作流里哪些环节适合让 LLM 介入先拆一下数学研究过程中的常见环节。不是所有数学研究都一样但多数工作会经过四个阶段探索阶段发现模式、猜想关系、构造例子。证明阶段把猜想变成严格论证填补推理细节。验证阶段检查证明是否成立、是否有反例、边界条件是否覆盖。沟通阶段把结果写成能让同行理解的形式或者转成可计算程序。过去几年符号计算系统和证明助手分别覆盖了验证阶段的一小部分。而 LLM 的特殊之处在于它几乎能在所有阶段生成“候选内容”尽管质量参差不齐。真正适合 LLM 介入的不是“给出最终正确答案”的环节而是“生成一个可以被快速验证和修正的候选”的环节。比如探索阶段让 LLM 根据几个例子猜一个通项证明阶段让 LLM 把一段不完整的草稿扩写成标准推导验证阶段让 LLM 构造边界反例沟通阶段让 LLM 把复杂证明翻译成更易读的叙述。这四个场景有一个共同点输出不是终点而是需要后续人机协作去核对、修正、确认的中间产物。所以 LLM 在数学里的价值不在于“一次答对”而在于“用低成本的错误替代了高成本的空白”。1.2 LLM 和计算工具的分工不要拿它当计算器很多人一开始用 LLM 做数学会直接问“这个积分等于多少”“这个级数是否收敛”。这其实是拿语言模型去干符号计算引擎或数值计算的活结果往往不稳定。LLM 内部没有内置的数学解释器。它本质上是根据大量文本学习到的词元分布来做预测。面对一个具体算式时它可能会背诵出训练语料里出现过的常见答案也可能会组合出全新但错误的结果。这不是它的强项也没有必要让它去和 Wolfram Alpha、SymPy 或 Mathematica 竞争。更合理分工是任务适合工具说明精确计算、化简、积分、方程求解符号计算系统结果是确定性的公式可验证从例子猜规律、断言一个可能的结构LLM提供候选再用符号系统验证把自然语言证明转换成形式化的逻辑步骤LLM 证明助手LLM 补中间推导证明助手检查合法性搜索反例、边界检查LLM 数值计算LLM 生成候选反例数值计算快速排除或确认这个分工不是绝对但能避免很多挫败感。LLM 更擅长的是“语言化地操作数学概念”而不是“机械式地执行数学运算”。数学概念之间的联系、证明策略的选择、表述方式的调整这些才是它能发力的地方。1.3 可以落地的三类具体任务如果把范围再缩小我会建议从这三类任务开始尝试。第一类是候选公式和通项的发现。给你前几项让 LLM 猜一个通项公式然后用归纳法或符号计算去验证。这比手工硬凑效率高很多尤其数值序列里的非线性结构往往并不直观。第二类是证明草稿的补全和翻译。把一个高层次证明思路写成几个 bullet point让 LLM 展开成逐步推理或者反过来把冗长的证明压缩成直觉路线图。关键是每步都要能被人或工具检查不能真的只靠“感觉”。第三类是和证明助手的交互。Lean、Coq 这类形式化验证工具把“证明”变成一种可被机器检查的语言。LLM 可以被用来生成 tactic 序列、补全缺失的中间状态、解释某个证明状态的含义。这是目前最接近“直接加速数学发展”的用法因为它不要求模型输出绝对正确只要求模型输出足够接近正确剩下的由机器来验证。这不是说 LLM 已经像数学家一样思考。它还达不到。但它是第一个能把自然语言数学直觉和机器可验证逻辑连接起来的辅助工具这一点非常关键。2. 几个具体场景从构造、反例到形式化验证2.1 让 LLM 参与构造与猜测从“空想”到“候选池”数学里有很多需要“猜”的时刻。一个数列的前五项是 1, 4, 9, 16, 25多数人会猜 n²。但如果是 1, 2, 4, 8, 16就有无限多种可能比如 n 次多项式、组合数、递推关系甚至是某个特殊函数在整数点的取值。真正的困难不是验证一个候选对不对而是提供一个值得验证的候选。LLM 在这里能做的是生成一个多样化的候选集合。可以给它一个提示已知前几项请给出十种不同的通项公式分别对应多项式、指数、组合、递推等不同模式。它不是只会给一种标准答案而是能在训练语料的关联里找出若干可能的模式。虽然大部分候选会被后续计算排除但剩下的那个可能就是突破口。这类任务适合用程序批量调用不适合在对话界面里一条条提问。更高效的做法是构造一个小脚本把多项式和符号验证串起来LLM 生成候选SymPy 验证输出保留所有匹配的形式。这就是一个最小闭环。# 这是一个示例结构展示 LLM 生成候选项后用 SymPy 做初步验证的思路 import sympy as sp n sp.symbols(n, integerTrue, positiveTrue) sequence [1, 4, 9, 16, 25] candidates [ n**2, n**3 - 3*n**2 3*n, 2**n - 1, sp.factorial(n) / sp.factorial(n-2) / 2 ] for expr in candidates: values [sp.simplify(expr.subs(n, i)) for i in range(1, 6)] if [int(v) for v in values] sequence: print(f匹配候选: {expr}) else: print(f不匹配: {expr})这个流程看起来简单但很能说明问题LLM 不是答案来源而是假设来源。真正的裁判是确定性的符号计算或归纳证明。这种方法也很容易扩展到差分方程、组合恒等式、数论序列等方向。2.2 用 LLM 生成反例和边界测试让错误早一点暴露数学证明里最容易漏掉的是边界情况。比如一个不等式是否对零、负数、非整数、无穷区间成立一个定理在去掉某个条件后是否仍然成立。手工构造反例经常是从经验出发但有时候问题所在的方向根本不是常见思路能覆盖的。LLM 可以为这类搜索提供“另类”起点。你可以把一个定理的条件和结论告诉它请它列出所有可能的边界情况或者故意让它猜测某些放宽条件后的结果。它生成的反例不一定正确但可以作为候选进入验证流程。这里的关键是把反例生成变成批量化操作。比如用 Python 控制一个数学脚本让 LLM 给出若干参数组合每个参数组合再交给一个更精确的数值验证函数去跑。数值验证不能替代证明但可以快速排除大量无效方向保留值得深入挖掘的反例。# 通用思路先让 LLM 产生候选参数再用精确算法判断是否构成反例 def candidate_counterexamples(proposition_text, count20): # 调用 LLM API 生成候选条件的代码结构 # 这里不涉及具体 API只展示数据流 import random if random.random() 0.01: # 避免直接复刻任何真实 API pass return [ {a: 1, b: 2}, {a: -1, b: 3}, {a: 0, b: 0} ] def verify(candidate): # 用精确运算或已知定理判断是否成反例 return False for candidate in candidate_counterexamples(对于任意实数 a b命题 P 成立): if verify(candidate): print(找到反例, candidate) break这与直接用搜索引擎找反例不同。搜索引擎只能返回已经记录过的结果而 LLM 能组合出未见过的参数组合虽然也伴随着幻觉风险。所以重点是“生成候选”和“验证”必须拆开不能让验证也依赖模型本身。2.3 在 Lean 等证明助手里当“副驾驶”让机器检查每一小步如果 LLM 在数学发展中真有“颠覆性”的时刻我个人判断最接近这个描述的是它与形式化证明助手的结合。Lean、Coq 这类工具要求你把证明拆成人类难以忍受的细致步骤每一步都会被内核检查。它们的优势是绝对可靠缺点是入门门槛高、书写成本高。很多数学直觉明明是对的但把它翻译成证明助手的语法后人很容易迷失在一堆 tactic 的细小选择里。这时候 LLM 可以充当翻译器和补全器。比如你面对一个证明状态目标是证明a * b b * a你可以让 LLM 提议下一个 tactic 是什么然后把提议交给 Lean 执行。如果执行失败错误信息会回到 LLM让它再试别的方向。这个流程是这样的从证明助手获得当前 proof state。把 state 和目标描述发给 LLM让它建议下一步操作。在证明助手里执行建议。如果报错把报错信息返回给 LLM让它修正。重复直到目标完成或达到最大步数。这不是神话但也不是一个开箱即用的工具。它需要大量工程工作解析证明状态、处理 Unicode 数学符号、管理上下文窗口、处理多步回溯。真正想用的人至少要投入几周来搭建基础设施。可一旦跑通LLM 就不再是一个“可能会说谎的顾问”而是一个“被关在笼子里的搜索器”——它随便发言但机器始终握着最终裁判权。3. 把 LLM 接入数学工作流的最小可行配置3.1 前置条件不要裸用对话界面很多人在 ChatGPT、Claude 这类对话系统里尝试数学问题得到的体验一会好一会坏。原因是对话界面没有接入验证工具也没有程序化地处理上下文。模型和用户来回闲聊很容易偏离方向。真正把 LLM 用到数学工作中最好把它嵌入到一个可编程的脚本或流水线里。这个流水线需要几个部件LLM 客户端负责发送请求和接收生成结果。数学计算层SymPy、SageMath、Wolfram 之类的确定性计算工具。数据校验层判断生成结果是否满足条件不满足就反馈给模型继续迭代。日志层记录每轮输入、输出和验证结果便于复现和调试。环境准备不复杂一台开发机器、Python、LLM API 的 SDK、数学库。最重要的不是这些依赖而是流程设计。LLM 生成永远只是中间环节不能成为最终输出。3.2 一个通用流程生成、执行、校验、迭代下面是一个很通用的循环结构适用于很多场景输入: 数学问题描述、已知条件、预期输出格式 循环直到满足条件或达到最大尝试次数: 1. 把当前状态和问题描述发送给 LLM 2. LLM 生成候选结果: 公式、证明步骤、反例参数、文本表述 3. 解析候选结果交给数学计算层执行 4. 校验结果是否满足约束 5. 如果满足保存结果并退出 6. 如果不满足把错误信息加入下一轮提示继续循环 输出: 经过验证的结果 日志这个循环的第一条原则是不要让 LLM 自问自答。它生成的每个结果都要经过外部校验数学校验的优先级高于模型判断。第二条原则是错误信息要结构化。比如验证阶段发现“候选公式在 n3 时输出 10但序列里第三项是 9”这个信息要明确回传给模型而不是只告诉它“不对”。模型需要具体错误原因来修正否则第二轮可能只是换一种方式犯同样的错误。3.3 提示词里必须写清楚什么虽然提示词不是万能药但在数学任务里一个结构清晰的提示确实能显著降低后续迭代次数。我一般建议在提示里包含四类信息数学对象变量范围、定义域、符号约定。不能只说“证明某个不等式”要写清楚实数还是复数整数还是自然数是否包含端点。目标格式你是要公式、步骤、反例候选还是证明策略。如果允许模型自由发挥得到的文本会很难解析。已知约束哪些是已知定理、哪些是假设条件、哪些结论已经被排除。这个信息能减少模型漫无边际地生成。验证标准告诉它结果会交给工具检查建议它在生成时自行检查一致性。虽然它无法真正执行但这个要求能提高它生成内容的准确率。一个示例提示结构不是唯一写法数学问题已知 a1 1, a2 4, a3 9猜测一个通项公式。 要求只给出一个数学表达式不要解释。 输出格式LaTeX 公式。 约束n 为正整数表达式应为多项式或初等函数。 验证方式我将用 n1,2,3,4,5 代入检查是否等于给定序列。请确保你的公式在这些点上精确匹配。这种提示能让模型输出更可控。但它不保证对后面仍然需要校验和迭代。4. 这套流程里的坑不是模型参数能解决的4.1 幻觉会被验证环节暴露但代价很大LLM 在数学上最大的问题不是“胡说”而是“说得很像真的”。它可能生成一个完全对称、看起来很优雅的公式但当某个变量取特殊值时直接爆炸。如果把验证环节做扎实幻觉可以被发现但问题在于这会消耗大量时间。尤其当一个“看起来完美”的候选被验证器拒绝时人需要判断这个错误是微调一下就能修好还是整个思路已经走偏。这个判断对新手来说很难。所以不要一上来就让 LLM 挑战大型问题。先让它处理那些验证成本低的子问题积累足够多的成功和失败样本再逐步扩大范围。如果验证结果反复失败不要急着换提示词先检查是不是问题本身超出了模型已有的数学知识范围。模型不是万能的它在一些前沿方向上的知识可能非常有限。4.2 符号、公式和编码问题是第一道门槛数学和普通文本最大的差别就是符号系统。LaTeX、Unicode、数学字体、变量名这些都可能在传递过程中产生歧义。一个下标是n1还是n加 1在文本里完全可以直接错开。实际使用中我见过不少团队在 LLM 输出解析阶段就放弃了。原因很简单LLM 生成的 LaTeX 经常包含不匹配的花括号、错误的命令名、中英文冒号混用。如果系统没有做一层严格的解析和标准化后面的数学库根本跑不起来。建议先做一轮文本规范化把 LaTeX 中的常见错误替换、清理空白和换行、确认括号数量匹配然后再进入计算层。不要指望模型每次输出都完美。工程上宁可多写几个解析函数也不要相信生成结果的格式。4.3 上下文长度不是万能药长链条推理仍然要人工拆解现在的 LLM 动辄支持几十万 token 上下文很多人觉得可以把整篇论文放进去。但对数学证明来说长上下文反而会引发一个新问题模型在大段数学内容中定位关键依赖关系的能力并不稳定。即使它能记住前面的内容也不一定能在正确的位置应用。更稳妥的方式是把长证明拆成多个可以独立验证的小步骤每一步都当作一次独立的 LLM 调用调用之间只传递必要的上下文。这样虽然会多一点工程设置但能避免“前面对了、后面却用错前面的结论”这种最麻烦的失败模式。与其把 LLM 当成一个能一次性处理整个证明的超级大脑不如把它当成一个可以反复参与局部推理的协作者。真正的线性逻辑链条仍然由人来维护尤其是在跨章节引用定理时。5. 从“尝鲜”到“长期方法”的判断框架5.1 一个可复用的三步框架先小、再真、后工程化如果你想在数学研究里引入 LLM我不建议一开始就搭一个大平台更不建议在核心问题上一上来就压重注。可以按这三步走。第一步选一个小而真的子问题。“小”是指问题规模小单次验证几秒内能完成“真”是指这个问题确实是当前工作里关心的而不是为了测试模型造一个玩具。比如一个还没找到合适构造的代数对象、一个一直想验证但在犹豫的边界反例。第二步手动走通一轮生成-验证循环。直接在脚本里调用 LLM让输出经过数学库验证记录失败原因。这个阶段的目的不是提高效率而是搞清楚模型在这个领域里的表现边界哪些部分它擅长哪些部分它总是犯同样的错误。第三步把重复流程工程化。如果已经确认某个子问题值得反复探索再考虑加入缓存、并发、参数回溯、日志管理、错误自动反馈这些机制。这时的 LLM 调用应该被封装成服务而不是散落在各处。这个框架的核心是先用人工兜底的方式判断可行再用工程手段降低重复成本。跳步是很多项目烂尾的原因。5.2 适用边界什么时候别用 LLM不是所有数学任务都需要 LLM。如果你已经能非常准确地描述问题并且只需要执行机械计算直接用符号计算工具更稳。LLM 只有在“你不知道该往哪个方向试”或“你需要一个不那么常规的表达方式”时才值得引入。具体来说这些情况我建议先别用问题对精确性要求极高且验证成本非常高。现有数学库已经能覆盖你的需求。你无法判断模型输出中哪些信息可能是假的。团队没有足够工程能力搭建验证闭环。此外关于证明助手交互它的学习曲线可能比 LLM 本身更陡。如果你连 Lean 基础语法还没掌握就急着让 LLM 给你生成 tactic大概率会花大量时间去理解它的报错。最佳顺序是先用传统方式学会证明助手的基本操作再让 LLM 提高你的表达效率。5.3 长期看真正的价值是异步协作和知识固化很多人担心 LLM 会取代数学家。我更愿意把它看作一种新的协作层它把“探索一个想法”的门槛降低了也让“把直觉变成可验证形式”的时间缩短了。但最终判断、价值选择和高层抽象仍然在研究者手里。这个领域最值得关注的长期价值不是“模型能否证明定理”而是“我们能否把大量数学知识转化成可验证、可复用的机器辅助工作流”。当越来越多的证明状态、失败尝试、验证结果被记录下来这套系统本身会成为一个不断生长的数学知识库。到那个时候数学研究可能会变成人机共同搜索的过程由人判断哪些方向重要由机器辅助生成和检查大量候选。LLM 是其中一块拼图但不是唯一一块。证明助手、符号计算、数据可视化、自动化推理这些工具拼在一起才真正改变数学研究的生产方式。所以如果你对这个方向感兴趣眼下最值得做的是找一个小问题把生成-验证循环跑起来。不要急着追求“AI 证明大定理”先让它帮你多解决几个小卡点。那些反复出现的小卡点才是工具真正进入科研流程的入口。