AI数学思维与验证闭环:大模型推理能力边界及工程实践 最近在技术社区里有一个讨论让我印象很深陶哲轩在菲尔兹奖大师课内容被反复转发核心观点是“AI 还没有学会顶级数学家的思维但普通人却可以通过训练掌握这种思维”。评论区里很多同学在争论——大模型不是已经能解竞赛题、写证明过程、做符号计算了吗为什么说它还没学会数学思维普通人又凭什么能学会作为一个经常用大模型做代码生成、算法验证和 AI 应用开发的工程师我理解这个问题的角度不太一样。AI 缺的不是计算能力也不是知识量而是“提问、猜想、构造反例、验证、重构”这一整套闭环。而恰恰是这套闭环才是数学思维的核心。本文我想从技术角度拆解这件事为什么大模型会在这类任务上露出短板普通开发者如何把“验证闭环”补进 AI 应用里以及我们如何用一套可运行的工程方案让大模型在做数学推理时更接近人类思维。这篇文章适合对 AI 大模型应用、AI Agent 开发、数学思维训练感兴趣的开发者阅读内容包含完整代码示例和项目调试思路。1. 背景与核心概念AI 的“会做题”和数学家的“会思考”是两回事1.1 计算能力不等于数学思维要理解陶哲轩这段话的深意我们得先区分两个概念“会做数学题”和“具备数学思维”。大模型在数学题上的表现本质上是一种基于海量语料的条件概率生成。它见过大量数学题的解法、证明过程、题目套路所以在面对类似题目时可以生成看起来非常合理的解题步骤。这也是为什么很多人在用 AI 解高等数学、线性代数、竞赛题时会觉得“它好聪明”。但“会做题”和“会思考”之间有巨大的鸿沟。题目通常有明确条件和固定答案模型要做的只是从训练数据中检索相似的解题模式并组合输出。而真正的数学思维是在没有明确提示的情况下主动提出“这个问题可能和哪个领域相关”“这个猜想是否可能被反例推翻”“这个定义是否还可以再抽象一层”。这种能力不是简单的模式匹配而是对概念结构的深层理解。实际开发中我们也能观察到这个现象。你让大模型证明一个经典结论比如“n 的三次方减 n 能被 6 整除”它可以很快给出漂亮的因式分解证明。但如果你让一个大模型独立探索一个开放性问题比如“是否存在某个多项式它对前 k 个整数都给出素数但之后失效”它很可能会顺着经验给出“应该存在”的猜测却很难主动构造出那个反例。这就是计算能力与思维能力的差距。1.2 顶级数学家的思维到底指什么陶哲轩作为菲尔兹奖得主谈到的数学思维并不是某种玄学而是可以拆解成具体能力的组合。我把它归纳为以下几点。第一是提问能力。数学家最重要的工作不是解题而是提出一个好问题。比如“连续函数是否一定在某点可导”这个问题本身就比答案重要。第二是类比迁移能力。看到一个陌生结构时能联想到以前见过的结构把新问题映射到旧框架中。第三是构造反例的能力。面对一个猜想不是先想着证明它而是先尝试推翻它。这种“先找反例再找证明”的习惯在普通人的思维训练中经常被忽略。第四是审美判断。数学家会在多个证明方案中选择更优雅、更通用的那一个这种品味来自大量实践和经验沉淀。这些能力有一个共同点它们都需要与外部世界交互。提出猜想之后要去验证构造反例之后要去检查证明写完以后要反复寻找漏洞。数学思维不是一次生成出来的而是在“猜想—验证—推翻—修正”的循环中打磨出来的。1.3 普通人为什么反而可以学会为什么陶哲轩说“普通人却可以学会”关键在于数学思维不是天赋而是一套可以刻意练习的思维习惯。它像编程中的调试思维一样不是天生就会而是在反复报错、定位、修复中练出来的。普通人在学习数学时可以随时做试验、举例子、画图、构造反例。这种“试错—反馈—修正”的闭环是大脑学习最自然的路径。而当前的大模型在标准推理模式下缺少这种外部验证闭环——它生成一个结论后往往无法自己判断这个结论是否真的成立。它看起来“知道很多”但缺少“验证自己知道的东西是否正确”的这个环节。换句话说普通人的优势在于可以调用计算器、画图工具、符号计算系统甚至纸张和铅笔来验证自己的想法。只要愿意花时间去试错大多数人都能培养出相当不错的数学直觉。而大模型如果只停留在“生成文本”这一步就永远停留在“纸上谈兵”的阶段。2. 拆解大模型在数学任务上的能力边界2.1 大模型在数学任务中的强项在讨论弱点之前先客观看看大模型在数学任务上的强项。这样我们才能在工程实践中合理利用它的能力而不是一味否定。第一大模型擅长检索与匹配典型题型。它训练语料中包含了大量教材、论文、博客、竞赛题解所以对“常见题型”的解题套路非常熟练。例如求极限、求导数、解微分方程、常见不等式证明等它都能给出规范的步骤。第二大模型擅长生成候选思路。面对一个陌生问题时它可以快速给出多个方向的猜测这相当于一个“思路生成器”。虽然不一定每个思路都对但能提供很有价值的启发。第三大模型擅长文本翻译与形式化描述。它可以把一段自然语言描述的问题转换成数学公式也可以把一段符号推导用自然语言解释出来这种能力对数学交流非常有帮助。在我实际使用经验里大模型最好用的地方不是“直接给答案”而是“生成多个候选证明方案”让人类去筛选。它像一个知识面极广但缺乏判断力的助手可以快速产出大量半成品而人类负责验证和筛选。2.2 大模型在数学任务中的薄弱点大模型的薄弱点同样明显。首先是幻觉问题。大模型在不确定答案时会生成一段“看起来正确”的内容而不是承认自己不知道。这在数学任务是致命的因为数学对严谨性要求极高。比如让模型证明一个结论它可能在中间步骤偷换概念、跳过关键条件甚至编造一个不存在的定理。其次是缺少对反例的敏感度。模型在语料中学到的是“某个命题经常成立”但它很难主动去寻找边界条件。一个命题可能在前 1000 个整数上都成立却在第 1001 个整数上失效大模型生成的思路往往会忽略这类边界检验。第三是缺少长期规划能力。复杂的数学证明往往需要几十步甚至上百步的逻辑链模型在生成长文本时容易遗忘前文假设导致推导到后面出现自相矛盾。这些问题的根源都在于大模型的训练目标——它只学习“下一个词是什么”却没有学习“这句话在数学上是否成立”。就像一个人背了整本数学书却从没动手做过一道需要检验的题目。2.3 从陶哲轩的公开讨论中看 AI 与数学研究陶哲轩在公开场合多次表达过对 AI 工具的兴趣。他的态度并不是全盘否定 AI而是认为 AI 需要与人类数学家形成互补。他更看重的场景是AI 帮助数学家快速处理计算、穷举搜索反例、验证复杂推导而人类数学家负责提出有意义的问题、选择研究方向、判断哪些结果真正重要。这个观点对普通开发者非常有启发。我们使用大模型的时候也应该是“让 AI 负责生成和计算让人类负责提问和验证”的分工模式。尤其在 AI Agent 和 AI 应用开发中不能把大模型的输出当作最终答案而要把“验证模块”嵌入整个系统流程。这也是本文后面实战项目要解决的问题。3. 环境准备与工具版本3.1 运行环境与版本说明在开始写代码之前先明确环境准备。本文的实战项目使用 Python 编写核心依赖是requests和sympy。大模型部分采用 OpenAI 兼容接口也可以替换为本地部署的模型服务。版本号不需要与我的环境完全一致只要满足基本功能即可重点在于掌握整体思路。本文示例环境的参考版本如下工具/依赖版本说明Python3.9 及以上requests2.31.0 及以上sympy1.12 及以上大模型接口任意 OpenAI 兼容的/chat/completions接口操作系统Windows / macOS / Linux 均可如果你本地不方便调用远程大模型接口也可以使用 Ollama 部署本地模型然后把base_url指向本地服务。本文的代码封装了对base_url的可配置支持切换成本很低。需要注意的是不同大模型对数学推理的支持差异很大。在实际项目里建议选择数学能力较强的模型并在正式使用前用固定的测试集做效果对比。本文示例以“思路生成 程序验证”为核心即便模型能力一般也能通过验证模块兜底。3.2 安装依赖创建项目目录后先安装依赖。建议使用虚拟环境。mkdir math-thinking-ai cd math-thinking-ai python3 -m venv venv source venv/bin/activate # Windows 系统使用 venv\Scripts\activate pip install requests sympy安装完成后创建一个config.py文件用来管理大模型接口配置。为了安全和灵活性敏感配置建议通过环境变量注入而不是写死在代码里。# config.py import os # 使用 OpenAI 兼容接口 MODEL_NAME os.getenv(MODEL_NAME, qwen2.5-math) # 按实际模型名修改 BASE_URL os.getenv(BASE_URL, http://localhost:11434/v1) # 本地 Ollama 示例 API_KEY os.getenv(API_KEY, ollama) # 本地服务通常不需要真实密钥如果你使用云厂商的 OpenAI 兼容服务把BASE_URL改为服务商提供的地址再把API_KEY改成自己的密钥。环境变量可以写到项目根目录的.env文件中但注意不要把真实密钥提交到代码仓库。3.3 项目目录结构整个项目采用如下结构math-thinking-ai/ ├── config.py # 配置文件 ├── llm_client.py # 大模型调用封装 ├── verifier.py # 数学命题验证器 ├── pipeline.py # 主流程生成思路 - 验证 - 反思 └── requirements.txt # 依赖清单这样的结构把配置、模型调用、验证逻辑和主流程分开方便后续扩展。比如你想增加新的数学命题只需要在verifier.py中新增验证函数想更换模型只需修改config.py。4. 核心原理把“验证”补进 AI 的推理闭环4.1 为什么单独的生成式推理不可靠大模型的标准使用方式是“输入 Prompt输出答案”。这种方式在写作、翻译、代码生成等场景下表现不错但在数学推理中有一个严重问题没有反馈信号。人类数学家在做证明时每推进一步都会自我检查这个条件用到了吗这个推导是否有反例中间步骤是否跳过了必要限制这种自我检查不需要外部系统也能部分完成。但大模型在训练时没有经过这种自我验证的强化它只会顺着概率生成下去即使生成到某一步已经错了也可能继续沿着错误方向推进。要让大模型在数学任务上表现得更可靠不能只靠换一个更大的模型而要在系统设计上增加外部验证器。把“模型输出”从终点变成中间产物让验证器去检查、纠错再把错误信息反馈给模型进行二次生成。这就是 AI Agent 开发中常见的“生成—评估—反思”循环。4.2 一个可靠的闭环设计我们设计的数学猜想验证工具采用以下闭环流程用户输入一个数学命题例如“对所有正整数 nn^2n41 都是素数”。大模型生成一组解题思路或证明方向。程序调用验证器对命题进行穷举、符号推演或反例搜索。如果验证器发现反例把反例信息作为上下文反馈给大模型。大模型基于反例信息进行反思输出修正后的结论。最终输出包括模型初始思路、验证结果、反思结论。这个流程的核心思想是不要信任大模型的结论只信任验证器验证过的结论。验证器可以是程序化的穷举检查也可以是符号计算系统甚至可以是一个人工审核步骤。无论形式如何它一定要提供独立的、可靠的反馈信号。4.3 提示词设计思路在这个系统中提示词设计直接决定模型生成质量。我们需要设计两类提示词初始思路生成提示词以及反思修正提示词。初始思路生成提示词的关键是让模型输出“思考过程”而不是直接给结论。这样可以保留更多中间信息供验证和反思。反思提示词则需要把反例信息完整地提供给模型并明确要求它找出自己的错误假设。我们可以在实际代码中体现这个设计。后面小节会给出完整实现。5. 完整实战设计一个数学猜想验证与思路诊断工具5.1 创建项目结构先创建项目文件逐步填充代码。项目目录结构在第 3.3 节已经给出。我们先写requirements.txtrequests2.31.0 sympy1.12接着写config.py代码在 3.2 节已经给出。这里不再重复。5.2 封装大模型调用llm_client.py负责与大模型交互。这里使用requests直接请求 OpenAI 兼容的/chat/completions接口避免引入额外的 SDK 依赖。# llm_client.py import requests import config def chat(messages, temperature0.3, max_tokens1024): 调用 OpenAI 兼容接口。 messages 格式示例 [ {role: system, content: 你是一个数学助手。}, {role: user, content: 请证明n的三次方减n能被6整除。} ] url f{config.BASE_URL}/chat/completions headers { Authorization: fBearer {config.API_KEY}, Content-Type: application/json, } payload { model: config.MODEL_NAME, messages: messages, temperature: temperature, max_tokens: max_tokens, } response requests.post(url, headersheaders, jsonpayload, timeout60) response.raise_for_status() data response.json() return data[choices][0][message][content]这里有几个设计要点。第一temperature设置为 0.3是为了在数学任务中保持输出相对稳定减少随机性如果你希望模型生成更多发散候选思路可以适当调高到 0.7 左右。第二timeout60防止模型响应过慢导致程序卡死。第三这个函数完全独立于具体模型服务只要对方兼容/chat/completions接口就能使用。5.3 编写反例验证器verifier.py是整个项目中最关键的模块。它负责对数学命题做独立的程序化验证。我们实现两个经典命题第一个命题是“对于任意正整数 nn^3-n 能被 6 整除”。这个命题是正确的我们可以用穷举验证也可以让模型给出证明思路。第二个命题是“对于任意正整数 nn^2n41 都是素数”。这个命题在 n 取较小值时看起来成立但在 n40 时会失效因为 40^24041168141^2。这是一个非常经典的“看起来对但实际不对”的例子非常适合用来展示“验证闭环”的价值。# verifier.py from sympy import isprime def check_n3_minus_n_divisible_by_6(limit10000): 验证命题对于所有 1 n limitn^3 - n 是否能被 6 整除。 返回 (是否通过, 反例或None) for n in range(1, limit 1): if (n ** 3 - n) % 6 ! 0: return False, n return True, None def check_n2_plus_n_plus_41_is_prime(limit10000): 验证命题对于所有 1 n limitn^2 n 41 是否为素数。 返回 (是否通过, 反例或None) for n in range(1, limit 1): val n ** 2 n 41 if not isprime(val): return False, n return True, None这里的isprime来自sympy是确定性的素数判定函数比自己在循环里试除要可靠得多。每个验证函数都返回两个值是否通过以及反例。这样主流程可以很方便地把反例信息反馈给模型。在实际项目中验证器不一定是纯穷举。对于更复杂的命题可以接入符号积分、矩阵运算、约束求解器等工具。核心原则是验证器必须独立于大模型必须能给出确定性的判断结果。5.4 编写主流程pipeline.py是主流程文件把大模型生成和验证器结合起来。流程如下用户输入命题描述。调用大模型生成初始思路。调用对应的验证器检查命题。如果发现反例将反例信息拼接到提示词中让模型反思并修正。输出最终结果。# pipeline.py import llm_client import verifier SYSTEM_PROMPT 你是一位严谨的数学思维教练。请给出推理过程和结论并明确指出你使用了哪些假设。 def generate_initial_thought(problem): messages [ {role: system, content: SYSTEM_PROMPT}, {role: user, content: f请分析以下数学命题是否成立并给出理由\n{problem}}, ] return llm_client.chat(messages) def generate_reflection(problem, initial_thought, counterexample): messages [ {role: system, content: SYSTEM_PROMPT}, {role: user, content: f请分析以下数学命题是否成立\n{problem}}, {role: assistant, content: initial_thought}, { role: user, content: f你的上述分析可能有误。程序找到了一个反例n{counterexample} 时命题不成立。 f请检查你的分析过程指出错误原因并重新给出结论。, }, ] return llm_client.chat(messages) def run_pipeline(problem, verifier_func, problem_key): print( * 60) print(数学命题, problem) print( * 60) # 第一步生成初始思路 print(\n[1/4] 大模型生成初始思路中 ...) initial_thought generate_initial_thought(problem) print(模型思路) print(initial_thought) # 第二步验证器检查 print(\n[2/4] 程序验证中 ...) passed, counterexample verifier_func() if passed: print(验证结论在验证范围内未发现反例命题通过程序检查。) print(\n[3/4] 无需反思直接结束。) print([4/4] 完成。) return print(f验证结论发现反例 n {counterexample}命题不成立。) # 第三步反思修正 print(\n[3/4] 将反例反馈给模型请求反思 ...) reflection generate_reflection(problem, initial_thought, counterexample) print(模型反思) print(reflection) # 第四步输出结果 print(\n[4/4] 完成。最终结论以验证器为准。) print(f反例n {counterexample}) if __name__ __main__: problem1 对于所有正整数 nn 的三次方减 n 能被 6 整除。 problem2 对于所有正整数 nn 的平方加 n 加 41 都是素数。 print(示例一正确命题) run_pipeline(problem1, verifier.check_n3_minus_n_divisible_by_6, p1) print(\n\n示例二存在反例的命题) run_pipeline(problem2, verifier.check_n2_plus_n_plus_41_is_prime, p2)这个主流程把整个“生成—验证—反思”的 AI Agent 闭环串起来了。运行之后你会看到模型对第二个命题初始可能给出“这个表达式由欧拉发现前很多项都是素数”之类的分析但程序验证直接找到 n40 这个反例并触发模型反思。这个对比非常直观地展示了“AI 思路”和“数学事实”之间的差距。5.5 运行与结果演示在项目根目录下运行python pipeline.py预期输出大致如下实际内容取决于你使用的模型 数学命题 对于所有正整数 nn 的三次方减 n 能被 6 整除。 [1/4] 大模型生成初始思路中 ... 模型思路 可以将 n^3 - n 分解为 n(n-1)(n1)这是三个连续整数之积。 三个连续整数中必有一个能被 3 整除至少有一个能被 2 整除 所以它们的乘积能被 6 整除。 [2/4] 程序验证中 ... 验证结论在验证范围内未发现反例命题通过程序检查。 [3/4] 无需反思直接结束。 [4/4] 完成。 数学命题 对于所有正整数 nn 的平方加 n 加 41 都是素数。 [1/4] 大模型生成初始思路中 ... 模型思路 这个多项式在 n0 到 39 时都给出素数看起来很可能对所有正整数成立。 但需要进一步证明。 [2/4] 程序验证中 ... 验证结论发现反例 n 40命题不成立。 [3/4] 将反例反馈给模型请求反思 ... 模型反思 我之前的分析过于依赖局部观察。虽然 n0 到 39 都成立 但当 n40 时40^24041168141^2不是素数。 这说明一个命题不能通过有限个例子来证明。 [4/4] 完成。最终结论以验证器为准。 反例n 40这个输出很好地展示了整个系统的价值大模型负责生成人类可读的思路程序验证器负责给出确定性结论反例信息再反馈给模型促成反思。你还想继续深挖的话可以在这个基础上增加更多的验证器例如不等式验证、数值积分验证、方程求解验证甚至接入形式化证明工具。6. 常见问题与排查思路在跑这个项目或者扩展类似 AI Agent 应用时你可能会遇到一些问题。下面按照常见程度做一个汇总。问题现象常见原因解决思路调用大模型接口超时模型较大或网络延迟较高增大timeout参数改用流式请求使用本地模型返回内容被截断max_tokens设置太小调大max_tokens例如 2048 或 4096模型输出大量无关内容提示词没有限定输出格式在 System Prompt 中要求结构化输出穷举验证范围过大数据量太大单线程循环太慢使用numpy向量化计算或只验证关键边界区间模型反复坚持错误答案反例信息在上下文中不够醒目把反例放在 Prompt 末尾并使用加粗或强调格式sympy.isprime对大数很慢大素数判定本身计算量较大缩小验证范围或先用概率性素数判定方法更换云厂商后鉴权失败API_KEY或接口路径不正确检查服务商的接口文档确认/chat/completions路径本地 Ollama 无法连接服务未启动或端口不对确认 Ollama 服务已启动检查BASE_URL是否指向 11434如果模型在反思之后仍然给出错误结论不要感到奇怪。这不是代码 bug而是反映了大模型在某些数学推理任务上的真实局限。此时验证器的“一票否决权”就显得格外重要。在实际 AI 工程实践中我们应该始终把验证器作为最终裁判把大模型作为辅助生成器。另外提醒一点如果你把这类工具用于生产环境比如接入自动化解题系统、数学教育平台一定要对验证器的覆盖范围做充分测试。穷举验证只能证明“在验证范围内成立”不能证明“对所有情况成立”。对于需要严格证明的场景建议接入符号计算系统或人审流程。7. 最佳实践与工程建议7.1 把数学思维迁移到软件开发陶哲轩谈到的数学思维其实可以直接映射到软件开发中。提问能力对应需求分析中的“识别真正的问题”类比迁移能力对应设计模式复用构造反例的能力对应测试用例设计审美判断对应代码重构和架构设计。很多开发者写代码时习惯“先写了再说”遇到 bug 再慢慢调试。这就像不做验证就直接让大模型输出答案。更好的做法是先构造反例这个函数的边界条件是什么如果输入为空、为最大值、为 None会发生什么把这些反例前置到编码阶段能显著降低返工率。我在工程实践中发现数学思维好的开发者在排查线上问题时往往会先问“这个假设在什么情况下不成立”而不是急于翻日志。这种习惯本质上就是数学中的“反例思维”。如果你想提升自己的编程能力可以从刻意练习“给自己挑错”开始。7.2 使用 AI 学习数学思维的正确姿势既然大模型在数学推理上需要验证闭环那我们普通人使用 AI 学习数学时也应该建立这个闭环。不要把大模型当成答案机器而是当成“可以对话的思维陪练”。一个推荐的做法是拿到一个数学问题后先自己尝试提出猜想再让大模型给你多个证明方向然后用计算工具去验证最后把验证结果反馈给大模型让它反思。这个过程不是“用 AI 抄答案”而是“用 AI 做演练”。长期坚持下来你训练的是自己的提问能力、反例敏感度和验证意识而不只是记住某个题的解法。在 AI Agent 开发的语境下这也意味着好的 AI 应用不应该只是“Prompt 包装”而应该包含工具调用、验证反馈、自我反思等模块。当前的 AI Agent 框架已经支持这类设计但核心思路仍然是那条让模型生成让工具验证让反馈闭环。7.3 面向 AI 工程的生产建议如果你准备把类似“AI 数学验证”的方案落地到生产中有几点建议。第一把验证器设计成可插拔的模块。不同的数学问题需要不同的验证工具建议定义统一的验证接口方便后续扩展。第二日志要记录模型的原始输出、验证器结果、反例信息以及反思输出。这些日志既可以用于调试也可以用于构建测试集来评估模型效果。第三对模型输出做内容安全过滤。尤其是面向教育场景时要避免模型输出包含不当内容。第四注意模型幻觉对用户体验的影响。如果产品面向普通用户建议在 UI 上区分“AI 生成内容”和“程序验证结果”避免用户混淆。安全方面要特别提醒在使用大模型 API 时不要在 Prompt 中提交敏感个人信息在生产环境中为 API Key 配置最小权限任何涉及自动执行代码的功能都要放在沙箱环境中运行并经过严格的合法授权。8. 总结与下一步学习路线本文从陶哲轩关于 AI 与数学思维的讨论切入拆解了 AI 在数学推理上的能力边界并设计了一个可运行的“数学猜想验证与思路诊断工具”。在这个小项目中大模型负责生成解题思路程序验证器负责检查命题真伪反例信息被反馈给模型进行反思。这个过程还原了人类数学家“猜想—验证—修正”的思维闭环也展示了 AI Agent 开发中的经典模式。如果你对下一步学习方向感兴趣可以沿着三个方向继续深入。第一学习符号计算与形式化验证。sympy只是起点更深入的方向包括 Coq、Lean、Isabelle 等证明助手。这些工具能让 AI 的推理过程被机器严格校验也是目前 AI 数学研究的前沿方向之一。第二学习 AI Agent 开发框架。把本文的“生成—验证—反思”循环用 LangChain、LlamaIndex 等框架重写并加入记忆、工具调用、多步规划能力就是一个功能更完整的 AI Agent 应用。重点仍然是保持“验证器独立、反馈闭环”的设计原则。第三练习构造反例。你可以从经典数学问题开始比如欧拉多项式、连续但不可导的函数、满足一定条件的反常积分等尝试自己构造反例再把这些反例做成上述工具的新验证器让模型在反思时面对更丰富的素材。这个过程既训练数学思维也锻炼工程实现能力。如果本文对你理解 AI 与数学思维的关系有帮助可以收藏备用。也欢迎你根据自己的项目场景把验证闭环的思路应用到代码生成、数据分析、自动化测试等更多 AI 工程实践中。