大语言模型数学辅助工作流：从候选生成到符号验证的工程实践-平芜编程栈

在近两年的数学研究和教学工作中，AI 尤其是 LLM 的角色已经从“能聊数学问题”逐步变成“能参与数学发展流程的辅助工具”。所谓重要数学进展（major mathematical developments），并不只指证明某个公开猜想，也包括构造反例、整理证明思路、把自然语言证明形式化、为数值实验设计计算方案等工作。LLM 的用途集中在这些流程中“生成候选、解释思路、转换表达、辅助验证”的环节，而最后的正确性判断仍然需要人的推理和机器验证共同完成。这篇文章会带你搭建一套可以实际运行的 LLM 数学辅助工作流，包含环境配置、最小示例、提示词策略、验证方法和常见坑排查。

1. 先想清楚：LLM 在数学发展中到底承担什么角色

1.1 数学研究链条里哪些环节能交给 LLM

数学研究并不是只有“证明定理”这一个动作。一个完整的数学进展，通常包含提出问题、寻找候选结论、设计证明思路、完成符号推导、编写数值实验、形式化验证、审阅和返工等多个环节。不同环节的容错率完全不同，LLM 能承担的角色也完全不同。

下表是一个比较实用的分工视图：

数学工作环节	LLM 可参与程度	需要的配套工具	典型产出
文献调研与知识问答	高	检索接口、PDF 解析、向量库	概念地图、文献摘要、历史脉络
猜想生成	中	数值计算库、序列分析工具	候选公式、可验证命题
证明思路设计	中低	形式化证明助手	证明骨架、引理拆分
符号推导	低（LLM 负责表达，计算器负责计算）	SymPy、SageMath、Mathematica	可执行推导代码
形式化证明	中	Lean、Coq、Isabelle	可编译定理
审稿与找错	中	调试器、定理证明器	反例或错误定位

这个表想说明一个核心判断：LLM 不是用来替代数学家的判断力，而是用来降低“从想法到可验证表达”的转换成本。真正负责把关的，应该是符号计算器、定理证明器和人的审查。

1.2 LLM 的数学推理边界：它是启发式生成器，不是裁判

很多新手会犯同一个错误：把 LLM 当作数学权威，问完就抄结果。理解边界要从模型原理说起。LLM 本质上是在学习大量文本之后，根据上下文逐词预测最合适的下一个 token。它优化的是“看起来像正确数学文本”的概率，而不是“在逻辑上为真”的概率。

因此 LLM 给出的任何数学结论，都必须经过外部校验。即使它给出的证明步骤在局部看起来无懈可击，也可能在某个隐含假设上出错；即使它的语气非常自信，也可能把两个不同定理的条件混在一起。正确的用法是把 LLM 当成“生成器”，把验证器当成“裁判”。生成器负责提供候选，裁判负责判决，人负责设计验证策略和最终决策。

注意：当你要求 LLM 证明一个定理时，第一反应不应该是“它说的对不对”，而应该是“它给出的断言能不能转成一个可执行的检查”。

2. 搭建一套能跑通数学辅助流程的环境

2.1 模型选择与访问方式

选择模型时，不需要一上来就追求最大参数版本，而是看数学推理和代码生成能力是否够用。常见做法分两条路线：

在线 API 路线：调用当前可用的商用模型接口，优点是部署成本低、数学能力较强；缺点是数据隐私和费用需要评估。具体用哪家、什么版本，要以你实际申请到的接口为准。
本地模型路线：使用 Ollama 或 vLLM 加载开源数学系模型，例如 Qwen2.5-Math、DeepSeek-R1 等。优点是数据可控、可离线实验；缺点是显存要求高，推理速度不如在线接口。

两条路线可以抽象成同一个函数调用：给一个 prompt，返回一段文本。这样做的最大好处是，后续所有示例代码都可以在同一套接口上运行，不需要因为换模型而重写逻辑。

场景	推荐方式	注意点
快速原型验证	在线 API	注意 token 限制和输出稳定性
隐私数据或离线环境	本地模型	确认显存、量化精度和数学能力
自动化批处理	本地模型	设定超时、重试和结构化输出
学习调试	在线 API 或本地均可	用温度低参数减少随机性

2.2 创建 Python 项目和依赖

