数学证明验证工具链：公式OCR、SymPy与大模型推理实战

最近有个标题挺抓眼球：“困扰数学圈22年的难题，居然被协和实习医生解决了？”

先说明一下，本文不打算跟进这个热点本身，也不讨论新闻真假。作为一个搞技术的，看到这类标题时，第一反应其实是另外几个问题：这个难题到底是什么？证明过程能不能提取出来？里面的公式和推导能不能用工具去验证？如果我想复现一遍、把证明拆解成可检查的步骤，应该用什么技术栈？

这篇文章就围绕这件事展开。我会给出一套完整的技术验证思路，覆盖数学公式提取、符号计算验证、大模型辅助推理、工作流批处理和本地部署，整套流程能用 Python 跑通，也能接 API 做批量任务。不管你是做算法、做后端，还是单纯对数学工具链感兴趣，这套环境都能直接上手。

1. 核心能力速览

这套流程里，最关键的三件事是：把图片和 PDF 里的公式变成结构化文本，用符号计算引擎做确定性验证，再用大模型做开放式的思路分析。下面分别展开。

2. 为什么技术手段能介入这类数学新闻

数学难题的新闻传播有一个特点：结论很容易被浓缩成一句话，但证明过程往往藏在论文附件或 PDF 里。普通人看到标题只能记住“解决了”，技术人却可以做得更多。

数学证明本质上是一个形式化对象。只要能把证明里的关键步骤转成机器可读的符号表达式，就能用符号计算工具逐步检查等式是否成立、不等式是否严格、推导是否有跳步。这是计算机辅助验证能参与的领域，也是这套工具链能落地的原因。

但要注意边界。目前的符号计算工具还无法自动验证一整篇论文的全部逻辑，尤其是涉及构造性证明、数论估计、复杂不等式放缩时，机器只能检查局部。更合理的定位是：用工具加速阅读、辅助复算、标记可疑步骤，而不是替代数学家的判断。

另外，围绕数学新闻做技术验证，也必须遵守版权和学术规范。论文内容不能随意转载，公式提取只用于个人学习复现，引用时要标注来源。

3. 环境准备与前置条件

整个工具链建议分成三个独立环节，每个环节都有对应的工具包。

3.1 基础环境

建议用 conda 或者 venv 创建独立环境，避免依赖冲突。

# 以 venv 为例 python -m venv math_verify_env source math_verify_env/bin/activate # Windows 用 math_verify_env\Scripts\activate

3.2 各环节工具清单

公式提取环节，推荐开源方案 LaTeX-OCR，也就是 pix2tex 项目，它能把公式图片直接转换成 LaTeX 代码。如果想处理 PDF，可以配合 PyMuPDF 把 PDF 页面转成图片，再走 OCR 流程。数学公式 OCR 对 GPU 要求很低，CPU 也能跑。

符号计算环节，使用 SymPy，这是 Python 生态里最成熟的符号计算库，支持微积分、方程求解、矩阵运算、级数展开、不等式简化。更重的计算可以使用 SageMath，但安装体积大，配置成本高，一般场景 SymPy 足够。

大模型辅助推理环节，可以本地部署量化版的开源数学推理模型，也可以直接调用商用 API。本地部署需要根据显存选择模型版本，8G 显存可以选择较小规模模型，实际占用以运行日志为准。如果机器配置不够，优先使用 API。

4. 公式提取：把论文里的数学内容变成 LaTeX

数学证明的第一步是提取公式。直接从 PDF 复制经常会出现乱码，特别是双栏排版、特殊符号和矩阵环境。最稳定的是先把页面转成高分辨率图片，再做公式 OCR，最后人工校对。

4.1 安装公式 OCR 工具

这里以 LaTeX-OCR 为例。

pip install pix2tex[gui]

安装完成后，可以启动 GUI 版本，也可以直接用 Python API。

from PIL import Image from pix2tex.cli import LatexOCR model = LatexOCR() image = Image.open("formula_sample.png") latex_code = model(image) print(latex_code)

4.2 从 PDF 批量提取公式

真实场景里，论文通常是 PDF 页面。可以通过 PyMuPDF 把指定区域转成图片，再交给 OCR 模型。但更实用的是先整页转图，再人工截取需要验证的公式区域。

import fitz doc = fitz.open("paper.pdf") page = doc[0] # 设置缩放比例，高分辨率可以提高 OCR 准确率 mat = fitz.Matrix(2.0, 2.0) pix = page.get_pixmap(matrix=mat) pix.save("page_0.png")

OCR 模型对清晰度很敏感。分辨率低于 150 DPI 时，复杂分数的识别准确率会明显下降。工程上建议用 2 倍缩放导出，然后做一次对比度增强。

4.3 判断公式提取是否成功

提取结果不是看“看起来像不像”，而是看能不能被后续的 LaTeX 解析器正确编译成符号表达式。建议用 pylatexenc 做基础语法检查。

pip install pylatexenc

