企业官网建设流程全解析

哈萨比斯预告了人工智能在数学领域的下一场突破：用AI生成高难度数学猜想，把人类数学家的作用从“发现”推向“验证”。这篇文章从AlphaProof、AlphaGeometry等系统的技术路径讲起，分析为什么数学是最适合AI的“封闭测试场”，以及为什么说“第37手”只是时间问题。不吹不黑，适合关心AI4Science、数学AI和大模型推理能力上限的技术读者阅读。

哈萨比斯预告：数学的AI“第37手”只剩时间问题

最近DeepMind的哈萨比斯又放了一句话：数学领域会诞生属于AI的“第37手”。这个说法借用了围棋里“第37手”的典故——AlphaGo在2016年人机大战第37手落子，在当时几乎没人预料到，事后却被证明是一手开天辟地的好棋。哈萨比斯的言下之意很清楚：数学研究中，AI也能下出类似的“非人类”妙手，而且这个时刻已经不远了。

如果你关心AI4Science、大模型推理能力、或数学AI的工程化落地，这篇文章比较值得读完。我们不只聊口号，而是把AlphaProof、AlphaGeometry这些系统的技术路径拆开看，分析它们为什么能解决数学问题、如何落地复现、在普通GPU上能跑到什么程度、以及“AI数学家”还有哪些硬边界。

1. 核心能力速览

从这张表能看到一个关键点：所谓的“AI数学突破”并不是一个端到端的魔术，而是一条标准流水线——生成候选、符号验证、反馈迭代。这跟市面上的AI编程工具思路很像，只是验证器从编译器换成了数学证明系统。

2. 为什么数学是AI最容易突破的领域

数学一直被看作人类智力的最高象征，但站在机器学习角度，它反而是最“友好”的测试场。

2.1 数学具备完整自动验证器

围棋能成为AI突破口，是因为规则明确、胜负可判。数学更极端：一个定理，只要给出严格形式化证明，机器就可以自动验证。Lean、Coq、Isabelle这些证明助手已经把“验证”这件事变成了可计算的过程。AI不需要“主观作答”，只需要生成一连串证明步骤，剩下的交给验证器判定正误。

2.2 试错成本极低

物理实验要花钱，化学实验要耗材，医学试验要伦理审批。数学推演纯粹是符号和逻辑操作，错了就从头再来，成本几乎为零。这让强化学习有了极好的训练环境：AI可以自己和自己对弈，生成无数候选证明，保留成功的，丢弃失败的。

2.3 结果有客观边界，没有“差不多”

AI写作文、画图、生成视频，好坏很难量化。但数学证明就两种状态：证出来了，或者没证出来。这种二元反馈让模型训练变得干净利索，不需要人工标注好坏，只需要验证器给出对错。

2.4 搜索空间虽大但有结构

数学难题本质上是组合爆炸的搜索问题，但数学结构里有大量可用的剪枝信息。AlphaGeometry能解奥数几何题，核心不是暴力搜索，而是让语言模型学习“辅助点应该加在哪里”，把搜索空间压缩到可计算范围。只要找到关键构造，后面的证明路径往往会自然展开。

3. 核心技术拆解：AlphaProof、AlphaGeometry、FunSearch

3.1 AlphaProof：形式数学与强化学习的结合

AlphaProof是DeepMind在IMO 2024中交出的一份答卷。它把大语言模型生成的候选证明步骤接入Lean证明器，让模型不断尝试、不断被验证器纠错，再用强化学习提升成功率。整个系统更像“推理模型 + 编译器”的闭环，而不是一个单纯的对话式大模型。

它做到的成就是在IMO 2024真题中解决了4道题，达到银牌水平。虽然离满分还有距离，但这个结果对“AI主动提出新数学”来说已经是一个重要信号。

3.2 AlphaGeometry：把几何题转成可搜索的推理树

AlphaGeometry是专攻欧几里得几何的系统。传统几何题的难点在于辅助线、辅助点怎么找。AlphaGeometry的做法是：先用大语言模型（或预训练网络）生成辅助构造，再用符号推理引擎（类似DG解算器）检查这些构造是否通向证明。

它的关键洞察在于，符号引擎负责穷举推导，神经网络负责提出“有希望”的辅助点。前者严谨但迟钝，后者灵活但粗放，二者结合以后，它第一次在IMO几何题上达到了接近人类金牌选手的表现。

需要注意一点：这套系统并不像ChatGPT那样能和你谈笑风生。你输入一道几何题，它返回的是一棵证明树，而不是一段自然语言解答。这也正是数学AI和普通AI助手的本质区别。

3.3 FunSearch：把代码当数学猜想，用LLM搜索

FunSearch的思路更有意思：它不直接搜索数学公式，而是让LLM编写一个能生成数学候选结果的程序，再由程序自动运行打分，把分数反馈给LLM，继续迭代。这个方案在面对“极值问题”时表现很好，比如上限集问题、装箱问题。