下面用一个最小项目math-llm-lab作为实验环境。这个项目会把 LLM 调用、符号计算、验证逻辑放在同一套代码里，方便连成管线。

mkdir math-llm-lab cd math-llm-lab python -m venv .venv source .venv/bin/activate pip install -r requirements.txt

在项目根目录创建requirements.txt：

requests==2.32.3 openai==1.48.0 sympy==1.13.2 python-dotenv==1.0.1 jupyter==1.0.0

解释一下为什么选这些依赖：openai是调用 OpenAI 兼容接口的客户端；sympy用于符号验证；python-dotenv用于读取 API Key，避免把密钥写进代码；jupyter用来做交互式探索，方便一格格观察输出。

2.3 把 LLM 和符号计算器连成一条管线

数学辅助工作流不建议“问一句答一句”，而是建议设计成管线：输入数学问题，LLM 生成候选表达式或证明步骤，解析器提取结构化内容，符号计算器或定理证明器验证，最后把验证结果返回给人。

下面这段代码演示了一个最小封装，把 LLM 调用和 SymPy 验证放在一起：

import os import openai from sympy import sympify, simplify client = openai.OpenAI( base_url=os.getenv("LLM_BASE_URL", "https://api.openai.com/v1"), api_key=os.getenv("LLM_API_KEY"), ) def ask_expression(problem: str) -> str: resp = client.chat.completions.create( model=os.getenv("LLM_MODEL", "gpt-4o-mini"), messages=[ {"role": "system", "content": "你只输出 LaTeX 数学表达式，不要解释。"}, {"role": "user", "content": problem}, ], temperature=0.2, ) return resp.choices[0].message.content.strip() def verify_identity(candidate: str, x_sym) -> bool: expr = sympify(candidate) return simplify(expr) == 0

这里的关键点是：ask_expression负责生成，verify_identity负责判断。不要把 LLM 的文本输出直接当作结论，而是先转成 SymPy 表达式再验证。实际项目中，base_url、api_key、model都应该从环境变量读取，禁止硬编码。

3. 三个最小可运行示例：从“聊天”变成“开发”

这一节通过三个示例说明 LLM 在数学发展中三种典型用法：触发猜想、把自然语言推导转成可执行计算、生成形式化证明骨架。三个示例都遵循同一个原则：LLM 只做生成，验证交给机器。

3.1 示例一：用数值实验触发猜想

很多数学猜想最初来自数值观察，但观察数据本身往往稀疏、无序。LLM 可以帮助从数据中提出候选公式。比如先给模型一组序列数据，请它猜测规律。

import openai import os client = openai.OpenAI( base_url=os.getenv("LLM_BASE_URL", "https://api.openai.com/v1"), api_key=os.getenv("LLM_API_KEY"), ) data = { 1: 1, 2: 4, 3: 9, 4: 16, 5: 25, 6: 36, } prompt = f""" 我做了数值实验，得到 n 与 f(n) 的对应关系： {data} 请给出一个最自然的候选公式，用 LaTeX 表示。 只输出公式，不要输出解释。 """ resp = client.chat.completions.create( model=os.getenv("LLM_MODEL", "gpt-4o-mini"), messages=[{"role": "user", "content": prompt}], temperature=0.2, ) print(resp.choices[0].message.content)

如果模型输出f(n) = n^2，这只是候选。接下来要做的不是停止，而是用更多数值验证，并继续追问“为什么”：

for n in range(1, 100): if n * n != sum(2 * k - 1 for k in range(1, n + 1)): print("候选公式与数值实验结果不一致") break else: print("前 99 项数值验证通过")

这段代码验证的是：前 n 个奇数的和等于 n 的平方。一旦候选公式通过数值验证，才能进入下一步，思考它是否由已知定理推导得出。

这里有一个重要提醒：数值通过永远不等于证明。它可以提高置信度，也可以暴露错误，但唯一能作为最终结论的，是完整逻辑证明或形式化验证。

3.2 示例二：把自然语言证明步骤转成 SymPy 验证

数学推导中最容易被 LLM“一本正经地编错”的场景是恒等式化简。比如让 LLM 判断一个三角函数恒等式是否成立，它可能直接给出“成立”，但实际缺少条件。更稳妥的方式是让 LLM 生成一个候选表达式，然后用 SymPy 去验证。