from pylatexenc.latex2text import LatexNodes2Text lat = LatexNodes2Text().latex_to_text print(lat(r"\frac{a}{b} + \sqrt{c}"))

如果这一步能输出正常文本，说明公式基本规范，可以进入符号计算环节。

5. 符号计算：用 SymPy 验证关键推导

公式提取只是预处理，真正有价值的是验证。我们来看一个例子：假设论文结论里的关键不等式是 a(x) >= b(x)，其中 a(x) 和 b(x) 有明确的表达式，就可以用 SymPy 做符号化简和差式恒正判断。

5.1 安装和基础用法

pip install sympy

import sympy as sp x = sp.symbols("x", positive=True) a = sp.sqrt(x**2 + 1) b = sp.log(x + 2) + 1 diff_expr = sp.simplify(a - b) print(diff_expr)

这里只是一个示例。实际验证时，需要把论文里的中间表达式逐段手动输入，然后让 SymPy 化简、展开、求导或求极限，检查每一步是否和原文一致。

5.2 典型验证操作

5.3 设计可重复的验证脚本

建议把每个验证步骤写成独立函数，输出“通过 / 不通过 / 无法自动判断”三种结果。

import sympy as sp x = sp.symbols("x", positive=True) def verify_identity(lhs, rhs): diff = sp.simplify(lhs - rhs) if diff == 0: return "PASS" return "FAIL" lhs = sp.expand((x + 1) * (x - 1)) rhs = x**2 - 1 print(verify_identity(lhs, rhs))

对于“无法自动判断”的情况，可以再用数值抽样辅助判断。比如在定义域内随机取 1000 个点，比较两端数值差是否都接近 0，虽然不能证明，但能快速发现问题。

6. 大模型辅助推理：让 AI 解释和检查证明脉络

公式验证解决的是“这一步算得对不对”，而大模型解决的是“作者这一步为什么要这样做、前后逻辑是否通顺”。在解析数学新闻的热点难题时，这一步相当有用。

6.1 两种接入方式

第一种是调用商用 API，成本低、速度快、不占本机显存，但对论文内容存在数据外发风险，不能传未公开成果。

第二种是本地部署开源数学推理模型，隐私性好，可以离线使用，但需要准备模型文件和推理环境。

# 本地部署示例，实际命令以对应模型的官方文档为准 pip install vllm

启动本地 OpenAI 兼容服务时，端口和模型名需要按实际环境替换。

# 伪代码示例，需要替换为实际模型路径和端口 python -m vllm.entrypoints.openai.api_server \ --model /path/to/your/model \ --port 8000

然后就能用标准的 OpenAI SDK 调用本地服务。

from openai import OpenAI client = OpenAI(base_url="http://127.0.0.1:8000/v1", api_key="EMPTY") resp = client.chat.completions.create( model="your-model-name", messages=[ {"role": "user", "content": "请解释这个不等式放缩的关键思路："} ] ) print(resp.choices[0].message.content)

6.2 结构化提问模板

大模型对数学问题的回答质量很依赖提问方式。推荐使用下面这套模板：

【任务】 你是一名数学审稿人。请检查下面这段证明步骤是否有逻辑跳跃。 【证明步骤】 （粘贴提取出来的文字） 【要求】 1. 指出最关键的一步。 2. 列出可能需要补充证据的地方。 3. 如果有疑似错误，给出你的理由。 4. 结论只输出“基本可靠 / 存在疑点 / 推断不充分”。

6.3 关注生成结果的一致性

大模型回答要重复多次做一致性检查。同一个问题跑三次，如果三次结论明显冲突，说明模型本身不稳定，不能作为依据。工程上可以在提示词里要求模型输出完整的推理链，再做结果文件比对，更容易发现矛盾。

7. 完整工作流编排与批量任务

单条验证很轻松，但数学论文动辄几十页，公式几十个，必须批量处理。建议把整个流程拆成四个阶段：输入采集、公式提取、逐项验证、结果汇总。

7.1 目录结构

math_verify/ ├── input/ # 原始 PDF 和图片 ├── pages/ # PDF 转出的页面图片 ├── formulas/ # 裁剪出的公式图片 ├── latex/ # OCR 生成的 LaTeX 文本 ├── results/ # 验证结果 JSON/Markdown ├── scripts/ │ ├── pdf2img.py │ ├── formula_ocr.py │ ├── sympy_verify.py │ └── batch_run.py └── logs/

7.2 批量处理脚本示例

用 Python 的concurrent.futures做简单并发，避免过度设计。

from concurrent.futures import ThreadPoolExecutor from pathlib import Path def process_one(formula_file: Path): # 这里替换成实际的 OCR + 验证逻辑 result = {"file": formula_file.name, "status": "ok"} return result formula_dir = Path("./formulas") with ThreadPoolExecutor(max_workers=4) as executor: results = list(executor.map(process_one, formula_dir.glob("*.png"))) print(results)

如果任务量超过几千条，可以引入消息队列，比如 Redis + RQ 或者 Celery。但数学验证场景多数是几十到几百条，文件队列加日志就够用。

