LLM辅助数学研究：从反例构造到形式化证明的实践指南

这次我们来看一个比较特殊的 AI 项目Examples for use of AI and especially LLMs in major mathematical developments。它不是又一个界面漂亮的 WebUI也不是又一个能出图的扩散模型而是一组聚焦“LLM 在重大数学发展中能做什么”的示例集合。直白说这个项目的核心不是在演示“AI 能聊数学题”而是在梳理当数学家面对一个真正困难的研究问题时LLM 到底能在哪个环节产生实质帮助以及怎么验证它给出的结果是否可靠。从材料看这类示例通常覆盖反例构造、证明补全、形式化证明辅助、文献分析、数值实验设计等方向。它的特点可以归纳为几点一是以“示例驱动”而不是“模型驱动”重点在方法论二是强调“建议搭配形式化验证工具使用”不鼓励把 LLM 的推理结果直接当结论三是对环境要求比较灵活既可以用 API 调用大模型也可以接本地推理服务。这篇文章我会按“能用来做什么、环境怎么准备、示例怎么跑、效果怎么验证、批量任务怎么做”的顺序展开尽量给出一套可以落地的操作思路。内容会比较适合三类读者想用 AI 辅助数学研究的科研人员和学生、在 LLM 应用层做垂直场景开发的工程师、以及打算把 LLM 接入验证流程Lean/Coq/SymPy的技术爱好者。如果你只是想把 LLM 当计算器用这文章可能帮不上太多忙但如果你关心的是“AI 在数学推理里到底有没有用、怎么用才不算瞎用”那这篇可以直接收藏。1. 核心能力速览能力项说明项目类型AI/LLM 在数学研究中应用的示例集合偏向方法论与案例实践核心方向反例构造、证明草稿补全、形式化证明辅助、文献与符号推理、数值实验设计运行方式Jupyter Notebook / Python 脚本 / LLM API / 本地推理服务推荐环境Python 3.9、Jupyter 或 VSCode需要连接 LLM 服务模型接入OpenAI 兼容 API 或本地模型Ollama、vLLM、LM Studio 等按需自备显存占用API 模式几乎无本地显存压力本地模型显存取决于模型参数量与量化格式需按实际测试是否支持批量任务支持可通过脚本对多道数学题或多组超参数循环调用是否支持 API取决于所选 LLM 服务示例本身通常不强制自带后端部署难度低到中主要成本在 prompt 设计、验证闭环和结果评估适合场景数学研究辅助、教学演示、推理测评、形式化证明环境接入这里要说明一下由于原始材料没有给出具体的仓库地址、作者团队、依赖清单和示例文件清单上表中的“显存占用”“是否支持 API”等条目只能按通用情况给判断。真正部署时需要以你拿到的项目 README 或示例代码为准。2. 适用场景与使用边界AI 在数学发展中的价值不在于让模型直接“写出一个惊天动地的证明”而在于它能把人类研究者从重复性、机械性的探索中解放出来。从实际用途看LLM 在这类项目里最常见的角色有五个反例搜索。针对一个猜想或命题让模型尝试构造反例或者分析命题在哪些边界条件下会失效。数学研究中反例往往比证明更能推动认知前进。证明草稿生成。给定定理描述和部分证明思路让模型补全中间步骤。这能提供一个“初稿”再由数学家验证和修正。形式化证明辅助。Lean、Coq、Isabelle 等交互式证明助手使用门槛高LLM 可以帮忙生成 tactic 序列或者解释报错信息降低入门成本。文献与概念分析。把一段数学摘录或某个定义交给模型让它梳理逻辑依赖、给出直觉解释、列出相关引理。数值实验与代码生成。让模型生成 Python/SymPy 代码来验证某些特殊情形辅助形成更严谨的猜想。但也要把边界说清楚。这里最大的风险是“幻觉”和“格式正确但逻辑错误”。LLM 输出的证明过程可能看起来完全合理实际上中间藏着跳步或错误假设。所以任何使用场景都必须搭配符号计算、形式化验证工具或者至少经过数学家的严格复核。还有几类场景不建议使用涉及保密或未公开研究内容的场景不要把私有思路直接传给外部 API。需要确定性输出的场景比如自动判题系统LLM 可能给出不一致答案。涉及版权材料、他人论文正文的场景未经授权不要整篇投喂给模型做分析。如果后续要在论文或项目中引用 AI 辅助得到的结论建议遵循学术规范明确标注 AI 的参与程度并保留 prompt、模型版本和验证日志方便追溯。3. 环境准备与前置条件这个项目不像常见的 ComfyUI 或 WebUI没有一个“双击启动”的固定入口。更合理的做法是把它当作一个实验环境来搭建。下面是一套通用检查清单具体版本以实际项目说明为准。3.1 基础软件操作系统Linux / macOS / Windows 均可。Linux 在本地 LLM 推理和生产化批量任务上更省心。Python建议 3.9 以上。多数 LLM SDK、符号计算库和 Notebook 都依赖较新的 Python。Jupyter Notebook 或 Jupyter Lab适合跑示例和交互式调试。Git克隆示例代码、管理 prompt 和实验脚本版本。# 通用安装命令具体包名以项目 requirements.txt 为准 python -m venv .venv source .venv/bin/activate # Windows 下使用 .venv\Scripts\activate pip install jupyter notebook openai python-dotenv sympy3.2 LLM 服务接入有两类接入方式云端 APIOpenAI、Anthropic、Google 等厂商提供的 API接入简单不占用本地显存。需要准备 API Key并在环境变量中配置。本地推理服务Ollama、LM Studio、vLLM 等。适合数据敏感、希望控制成本的场景。缺点是会占用 CPU/GPU 资源显存需求取决于模型大小。如果选择本地服务可以先拉一个较小的数学推理能力不错的模型比如 Qwen 系列或 DeepSeek 系列的量化版本。不要一开始就上 70B 级别的模型先跑通流程再换大模型是更稳妥的做法。3.3 形式化验证工具可选如果示例涉及证明辅助需要安装 Lean 4 或 Coq。以 Lean 4 为例一般通过 elan 安装工具链# Lean 4 安装示例具体版本见 Lean 官方文档 curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh elan default stable这里提醒一句Lean 和 Coq 的学习曲线比较陡如果只是先看示例可以直接跑“LLM 生成证明草稿 人工判断”的闭环不一定要立刻引入形式化验证。3.4 环境变量配置建议把 API Key 和模型配置写入.env而不是写在代码里。示例# .env 示例修改成你自己的配置 LLM_API_KEYsk-xxxx LLM_BASE_URLhttps://api.openai.com/v1 LLM_MODELgpt-4o-mini LLM_TEMPERATURE0.2这样既方便批量任务切换模型也避免 Key 泄露。4. 安装部署与启动方式由于没有具体的仓库地址这里给出一套“拿到示例代码后如何启动”的标准化流程。如果你已经拿到了 GitHub 仓库地址第一步就是克隆仓库git clone your-example-repo-url cd example-repo-directory然后创建虚拟环境并安装依赖python -m venv .venv source .venv/bin/activate # Windows 下使用 .venv\Scripts\activate pip install -r requirements.txt启动 Jupyterjupyter notebook如果项目提供的是纯 Python 脚本则可以直接用命令行运行python examples/01_counterexample_search.py --prompt Your math statement here从部署难度看这类项目通常比部署 Stabel Diffusion WebUI 简单得多因为核心计算在 LLM 服务端本地只是做 prompt 拼装和结果解析。最容易出问题的反而是环境变量没配对、API 模型名写错、或者 Jupyter 内核没有选中虚拟环境。5. 功能测试与效果验证测试这类示例不能只盯着“模型有没有输出”更要关注“输出是否正确、是否可验证”。下面给出 5 类典型测试用例每个用例都包含输入示例、操作步骤、判断标准和失败排查思路。5.1 反例搜索测试测试目的验证 LLM 是否能够针对给定的数学命题构造反例或边界情况。输入示例命题对所有实数 a、b都有 |a b| |a| |b|三角不等式。 这个命题是否成立如果成立请给出思路如果不成立请给出反例。操作步骤构造一个包含命题描述的 prompt。设置较低的温度参数如 0.2避免输出过于发散。运行示例脚本并记录输出。将模型输出的反例代入原命题用 SymPy 验证。预期结果模型能识别三角不等式成立并给出证明思路如果命题不成立应能给出具体数值反例。判断是否成功代入验证后如果输出与命题的真假一致且验证代码运行结果正确认为通过。失败排查如果模型给出错误反例尝试在 prompt 中增加“请先判断命题真假再给反例最后用数值验证”。如果模型反复出错考虑换更大的模型或改用带数学推理增强的模型。5.2 证明补全测试测试目的考察 LLM 补全数学证明中间步骤的能力。输入示例证明如果 n 是奇数那么 n^2 也是奇数。 已知n 2k 1k 为整数。 请补全从 n 2k 1 到 n^2 是奇数的完整推理步骤。操作步骤把“已知条件 目标结论 当前进度”一起放入 prompt。要求模型分步输出并标记每一步依据。人工检查是否存在跳步。用符号运算验证关键恒等式。预期结果模型能写出 n^2 (2k1)^2 4k^2 4k 1 2(2k^2 2k) 1从而说明 n^2 是奇数。判断是否成功证明链完整没有逻辑断点所有代数运算正确。失败排查如果模型直接从 4k^2 4k 1 跳到结论缺少“令 m 2k^2 2k则 n^2 2m 1”这一步需要在 prompt 中强调“必须明确构造 m”。5.3 形式化证明辅助测试测试目的验证 LLM 是否能生成可被 Lean/Coq 接受的证明片段。输入示例Lean 4 中如何证明theorem sq_odd {n : Nat} (h : Odd n) : Odd (n ^ 2) : by操作步骤把目标定理和现有代码上下文传给 LLM。让模型生成by后面的 tactic 序列。用 Lean 编译器执行观察是否报错。如果报错将错误信息反馈给 LLM迭代修复。预期结果模型生成类似rcases h with ⟨k, rfl⟩, use 2 * k * (k 1), ring的可编译代码。判断是否成功Lean 编译器无报错且所有目标都被关闭。失败排查常见问题是模型不熟悉 Lean 4 的库函数可以喂给它对应的 import 列表和已有的辅助定理。也可以在 prompt 中加入“请使用数学库 Mathlib 中已有的定理”。5.4 文献概念分析测试测试目的验证 LLM 是否能把一段抽象数学文本拆解成结构化的逻辑关系。输入示例给定以下定义 “一个群 G 的子群 H 被称为正规子群如果对任意 g in G 和 h in H都有 g*h*g^{-1} in H。” 请解释1) 这个定义试图刻画什么结构2) 它与商群构造的关系3) 给出一个非平凡的正规子群例子。操作步骤把定义和问题一起发送给模型。要求输出格式化为三部分直觉解释、逻辑关系、例子。人工核对例子是否准确。如果用 Lean 或代码验证可以把例子转成具体集合运算。预期结果模型能指出正规子群是“对共轭运算封闭的子群”并能解释商群构造依赖于正规性条件。判断是否成功解释中的核心结论与教材一致例子构造正确。失败排查如果模型把“正规子群”和“特征子群”概念混淆需要补充提示词明确要求区分不同子群类型。5.5 数值实验代码生成测试测试目的验证 LLM 能否生成可运行的代码来辅助验证数学猜想。输入示例请用 Python 验证对于所有 1 n 10000n^3 n 1 都是质数。 如果发现反例输出第一个反例的 n 值。操作步骤运行模型生成的代码。观察代码是否能正确结束并输出结果。验证输出是否正确实际上这个命题很可能在某个 n 处失败。如果代码报错把报错信息返回给 LLM 修复。预期结果模型生成的代码可以运行并输出某个使表达式非质数的 n或者用户自行用 SymPy 验证时发现更小的反例。判断是否成功代码运行无致命错误输出结果经过独立验证正确。失败排查很多 LLM 在这个测试里会“偷懒”只检查了少量 n 就直接下结论。解决方法是要求模型必须遍历全部范围并打印检查过的最大 n。6. 接口 API 与批量任务这类项目非常适合批量化处理把一组数学命题交给 LLM让模型逐一判断、证明或构造反例然后收集结果并分析。下面给出一个通用 API 调用模板和批量目录设计路径和参数需要按实际项目调整。6.1 通用 API 调用示例import os import json import time from openai import OpenAI client OpenAI( api_keyos.environ.get(LLM_API_KEY), base_urlos.environ.get(LLM_BASE_URL, https://api.openai.com/v1), ) def ask_math_model(prompt: str, model: str None, temperature: float 0.2) - str: 通用数学 prompt 调用返回模型输出文本。 model model or os.environ.get(LLM_MODEL, gpt-4o-mini) response client.chat.completions.create( modelmodel, messages[ { role: system, content: 你是一位严谨的数学研究者。输出必须明确区分已知条件、推理步骤和结论。 }, {role: user, content: prompt}, ], temperaturetemperature, ) return response.choices[0].message.content6.2 批量任务设计建议将所有待测试数学题放入inputs/目录每条记录包含唯一 ID、命题描述、期望输出类型和验证代码。输出结果统一写入outputs/并用 JSONL 格式保存。{ id: prob_0001, statement: 对所有实数 a、b都有 |a b| |a| |b|。, task_type: prove_or_disprove, expected: true, note: 三角不等式 }批量循环脚本可以这样写import json import time with open(inputs/propositions.jsonl, r, encodingutf-8) as f: tasks [json.loads(line) for line in f if line.strip()] results [] for task in tasks: prompt ( 请判断以下命题是否成立。如果成立给出证明思路 如果不成立给出反例。请先明确你的结论。\n\n task[statement] ) try: answer ask_math_model(prompt) results.append({ id: task[id], statement: task[statement], answer: answer, status: ok, }) except Exception as exc: results.append({ id: task[id], statement: task[statement], error: str(exc), status: failed, }) time.sleep(1) # 简单限速避免触发接口频率限制 with open(outputs/results.jsonl, w, encodingutf-8) as f: for item in results: f.write(json.dumps(item, ensure_asciiFalse) \n)6.3 失败重试策略批量任务最常见的问题是网络超时、API 限流、模型偶尔给空输出。建议在代码里加入最多 3 次重试且每次重试时把错误信息追加到 prompt 里帮助模型在二次生成时避免同样的错误。同时为每个任务记录时间和模型名称方便后续分析不同模型在数学任务上的成功率。7. 资源占用与性能观察这个项目比较特殊的点在“算力消耗其实不在本地”。如果你走云端 API 路线本地资源占用可以忽略不计主要成本是 Token 费用和网络延迟。一个包含完整证明草稿的 prompt 可能消耗几千 Token如果批量运行需要提前估算预算。如果选择本地模型重点观察这几个指标显存占用。模型参数量、量化位数和上下文长度都会影响显存。7B 量化模型和 70B 全精度模型的差距非常大。不要轻信网上的固定数字建议用nvidia-smi实时看高水位。推理速度。数学证明往往需要长输出每步生成时间会明显拉长。小模型在普通显卡上可能勉强可用大模型会让人等到怀疑人生。上下文长度。长证明很容易截断上下文窗口。如果模型一次只能处理 8K 上下文可以考虑把证明切成多个阶段先让模型生成前半段再让模型基于前半段续写后半段。并发与批处理。本地推理服务通常支持并发请求但显存会被并发任务同时占用可能 OOM。建议先跑单条任务确认显存余量再逐步提高并发数。如果想降低资源占用优先从三点入手改用 API、使用量化模型、缩短单次 prompt 长度。把大任务拆成多轮对话会比一次性输入超长文本更稳。8. 常见问题与排查方法问题现象可能原因排查方式解决方案调用 API 返回 401API Key 错误或环境变量未加载检查.env文件和os.environ输出重新配置 Key确认代码读取了.env模型返回内容为空上下文过长截断、温度过高或内容被安全策略过滤查看返回对象的 finish_reason 字段缩短输入、降低温度或重试构造的反例验证失败模型“幻觉”出错误数值用 SymPy 手动复算模型给的反例在 prompt 中加入“请自行用 Python 验证”Lean 代码编译报错模型不熟悉当前版本库函数查看错误信息和 import 列表把 import 和已有 theorem 传入 prompt批量任务跑到一半中断API 限流、网络超时、进程被杀查看任务日志和异常栈加入重试机制延长 sleep 间隔显存不足OOM本地模型过大或并发数过高用nvidia-smi查看显存占用换量化模型降低并发减小 max_tokens模型输出大段 Markdown 公式难以解析prompt 未约束输出格式查看原始输出在 prompt 中要求输出纯 LaTeX 或 JSON 结构证明逻辑跳步模型缺乏验证意识人工检查证明链要求模型分步输出并为关键步骤补充重述如果一条 prompt 反复失败不要一直重试同样的 prompt。先把问题拆小或者换个模型试。很多情况下小模型 清晰的分步 prompt 效果优于大模型 模糊 prompt。9. 最佳实践与使用建议这类项目要从“能跑通示例”进化到“能帮上数学研究”需要建立一套工程化习惯。第一为每个实验保留完整的 prompt、模型版本、温度参数和输出日志。数学推理结果不像图像生成那样容易一眼判断好坏没有记录后面完全无法复盘。第二把 LLM 当“研究助理”而不是“裁判”。所有数学结论都必须经过符号计算、形式化证明或人工复核才能进入正式笔记。建议固定的验证流程是LLM 生成结论计算工具验证特例数学家判断全局。第三第一次跑示例时先拿一个自己已经知道答案的数学问题测试。比如先让 LLM 证明“根号 2 是无理数”确认它能输出标准证明再让它尝试没把握的命题。这样能快速判断模型在这类任务上的可靠性。第四对 prompt 做版本管理。数学 prompt 的写法对结果影响很大。例如“请判断命题真假”和“请先尝试证明如果失败则构造反例”会产生完全不同的输出。可以把 prompt 模板放入prompts/目录用文件命名区分版本。第五关注输出中的“确定性语言”。一个严谨的数学响应应该包含清晰的假设、推理链和结论。如果模型大量使用“显然”“易得”等词大概率是偷懒或掩盖跳步需要追问它补充细节。第六涉及引用和版权时保持谨慎。如果分析对象是别人的论文、图表或未公开数据必须确认授权。AI 辅助生成的内容在后续发表时也应按规定声明。10. 总结与下一步如果第一次接触这类项目最值得先测的其实是两件事反例搜索和证明补全。这两个场景门槛低、反馈直接能很快暴露 LLM 在数学推理上的短板和优势。建议先跑一个最简单的恒等式验证比如让模型判断“所有偶数平方都是 4 的倍数”是否成立然后要求它给出证明。跑通这一条完成“构造 prompt - 调用模型 - 符号验证 - 记录日志”的闭环再逐步扩大任务难度。最容易踩的坑有两个。一是把 LLM 的证明当成权威结论实际上它可能在代数变形里悄悄出错二是 prompt 写得过于宽泛模型不知道你希望它“证明、反驳还是构造反例”。把这两个问题解决了这个项目的价值才能体现出来。后续如果想继续深入可以考虑三条扩展方向接入 Lean 4 或 Coq 做形式化辅助、用多个模型对同一命题做结果投票、把实验脚本封装成带重试和进度条的批量工具。这样一步一步来AI 在数学研究流程里就不会只是一个“聊胜于无”的聊天窗口而是一个可以追踪、验证、存档的研究基础设施。