from sympy import symbols, simplify, sin, cos, tan, expand x = symbols("x", real=True) # 候选恒等式：sin(x)^2 + cos(x)^2 = 1 candidate = sin(x) ** 2 + cos(x) ** 2 - 1 print("化简结果:", simplify(candidate))

预期输出是0，代表该恒等式对实数 x 恒成立。如果把候选改成(sin(x) + cos(x))^2 = 1，化简结果不会为 0，说明它不成立。

这个例子的工程含义是：LLM 可以负责把“人类语言的推导”转换成数学表达式，但转换结果必须能在符号环境中执行。SymPy 的simplify、expand、factor、equals都是常用的校验函数。注意，SymPy 的sympify只能解析它支持的语法，LLM 输出的 LaTeX 需要先用parse_latex之类的工具转换，或者让模型输出 Python/SymPy 语法而不是 LaTeX。

3.3 示例三：LLM 生成 Lean 4 证明骨架，再由编译器把关

形式化证明是数学发展的另一个重要方向。Lean 4 是目前社区活跃度很高的证明助手。LLM 在这里的用法不是直接证明所有定理，而是生成证明骨架和中间目标，再由 Lean 的编译器检查每一步是否合法。

先用 elan 安装 Lean 4 工具链，并在 VS Code 中安装 Lean 插件：

curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash mkdir -p math-llm-lab/Lean cd math-llm-lab/Lean

创建一个最简单的验证文件Test.lean：

import Mathlib.Data.Real.Basic example (a b : ℝ) (h : a = b) : a ^ 2 = b ^ 2 := by rw [h]

这是一个非常基础的示例：如果 a 等于 b，那么 a 的平方等于 b 的平方。LLM 可以学习这类证明模式，然后在一个大定理的背景下生成若干中间步骤，但每个步骤必须通过 Lean 的类型检查。遇到不通过的步骤，就把 Lean 的错误信息回传给 LLM，让它重新生成，形成“生成—检查—反馈—再生成”的循环。

注意：Lean 的版本、Mathlib 版本不一致会导致大量无意义报错。项目里建议固定版本，并把版本信息写在 README 或 CI 配置里。

4. 让数学任务稳定输出的提示词设计与参数选择

4.1 生成参数：温度不是越高越好

LLM 的采样参数对数学输出影响很大。数学推理需要确定性，而发散性任务需要多样性。

参数	常见范围	数学证明与化简	猜想搜索与头脑风暴
temperature	0 到 2	0 到 0.3	0.7 到 1.0
top_p	0 到 1	0.1 到 0.5	0.8 到 0.95
max_tokens	视模型而定	足够容纳完整推导	允许较长的逐项分析
stop	自定义	遇到分隔符停止	用于结构化输出结束

从实践角度，做数学验证类任务时，推荐先把 temperature 设为 0，避免模型在同样的 prompt 下输出不同结果。只有在探索猜想、生成反例候选时，才提高温度，让模型给出更多样化的假设。

4.2 数学提示词模板

面向数学任务的 prompt 与普通提问不同。普通提问容易得到“综合回答”，数学任务最好要求模型输出结构化、可检查的内容。下面是一个可复用模板：

你是一名严谨的数学研究助手。当你处理数学问题时，必须遵守以下规则： 1. 先用一两句话复述问题，确保理解正确。 2. 把证明或推导拆成编号步骤，每步注明使用的前提条件。 3. 涉及恒等式化简时，输出一个可被 SymPy 解析的表达式。 4. 如果存在边界条件或反例，显式写出。 5. 结论必须放在 "结论：" 之后，便于程序解析。 问题：<这里放你的数学问题>

添加“复述问题”这一步，可以显著降低模型答非所问的概率。因为模型在生成回答前，先被迫把问题语义压缩成自己的表述，如果理解偏差，人马上能看出来。

4.3 把对话式交互改成函数式调用

在科研流程中，更推荐函数式调用而不是交互式聊天。原因是函数调用可以方便地做批处理、缓存和日志记录。比如把所有数学提问统一封装成ask_math_tasks，返回 JSON，方便后续自动验证。