本质上，FunSearch把“数学发现”转成了“程序合成 + 进化搜索”。这也是目前可复现性最高的一类方法，因为它不依赖专门的证明器，只依赖一个能写代码的LLM和一个打分函数。

3.4 AlphaTensor：从算法层面刷新矩阵乘法

AlphaTensor解决的不是证明题，而是计算复杂度问题。它把一个“如何用更少乘法完成矩阵相乘”的问题建模为单玩家游戏，然后使用强化学习去搜索更优的矩阵乘法分解。结果是它发现了比经典Strassen算法更优的小矩阵乘法方案，直接推动算法发现进入自动化时代。

从这些系统可以看出，数学AI并不是单一模型，而是一整套“模型 + 验证器 + 搜索策略”的组合。对工程团队来说，真正的门槛往往不在深度学习本身，而在于如何把数学规则转化成一个可计算、可反馈的闭环系统。

4. 本地复现思路：用开源LLM搭一个“数学AI流水线”

DeepMind的完整系统没有开源，但这不代表我们只能围观。用开源大模型也可以搭一条类似“生成-验证-迭代”的数学AI流水线，在本地GPU上做实验。

4.1 环境准备与硬件建议

先看硬件。推荐配置如下，实际以本机为准：

相比文生图、视频生成等任务，数学推理模型对显存的要求并不算极端。以DeepSeek-R1系列为例，7B量级的模型在8GB显存上可以跑通，671B满血版则需要多卡或量化部署。数学任务的瓶颈往往不是“生成答案”，而是“验证答案”，所以就算没有顶级GPU，也可以用CPU跑Lean验证器。

4.2 推荐开源模型

目前适合数学推理的模型主要有这几类：

需要注意，模型只能“提出步骤”，判断对错必须交给验证器。没有验证器的LLM数学对话，本质上只是“看起来合理的文字”。

4.3 部署一个可用于数学实验的推理服务

下面给出一套本地推理服务的通用启动方式，适用于绝大多数Ollama可运行的模型。

# 安装Ollama（Linux/macOS） curl -fsSL https://ollama.com/install.sh | sh # 拉取DeepSeek R1 7B量化版 ollama pull deepseek-r1:7b # 启动服务 ollama serve

启动后，Ollama默认监听11434端口。可以用Python调用：

import requests url = "http://127.0.0.1:11434/api/generate" payload = { "model": "deepseek-r1:7b", "prompt": "请用自然语言证明：存在无穷多个质数。", "stream": False } resp = requests.post(url, json=payload, timeout=120) print(resp.json()["response"])

这只是一个对话框服务，离AlphaProof还有距离。但它是所有数学AI实验的地基：没有生成器，后面的一切无从谈起。

5. 搭建“生成-验证-迭代”闭环：数学AI最小可运行示例

5.1 整体架构

一条最简数学AI流水线可以用三个模块表示：

• 生成器：LLM产出一个候选命题或候选证明步骤。
• 验证器：符号系统检查该候选是否成立。
• 迭代器：如果验证失败，把错误信息反馈给LLM，重新生成。

以“数值数学猜想发现”为例，我们可以让LLM提出一个整数序列的递推关系，然后用Python验证前N项是否成立。

5.2 示例：让LLM提出递推公式并用Python验证

import requests import sympy as sp def generate_candidate(sequence): prompt = f""" 给定整数序列前6项：{sequence} 请提出一个可能的递推公式或通项公式。 只输出公式，不要解释。 """ resp = requests.post( "http://127.0.0.1:11434/api/generate", json={"model": "deepseek-r1:7b", "prompt": prompt, "stream": False}, timeout=120 ) return resp.json()["response"].strip() seq = [1, 1, 2, 3, 5, 8, 13, 21] candidate = generate_candidate(seq) print("LLM候选公式:", candidate)

5.3 实现验证器并自动反馈

def validate(seq, formula_expr): n = sp.symbols("n") try: expr = sp.sympify(formula_expr) for i, val in enumerate(seq): if sp.simplify(expr.subs(n, i + 1)) != val: return False, f"第{i + 1}项不匹配，期望{val}，得到{expr.subs(n, i + 1)}" return True, "序列前N项验证通过" except Exception as e: return False, f"公式解析错误: {e}" ok, msg = validate(seq, candidate) print("验证结果:", msg)

这就是“AI第37手”的最小工程原型：先生成，再验证，失败就迭代。不要小看这个流程，AlphaProof的日常训练和它本质相同，只是把Python替换成了Lean，把序列公式替换成了定理证明项。

5.4 用Lean做形式化验证

如果想更接近AlphaProof的路线，可以安装Lean证明器，并让LLM直接生成Lean证明代码。

-- 简单验证：自然数加法结合律 theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by induction a with | zero => simp | succ a ih => simp [Nat.add_assoc, ih]

这个代码可以被Lean自动检查。如果LLM生成的不是合法证明，Lean会返回错误信息。把这个错误信息重新注入提示词，就能形成类似AlphaProof的强化学习反馈回路。

6. 接口API与批量任务：把数学AI变成工程服务

6.1 用FastAPI包装推理服务