7.3 输出结果设计

建议使用 JSONL 保存每条记录，方便后续排查。

{ "input_file": "formula_001.png", "latex": "\\frac{a}{b}", "verification": "PASS", "duration_s": 1.2, "error": null }

批量任务必须加失败重试和断点续跑能力。最简单的方式是处理前先检查输出文件是否存在，已经成功的跳过，避免重复计算。

8. 资源占用与性能观察

整套工具链里，资源占用差异很大。公式 OCR 和 SymPy 都是轻量计算，普通办公本就能跑，显存占用几乎可以忽略。真正吃资源的是本地大模型推理。

如果使用本地大模型，显存占用需要用nvidia-smi持续观察。

watch -n 1 nvidia-smi

当模型加载完成后，显存占用会达到一个稳定值。推理过程中如果出现频繁的显存溢出，可以降低最大输入长度、改用量化版本模型、缩小 batch size，或者干脆切换为 API 调用。

CPU 推理不是不能用，但单次生成速度会慢很多。数学推理任务往往需要长输出，体验差距尤其明显。更稳妥的顺序是：先跑通 CPU 小模型确认流程，再换 GPU 大模型提升质量。

批量任务建议一次不要跑满整机资源。给 OCR 预留一个线程池上限，给大模型推理限制并发数，避免内存被挤爆导致进程崩溃。日志里必须记录每个文件的耗时，方便定位卡死的任务。

9. 接口 API 调用示例

如果要把这套验证能力接到现有系统里，可以封装一个本地 API。用 FastAPI 是最快的方式。

9.1 定义接口

from fastapi import FastAPI, File, UploadFile from PIL import Image import io app = FastAPI() @app.post("/api/ocr") async def ocr_formula(file: UploadFile = File(...)): image_data = await file.read() image = Image.open(io.BytesIO(image_data)) # 调用 OCR 模型，这里省略具体实现 return {"latex": r"\frac{a}{b}", "status": "ok"}

启动服务：

uvicorn ocr_api:app --host 127.0.0.1 --port 8000

9.2 批量上传调用

import requests files = [("files", ("f1.png", open("./formulas/f1.png", "rb"), "image/png"))] resp = requests.post("http://127.0.0.1:8000/api/batch_ocr", files=files, timeout=60) print(resp.json())

需要注意，接口服务需要控制访问范围。不要在公网裸奔启动，建议只监听127.0.0.1，或者加一层简单的访问令牌。对于包含未公开论文内容的请求，还要考虑数据安全问题。

10. 常见问题与排查方法

依赖安装失败也很常见，优先换 pip 镜像源，再根据报错信息补装系统依赖。另外，模型文件的损坏会导致启动崩溃，下载完成后建议比对官方 checksum。

11. 最佳实践与合规边界

工程上建议先跑通一个最小流程，不要一开始就追求全自动。从一张干净的公式图片开始，确认 OCR 能识别、SymPy 能验证、输出能保存，再扩大范围到整个 PDF。

目录管理要规范。输入素材、中间图片、OCR 文本、验证结果分开存放，不要在根目录堆文件。批量任务必须有日志和失败重试，日志里记录输入文件、输出结果、耗时和错误信息。

大模型只是辅助工具，不能把它的回答当作最终结论。关键步骤要以 SymPy 等确定性工具的结果为准。涉及数学史、人物背景、未公开论文、他人研究成果时，更要注意信息来源的合法性和引用授权。不能把未经证实的传闻当作技术结论传播。

关于人脸、声音、图片素材这些扩展能力，本文没有涉及，但如果后续把公式 OCR 技术平移到文档识别、票证识别、试卷批改等场景，依然要遵守隐私和数据合规要求，对个人敏感信息先做脱敏。任何人脸、声音相关的功能都必须取得明确授权后才能使用，这是底线。

12. 总结与下一步

回到开头那个标题。对技术人来说，值不值得关注这件事的关键，不是“谁解决了”，而是“证明过程能不能被机器辅助验证”。本文给的这套工具链，把公式 OCR、SymPy 符号计算、本地大模型推理和批量任务编排串在一起，可以覆盖大部分数学证明复现的场景。

最先应该跑通的是 SymPy 那一步，成本最低，效果最确定。接着可以尝试把一篇论文里的关键公式转成 LaTeX，做一次小范围验证。最容易踩的坑也最容易被忽略：OCR 输出看着合理，但到 SymPy 里一化简就发现根本不成立，所以每一步都要和原文反复比对，不能盲目相信中间结果。

后续可以继续扩展的方向有几个，一是把 LaTeX 结果接到形式化验证工具里，比如 Lean 或 Isabelle，做更严格的推导检查；二是接入自动化论文解析摘要服务，把整篇 PDF 变成结构化的验证清单；三是把接口封装成内部工具，方便团队共用。

数学难题的新闻可能会不断出现，但这套验证流程是通用的。建议把本文的命令和脚本模板先存一份，遇到公式密集的资料时，直接套用流程，能省不少时间。