import json def ask_math_tasks(problem: str) -> dict: prompt = f""" 你是数学助手。请按 JSON 格式回答，字段包括： - restatement: 问题复述 - steps: 推导步骤列表 - conclusion: 最终结论 问题：{problem} """ resp = client.chat.completions.create( model=os.getenv("LLM_MODEL"), messages=[{"role": "user", "content": prompt}], temperature=0.2, response_format={"type": "json_object"}, ) return json.loads(resp.choices[0].message.content)

这种做法的好处是：输出的 JSON 可以直接进入下一步验证管线，而不用靠正则从自然语言中抽取内容。注意，response_format参数并不是所有模型都支持，本地模型可能需要改用“只输出 JSON，不要输出其他文本”的提示词。

5. 输出的数学结果必须经过三层验证才能进入研究流程

5.1 数值抽查：用随机数据暴露错误

数值验证是成本最低的第一层防线。无论是恒等式、不等式还是近似公式，都可以用随机采样验证。下面代码检查一个 LLM 给出的恒等式是否在大量随机点上成立：

import random from math import sin, cos count = 10000 for _ in range(count): x = random.uniform(-1000, 1000) lhs = sin(x) ** 2 + cos(x) ** 2 rhs = 1.0 if abs(lhs - rhs) > 1e-9: print("发现反例:", x) break else: print(f"{count} 个随机样本均通过")

注意，随机点可能落在函数的奇点附近，也可能因为浮点误差出现误报。所以数值抽查适合“快速排除明显错误”，不适合给出正确性终审。遇到在特殊点不成立的候选公式，多半是因为模型遗漏了定义域条件。

5.2 符号验证：SymPy 做精确化简

数值验证通过后，进入符号验证。好处是可以在不做近似的情况下判断表达式是否恒等。以 SymPy 为例：

from sympy import symbols, simplify x = symbols("x") # LLM 给出的恒等式 lhs = (x + 1) * (x - 1) rhs = x ** 2 - 1 print(simplify(lhs - rhs)) # 0 表示恒等

SymPy 的simplify并不总能对复杂表达式给出最简形式，所以如果一个恒等式验证失败，先不要急着否定，可以尝试expand(lhs - rhs)、factor(lhs - rhs)，或者使用trigsimp、powsimp等专用化简函数。这也是工程上的常见坑：验证器本身的能力边界会影响判断结果。

5.3 形式化验证：Lean 4 把证明交给类型检查器

对于需要作为研究成果的定理，最终推荐落到形式化证明工具。Lean 4 把数学证明变成了一组可以被编译器检查的命令。

import Mathlib.Data.Real.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric example (x : ℝ) : sin x ^ 2 + cos x ^ 2 = 1 := by exact ?_

在最开始写exact ?_只是为了先让 Lean 显示当前目标，再根据目标逐步补充证明。LLM 可以在这个阶段生成候选 tactic 序列，但每个 tactic 都必须通过 Lean 检查。实际上，这里推荐把 LLM 当作用来生成“下一步要做什么”的辅助，而不是期望它一次性输出完整证明。

三种验证方式的定位如下表：

验证层	工具示例	计算性质	结论强度	适用场景
数值抽查	Python + random	浮点近似	仅排除明显错误	快速筛选候选
符号验证	SymPy、SageMath	精确符号运算	可判断恒等式	论文推导、公式化简
形式化验证	Lean、Coq、Isabelle	逻辑证明检查	证明完全可靠	正式成果、大型定理

5.4 最后检查 LaTeX 可编译

数学论文里，LLM 输出的 LaTeX 经常存在无法编译的问题，常见的包括\left...\right不配对、自定义宏未定义、缺少%转义。处理方式是让模型输出“只含公式”的内容，然后用pylatexenc或临时 LaTeX 文档检查可编译性。

pip install pylatexenc

from pylatexenc.latex2text import LatexNodes2Text latex = r"\sum_{k=1}^{n} k = \frac{n(n+1)}{2}" text = LatexNodes2Text().latex_to_text(latex) print(text)

这一步虽然不校验数学正确性，却能避免把“无法编译的公式”带进论文草稿。实际项目中，可以把 LaTeX 检查放在 CI 里，每次修改论文源文件后自动跑一遍。

6. 常见坑与排查路径