在本地实验成功后，可以把推理服务封装成HTTP API。通用写法如下：

from fastapi import FastAPI from pydantic import BaseModel import requests app = FastAPI() class ProveRequest(BaseModel): statement: str @app.post("/prove") def prove(req: ProveRequest): ollama_resp = requests.post( "http://127.0.0.1:11434/api/generate", json={ "model": "deepseek-r1:7b", "prompt": f"生成Lean证明代码：{req.statement}", "stream": False }, timeout=300 ) return {"candidate": ollama_resp.json()["response"]}

然后启动服务：

uvicorn api_server:app --host 0.0.0.0 --port 8000

调用：

curl -X POST http://127.0.0.1:8000/prove \ -H "Content-Type: application/json" \ -d '{"statement": "证明：两个偶数之和是偶数。"}'

6.2 批量数学命题验证

批量任务建议用任务队列，简单的做法是先读入命题列表，逐个调用验证器，把结果写入JSONL文件。注意加上超时和失败重试。

import json import requests from tenacity import retry, stop_after_attempt, wait_fixed @retry(stop=stop_after_attempt(3), wait=wait_fixed(2)) def call_llm(prompt): resp = requests.post( "http://127.0.0.1:11434/api/generate", json={"model": "deepseek-r1:7b", "prompt": prompt, "stream": False}, timeout=120 ) return resp.json()["response"] tasks = [ "证明：存在无穷多个质数。", "证明：根号2是无理数。", "证明：所有边相等的三角形是等边三角形。", ] results = [] for task in tasks: try: candidate = call_llm(task) results.append({"task": task, "candidate": candidate, "status": "done"}) except Exception as e: results.append({"task": task, "error": str(e), "status": "failed"}) with open("math_results.jsonl", "w", encoding="utf-8") as f: for item in results: f.write(json.dumps(item, ensure_ascii=False) + "\n")

批量任务的核心原则是：每一条结果都要可追踪、可重试、可审计。数学AI尤其如此，因为生成结果必须和验证结果绑定存储，否则无法判断哪条候选真正有效。

7. 资源占用与性能观察

7.1 显存占用怎么看

运行LLM推理时，可以用nvidia-smi观察显存占用。以7B量化模型为例，在Windows或Linux下，单次生成的显存占用通常在6GB到10GB之间，实际取决于上下文长度和并发数。如果出现CUDA out of memory，优先降低num_ctx或改用更小量化等级。

# 实时查看显存 nvidia-smi -l 1

7.2 生成与验证的瓶颈

数学AI流水线的性能瓶颈往往不是GPU，而是验证器。LLM生成一段候选证明可能只需要几秒，但Lean或符号引擎检查证明可能需要几十秒甚至几分钟。所以在工程上，建议把生成服务和验证服务解耦，用消息队列异步处理。

7.3 如何降低资源占用

• 使用量化模型（q4_k_m、q8_0）。
• 限制输入输出的最大长度。
• 减少并发请求数。
• 验证任务放到CPU，GPU专注生成。
• 批量扫描时，不要把过长的失败历史拼进提示词，否则上下文会越来越长。

8. 常见问题与排查方法

9. 最佳实践与使用建议

在工程上复现“数学AI”这类系统，最容易踩的坑是过度信任LLM生成的自然语言推理。面对数学任务，自然语言证明只是“思路草稿”，真正可靠的做法是让形式化验证器兜底。

建议按下面这套流程推进：

• 先用小模型跑通流水线，再升级大模型。
• 原始命题、LLM生成结果、验证结果、错误日志全部落盘。
• 每个候选结果都记录模型版本、提示词版本和验证器版本。
• 批量任务必须加超时、重试和并发限制。
• 涉及发表论文或公开成果时，必须由数学家复核最终结论，不能直接采纳LLM输出。
• 做数学猜想发现时，把LLM当“思路生成器”，不要当“裁判”。

10. 总结与下一步

哈萨比斯说的“数学第37手”，本质上是说AI会像AlphaGo一样，在人类从没想过的地方给出一个反直觉的数学构造或证明路径。AlphaProof、AlphaGeometry、FunSearch已经证明这条路线可行，但这些系统目前更像“解题机器”，还不是“数学家”。它们能按已有规则搜索和验证，却还谈不上自主设定研究纲领。

对普通技术人来说，这件事离我们并不远。用一台8GB显存的NVIDIA显卡加开源推理模型，就已经能搭出“生成-验证-迭代”的数学AI实验环境。真正的价值不在于让AI解几道奥数题，而在于建立一套可验证的自动化推理流程——这套流程不仅能用于数学，也能迁移到代码验证、合约审计、知识库一致性检查等领域。

下一步如果想深入，可以先从三件事开始：第一，用Lean或Python验证器把你手头的问题形式化；第二，用DeepSeek-R1或Qwen2.5-Math生成候选步骤；第三，把验证失败的错误信息回灌给模型，观察迭代效果。做完这一步，你已经比绝大多数只看新闻的人更接近“AI第37手”的真实工作方式。