16. 数学推理数据怎么合成和验证？为什么数学训练数据这么难做？
整理数学推理数据的合成、验证与过滤思路。
简单回答
数学推理数据难做的核心原因有三个：高质量数学数据天然稀缺（互联网上的数学题大多没有详细推理步骤，或步骤错漏）、人工标注极贵（需要懂数学的人，且每道题要写完整步骤）、错误检测困难（一段推理过程是否正确不能简单 substring 匹配）。主流方案是通过 LLM 大规模合成 + 自动验证：用强模型生成多个解、用最终答案匹配过滤错误的、用过程一致性（多个解殊途同归则更可信）做置信度筛选、再用代码执行（数学题转 Python 跑一遍）或形式化验证（Lean/Coq）做硬验证。DeepSeek-Math、Llemma、Minerva 等模型都在这条路上。
详细解释
为什么数学数据这么难
数学训练数据的稀缺性有几个结构性原因：
互联网数学数据质量参差。MathOverflow、Stack Exchange、教材 PDF 里的数学问题大多只有最终答案没有详细步骤；有详细步骤的（Khan Academy、教科书）规模又有限；学术论文里的数学是高度抽象的、不适合训练基础推理。
符号表示混乱。同一个数学公式可能写成 LaTeX、Unicode、纯文本（"x^2 + 2x + 1"）、图片（PDF 里的扫描）。不同表示之间转换极难，OCR 出来的数学公式错误率惊人。
长链条推理的标注成本。一道高中数学题的完整推理可能要 10-20 步，每一步都要正确。标注一道题就要 10-30 分钟（标注员还得是懂数学的）。靠人工标几万道题就要消耗几百人月。
错误检测困难。一段推理过程的错误可能是隐蔽的——某一步代数变形错了但最终答案恰好对。或者过程对但答案抄写错了。简单的"答案匹配"不能可靠地过滤错误推理。
Out-of-Distribution 问题：训练数据里的题型有限，模型在训练分布外的题上能力急剧下降。要让模型有泛化推理能力需要题型多样化。
主流的合成方案
方案 1：用强模型生成 + 答案过滤
最常见的 pipeline：
- 用一个种子题集（GSM8K、MATH 训练集、各种数学竞赛题）作为起点
- 让一个强 LLM（GPT-4、Claude）对每道题生成 N 个解（temperature 调高保证多样性）
- 对比每个解的最终答案和参考答案（如果题目有标准答案）
- 保留答案正确的解
这种方式的优点是规模化容易、不需要人工标。缺点是答案对不代表过程对——LLM 可能用错误推理碰到正确答案。
方案 2：自一致性过滤（Self-Consistency Filter）
针对方案 1 的"过程错也可能答案对"问题，可以用自一致性做更严格的过滤：
- 对同一道题用模型生成 N 个解（比如 32 或 64 个）
- 看最终答案的分布——如果某个答案出现频率超过阈值（比如 60%）才接受
- 答案一致说明这个题模型有把握、推理过程更可能是对的
代价是采样成本高（每题要 N 次推理）。但对最终数据质量提升明显——MATH 数据集上自一致性过滤后正确率从 70% 提升到 90%+。
方案 3：代码执行验证（Code-as-Verifier）
对计算性数学题（算术、代数、概率），把题目转成 Python 代码执行，用执行结果作为 ground truth：
DeepSeek 在 DeepSeek-Math 中大量用了这个方法。能可靠验证的题型有限（要能转成可执行代码），但对覆盖范围内的题验证可靠性接近 100%。
方案 4：形式化验证（Lean/Coq）
最严格的方案——把数学题和证明翻译成 Lean、Coq、Isabelle 等形式化证明系统的语言，让证明助手验证。任何被验证通过的证明 100% 是正确的。
代表工作：MiniF2F、ProofNet、Llemma、DeepSeek-Prover。这条路适合定理证明类数学（不只是计算），是高端方向。
代价是形式化语言学习曲线陡、覆盖的数学领域有限（很多研究级数学还没形式化）、模型生成形式化证明的能力还很弱。但这是 理论上能彻底解决数学正确性 的方向，长期价值大。
方案 5：从答案反推过程（Reverse Synthesis）
数学竞赛题往往只有题目和最终答案没有过程。可以让 LLM 基于"题目 + 答案"反推一个合理的解题过程：
- Prompt: "已知答案是 X，请写出从题目到答案的详细推理过程"
- LLM 生成 step-by-step 推导
- 自一致性 / 代码验证过滤
这是把"光秃秃的题-答数据"扩展成"题-过程-答"丰富数据的常见做法。
题型扩展（Diverse Generation）
模型只在 GSM8K、MATH 这种特定题型上训练，泛化能力有限。要扩展题型常见做法：
模板变体：用模型对一道题生成"同类型不同数字"的变体——把"小明买 3 个苹果"换成"小红买 5 个梨"，保持解题逻辑不变但表面变化。
难度递进：基于一道简单题让模型生成"在此基础上加一步推理"的进阶题。从一步运算到两步、三步，逐步增加复杂度。
主题迁移：把代数题改写成几何题、把概率题改写成组合题，扩展题型多样性。
反向生成：先确定一个"目标答案 + 推理结构"，再让模型生成对应的题目。比如先定"答案是 42、要用到三步代数运算"，然后让模型生成符合的题。这种方式对覆盖特定推理 pattern 的题特别有效。
Process Reward Model（PRM）
数据合成的进阶——不止过滤"答案对的解"，还要过滤"过程也对的解"。
PRM 是一个专门给推理过程的 每一步 打分的模型。训练时人工标注（或用更强模型自动标注）每一步是否正确，PRM 学到"什么样的推理步骤是合理的"。
应用方式：
- 数据过滤：丢弃 PRM 给中间步骤打低分的解
- 推理时打分：模型生成时让 PRM 监督每一步，发现错误立刻回退重试
- RL 信号：把 PRM 打分作为 reward 信号训练模型（OpenAI 的 PRM800K 工作）
PRM 是过去两年数学推理的关键 enabler。开源的 Math-Shepherd、PRM800K 都是这条路。
训练数据规模 vs 质量
数学训练数据有个反直觉的现象：高质量小数据集 > 低质量大数据集。Llemma、DeepSeek-Math、Minerva 的实验都表明几亿 token 的高质量数学数据训练效果，远超几十亿 token 的低质量数据。
所以"先合成大量再严格过滤"通常优于"合成多少留多少"。生产里的常见 ratio 是合成 100 万道题，过滤后留 10-30 万道，能用于训练的精华是这一小部分。
评测的注意事项
数学模型评测要小心几个坑：
评测集泄露。GSM8K、MATH 训练数据来自互联网，模型如果在训练时见过题目和答案，分数虚高。要严格做去污染——把测试集的题目对训练数据做 substring/near-duplicate 匹配清理。
评测的"答案匹配"陷阱。评测脚本如果只匹配最终数字，会出现"过程对但格式不同导致匹配失败"或者"过程错但碰到正确数字"的误判。好的评测脚本要做答案规范化（"15"、"15.0"、"\boxed{15}" 算一致）和过程合理性检查。
OOD 测试集：训练数据多源时容易在已知 benchmark 上虚高。AMC/AIME/PutnamBench 这些不太可能进训练数据的题集是更好的真实能力指标。
面试时可以这样答
数学推理数据难做的核心是三个原因。互联网数据质量差（多是题没过程）、人工标注极贵（要懂数学的人写完整步骤）、错误检测困难（不能简单 substring 匹配）。
主流合成方案有几条。第一是 LLM 生成 + 答案过滤——用强模型生成多个解，用最终答案匹配过滤。问题是答案对不代表过程对。第二是自一致性过滤——同一道题生成几十个解，看答案分布频率超过阈值才接受。代价是采样成本高但质量大幅提升。
第三是代码执行验证——把题转成 Python 跑一遍，执行结果作为 ground truth。DeepSeek-Math 大量用了这个，对计算性题型验证可靠。第四是形式化验证——用 Lean、Coq 把证明翻译成形式化语言让证明助手验证，理论上彻底可靠。MiniF2F、Llemma、DeepSeek-Prover 走这条路。第五是从答案反推过程，把"题-答"数据扩展成"题-过程-答"。
题型扩展上常用模板变体、难度递进、主题迁移、反向生成。Process Reward Model（PRM）是过去两年的关键 enabler——专门对推理过程每一步打分，用于过滤、推理时监督、或作为 RL 信号。
一个反直觉的发现是高质量小数据 > 低质量大数据。Llemma、DeepSeek-Math 都验证了几亿 token 高质量 > 几十亿 token 低质量。所以"合成大量 + 严格过滤"是主流路径，过滤掉 70-90% 也正常。
评测要避坑——GSM8K/MATH 容易污染要严格去重，答案匹配要做规范化避免误判，最好用 AMC/AIME 这类不太可能进训练数据的题集做真实能力评估。
常见追问
- PRM 自己怎么训练？标注每一步对错的数据怎么来？人工标 vs 自动标？
- Lean 这类形式化语言学习曲线陡，模型怎么习得？
- 数学合成数据训出来的模型，对未见过的题型泛化怎么样？怎么评估泛化能力？