6.1 五个高频问题

问题现象	可能原因	检查方式	处理建议
模型自信地给出错误恒等式	LLM 生成的是近似正确文本，不是逻辑判断	随机抽样数值验证、SymPy simplify	所有结论强制走验证管线，不直接采信
输出的 LaTeX 无法编译	定义了不存在的宏、括号不配对	pylatexenc 或 LaTeX 文档编译	要求模型只输出公式；在 CI 中加入编译检查
浮点数验证整数结论	数据溢出或浮点误差	更换为大整数、Fraction、有理数类型	整数类结论用整数运算或形式化证明验证
Lean 代码大量报错	Lean 或 Mathlib 版本不一致	查看`lake env lean`版本和报错信息	固定版本，统一用 elan 工具链
同样 prompt 每次结果不同	temperature 设置过高	打印采样参数和完整 prompt	验证类任务 temperature 设为 0，并记录 seed

6.2 排查一条生成结果的完整路径

当发现 LLM 输出结果异常时，按下面的顺序排查，能快速定位问题在哪个环节：

先确认输入问题本身是否表达完整。问题含糊、缺少定义域和条件，模型自然容易答偏。
再确认 prompt 是否要求结构化输出。如果没有，结果可能被解释性文本污染。
检查模型参数。temperature、top_p 是否在验证场景下过高。
检查解析环节。SymPy 解析失败时，优先看 LaTeX 中是否有 SymPy 不支持的语法。
检查验证器本身。SymPy 对某些特殊函数化简不彻底，不代表命题必然错误。
检查版本。Lean、Mathlib、SymPy 的版本差异会改变可用的 API 和化简行为。
最后回到数学判断。如果所有机器验证都通过，再询问自己：这个结论是否合理，是否遗漏了边界条件。

顺序遵循“输入 -> 生成 -> 解析 -> 验证 -> 版本 -> 数学判断”的原则，每一步都能通过打印日志和中间结果确认。

7. 从实验到研究：可复用的工作清单与下一步方向

7.1 使用 LLM 做数学辅助的检查清单

下面这份清单适合在每次把 LLM 输出引入研究流程前逐项核对：

问题是否明确到“可判定”：是否存在反例空间、定义域是否完整。
prompt 是否限制了输出格式：JSON、LaTeX 或 Lean 代码要明确指定。
是否关闭了随机性：验证类任务 temperature 是否设为 0。
是否做过数值抽查：至少覆盖正常区间和边界点。
是否做过符号验证：能用 SymPy 化简的恒等式不能只靠肉眼判断。
是否做过形式化验证：正式成果是否进入 Lean 或 Coq 检查。
是否保留完整日志：prompt、输出、验证结果、版本号是否可回放。
是否由人做了最终判断：模型结论在整体证明策略中是否合理。

7.2 学习环境与研究环境的差异

维度	学习实验环境	正式研究/生产环境
数据隐私	可直接调用在线 API	需评估隐私，必要时本地模型
验证强度	数值抽查即可	需要符号验证加形式化证明
日志	打印在 Jupyter 即可	落盘、版本化、可追溯
API Key 管理	环境变量	密钥管理服务
错误处理	直接报错就行	超时、重试、失败降级
版本控制	可有可无	Lean/Mathlib/SymPy 版本全部固定

7.3 可以继续深入的方向

数学论文知识库：把已发表的论文解析后存入向量数据库，用 RAG 让 LLM 在回答前先检索相关定理和上下文，减少幻觉。
定理证明智能体：构建“LLM 生成步骤 + Lean 检查 + 错误回传”的循环，逐步提高自动化证明的长度和复杂度。
多智能体协作：一个模型负责猜测引理，另一个模型负责找反例，第三个负责形式化，形成互相验证的闭环。
从教学到科研的迁移：先在课堂和练习题中跑通流程，再逐步用于文献整理、公式纠错和论文草稿检查。

实际做项目时，最值得优先投入的是验证管线，而不是模型本身。模型总会迭代，API 总会变，但“任何生成结果都必须经过外部验证”这一原则是长期有效的。把这条原则固化到代码里，LLM 才能真正成为数学发展中可靠的生产力工具。

大语言模型数学辅助工作流：从候选生成到符号验证的工程实践