[WIP] 形式化验证辅助的推理链语料：中训练阶段的推理能力奠基

1. 问题定位：中训练阶段的推理链数据困境

中训练（Continued Pre-training / Mid-training）的目标，是在基座模型之上注入领域推理能力的倾向——它不改变训练目标（仍是 next-token prediction），而是通过向模型喂入高质量的领域语料，让模型在权重层面形成「把推理过程写清楚」的习惯。这个阶段是推理能力建立的早期基础，一旦打歪，后续无论 SFT 还是 RLHF 都是在歪基础上修补。

1.1 推理链语料的来源现状

当前可用的推理链数据大致来自两类：

人工撰写的高质量题解——教材例题、AMC/AIME 竞赛官方解析、数学奥林匹克答案等。这类数据推导严谨、步骤完整，是理想的中训练素材。问题在于规模严重受限：公开可用的高质量数学推理链总量约在几十万条以内，对于需要数亿 token 的中训练来说远远不够。

LLM 合成的推理链——以 NuminaMath、OpenHermes 为代表，用强模型批量生成 CoT 数据。规模可以轻松扩展到数百万条，但存在一个根本性的隐患：合成推理链中充斥着「推导看起来对但实际有逻辑跳步或结论错误」的样本。模型在生成推理链时，会在不确定的步骤处依赖语言流畅性「蒙混过关」，最终答案甚至可能碰巧正确，但中间某几步的推导实际上是错的。

1.2 核心问题：隐性错误的污染效应

大量吃进含隐性错误的推理链会对模型造成什么影响？直觉上，next-token prediction 对偶发噪声有一定容忍度，但当错误呈现系统性分布时——比如「代入检验步骤经常被跳过」「结论推导中经常省略某类边界条件」——模型会学到这种跳步习惯，并在推理时复现它。这不是可以轻易通过 RLHF 纠正的浅层问题，而是在权重中编码的推理风格偏好。

1.3 形式化验证的切入点

本提案的核心思路：用形式化验证和程序执行作为数据清洗层，在数据进入中训练语料库之前过滤掉逻辑错误，而不是训练一个 Process Reward Model（PRM）在推理时打分。

这两种路径的根本区别在于：PRM 方案是在「脏数据训出的模型」上打补丁；本方案是让语料库在源头就尽可能干净，让推理能力在中训练阶段就以正确的姿态注入模型。

---

2. 与现有方案的对比

方案	目标	核心手段	与本方案的差异
NuminaMath / OpenHermes	扩大 CoT 数据规模	LLM 合成	噪声问题未根本解决
Math-Shepherd / OmegaPRM	训练 Process Reward Model	MC 采样估计步骤价值	目标是奖励模型，非语料清洗
DeepSeek-Prover / Llemma	让模型学会写 Lean 证明	形式化证明微调	目标是形式化能力，非自然语言推理链
本方案	构建干净的中训练推理链语料	形式化验证作数据过滤器	产出自然语言推理链，中训练直接可用

Math-Shepherd 和 OmegaPRM 的思路非常有价值，但它们解决的是「如何在推理时识别好步骤」，本方案解决的是「如何在训练前就保证步骤是对的」。DeepSeek-Prover 走的是形式化证明路线，模型需要学习 Lean 语法，是另一条赛道。本方案的产出物是干净的自然语言推理链，训练目标不变，只是数据质量得到保证。

---

3. 具体构建方案

3.1 数据来源：三层架构

根据可验证性强弱，将数据来源分为三层：

Layer 1 — 可形式化验证的数学推理链（精度最高，规模最小）

• 来源：MATH 数据集（12,500 题）、AMC 10/12 历年真题、AIME 竞赛题、Lean MiniF2F benchmark 对应的自然语言解题过程
• 验证方式：将推理链的关键结论翻译成 Lean 4 定理并调用验证器；或对数值计算结论用 SymPy 等符号计算器做精确验证
• 特点：验证结果可信度最高，但 autoformalization 成功率约 40–60%，覆盖率有限

Layer 2 — 可程序化验证的推理链（覆盖较广，精度中等）

• 来源：代码推理题（从代码执行结果反推推理链是否正确）、统计推断题（用 Python 复现计算步骤）、数值计算类题目
• 验证方式：提取推理链中的数值结论，编写验证脚本执行，对比程序输出与推理链声称的结果
• 特点：能覆盖 Lean 无法处理的计算类场景，但只能验证「结论可计算性」，无法验证推导路径的合法性

Layer 3 — LLM 交叉验证的推理链（规模最大，精度最低）

• 来源：大规模 LLM 合成 CoT（如 NuminaMath-CoT、Orca 系列）
• 验证方式：用另一个强模型（如 Claude 3.5 Sonnet 或 GPT-4o）对推理链的每个步骤做逻辑一致性检验，要求多个独立验证通过为准入条件
• 特点：可扩展到数百万条，但验证者和生成者同属 LLM，存在系统性盲区

3.2 过滤流水线

┌─────────────────────────────────────────┐
│         LLM 批量生成推理链               │
│   (每题生成 4-8 条，保留多样性)          │
└───────────────┬─────────────────────────┘
                │
                ▼
┌─────────────────────────────────────────┐
│       结构化解析                         │
│  · 分割推理步骤（Step 1, Step 2, ...）   │
│  · 提取每步中间结论                      │
│  · 标注最终答案                          │
└───────────────┬─────────────────────────┘
                │
                ▼
┌─────────────────────────────────────────┐
│           按题型分流                     │
└────┬──────────────┬──────────────┬──────┘
     │              │              │
     ▼              ▼              ▼
  数学/逻辑题    代码/计算题     其他推理题
     │              │              │
  Lean 验证    程序执行验证    LLM 交叉验证
  符号计算        结论比对      多数同意规则
     │              │              │
     └──────┬────────┘──────┬──────┘
            │               │
          通过             失败
            │               │
            ▼               ▼
     加入干净语料库    错误分类器
            │         (跳步 / 结论错误 /
            │          前提错误 / 循环论证)
            │               │
            │               ▼
            │         LLM 生成修正版本
            │               │
            │               ▼
            │         人工抽检 (10% 样本)
            │               │
            └───────────────┘
                      ↓
               中训练语料库
        (干净推理链 + 错误→修正对比对)

3.3 失败案例的额外利用：推理纠错数据

被过滤掉的推理链不应直接丢弃。分类之后，可以构造「错误推理 → 修正推理」的对比对，作为推理纠错数据注入中训练语料。这类数据让模型在预训练阶段就接触到「识别跳步并补全」「识别错误结论并纠正」的模式，是比单纯干净数据更丰富的训练信号。

以下是对比对的 JSON 格式示例：

{
  "type": "correction_pair",
  "problem": "证明：对任意正整数 n，n² + n 是偶数。",
  "error_chain": {
    "steps": [
      "Step 1: n² + n = n(n+1)",
      "Step 2: n 和 n+1 是相邻整数",
      "Step 3: 所以 n(n+1) 是偶数。"
    ],
    "error_type": "logical_gap",
    "error_location": "Step 2→Step 3",
    "error_description": "跳过了「相邻整数中必有一个偶数，故乘积为偶数」的关键推导步骤"
  },
  "corrected_chain": {
    "steps": [
      "Step 1: n² + n = n(n+1)",
      "Step 2: n 和 n+1 是相邻整数，其中必有一个为偶数（若 n 为偶数则 n 本身是偶数；若 n 为奇数则 n+1 为偶数）",
      "Step 3: 任意整数与偶数的乘积为偶数，故 n(n+1) 是偶数。",
      "Step 4: 因此 n² + n 是偶数，证毕。"
    ],
    "verification": {
      "method": "lean4",
      "status": "verified"
    }
  }
}

3.4 数据格式设计

格式一：验证通过的干净推理链

{
  "type": "verified_chain",
  "id": "math_aime_2023_p5_001",
  "source": "AIME 2023 Problem 5",
  "problem": "设实数 x 满足 x³ - 3x = √(x+2)，求 x² 的所有可能值之和。",
  "chain": {
    "steps": [
      "Step 1: 两边平方，注意左边需非负：(x³-3x)² = x+2",
      "Step 2: 展开得 x⁶ - 6x⁴ + 9x² = x + 2",
      "Step 3: 整理为 x⁶ - 6x⁴ + 9x² - x - 2 = 0",
      "Step 4: 验证 x=√(2+√2) 满足原方程（代入验证），得 x²=2+√2",
      "Step 5: 同理验证 x=-√(2-√2)，得 x²=2-√2",
      "Step 6: x² 所有可能值之和为 (2+√2)+(2-√2) = 4"
    ],
    "answer": "4"
  },
  "verification": {
    "method": "sympy_symbolic",
    "script": "verify_aime_2023_p5.py",
    "status": "passed",
    "checked_at": "2026-03-28T14:22:00Z"
  },
  "layer": 1,
  "quality_score": 0.97
}

格式二：错误推理 → 修正版 对比对（见 3.3 节示例，结构相同）

3.5 数据规模估算

层级	原始来源规模	预期 autoformalization / 验证成功率	净产出（干净推理链）
Layer 1（形式化验证）	~15 万题	40–60%（Lean 翻译）× 70%（证明成功）	~4–6 万条
Layer 2（程序执行验证）	~50 万题	75–85%	~38–42 万条
Layer 3（LLM 交叉验证）	~500 万条	55–65%（多数同意通过）	~275–325 万条
纠错对比对（失败案例再利用）	失败样本约 200 万	50% 可生成有效修正版	~100 万对

目标中训练语料规模：约 350–450 万条推理链 + 100 万纠错对，折合约 40–60 亿 token（以平均每条推理链 800–1200 token 估算）。这一规模对于专注于数学/推理领域的中训练阶段是可用的量级。

---

4. 关键技术难点

4.1 Autoformalization 的准确率瓶颈

将自然语言推理链翻译成 Lean 4 定理（autoformalization）是 Layer 1 的核心依赖，但当前最优方案（如 LeanDojo + GPT-4o）的成功率约在 40–60%。这意味着：即使题目本身有清晰的形式化对应，仍有相当比例的推理链因翻译失败而无法进入 Layer 1 验证，只能降级到 Layer 3 处理。换言之，Layer 1 的高精度是以低覆盖率为代价的。这一限制在短期内不会消除，提案必须接受 Layer 1 只能覆盖全量数据的约 10–15% 这一现实。

4.2 程序执行验证的结构性局限

Layer 2 的程序执行验证只能检验「推理链的最终结论是否与程序计算结果一致」，但无法检验推导过程本身是否合法。一个典型的问题是：推理链可能在中间某步犯了错（如符号判断错误），但后续又通过另一个错误把结果「纠正」回来，最终答案正确，程序验证通过。这类「双重错误抵消」的样本会被误判为干净数据。缓解手段是对推理链中每个关键中间结论都单独执行验证，而不只验证最终答案。

4.3 LLM 交叉验证的同质性问题

Layer 3 用强模型验证另一个强模型生成的推理链，存在系统性盲区：如果生成模型和验证模型共享相似的训练数据，那么两者可能对同一类错误都「看不出来」。比如，当前主流大模型在某些概率论直觉题上存在共同的偏差（蒙提霍尔问题变体、条件概率解读等），用同类模型交叉验证无法发现这类系统性错误。解法之一是在验证阶段引入多样化的验证模型（不同训练来源）并要求更严格的一致性标准，但这会大幅提高成本。

---

5. 客观评价

5.1 真正有价值的地方

本方案的核心贡献是把「推理链质量保证」从事后前移到数据构建阶段。传统路径是：先用脏数据训模型，再通过 RLHF 或 PRM 在推理时纠偏。这条路在实践中有效，但始终是在修补——模型在权重层面已经编码了某些错误推理模式，事后的奖励信号需要克服这些根深蒂固的偏好。

中训练阶段打好基础的核心收益是减少后续对齐的阻力：如果模型在中训练阶段就习惯了「步步有据」的推理风格，SFT 和 RLHF 只需要在此基础上调整格式和偏好，而不需要从零扭转推理习惯。这对于资源有限、无法做大规模 RLHF 的团队尤其有价值。

5.2 局限与适用边界

本方案的适用范围主要集中在可验证的推理领域——数学、形式逻辑、程序推理。对于常识推理、社会科学推断、开放域问答等「没有客观正确答案」的场景，形式化验证完全无用，LLM 交叉验证的质量也大打折扣。

此外，本方案需要相当的工程投入：维护 Lean 环境、编写验证脚本、构建分类流水线，对于小团队而言门槛不低。

5.3 合理期望

在当前技术水平下，本方案能做到的是：显著降低中训练数学/逻辑推理语料中的逻辑跳步和结论错误比例，而不是「消灭所有错误」。过滤后的语料中仍会存在 Layer 3 漏网的系统性错误、Layer 2 的双重错误抵消样本。合理的预期是：将语料中的逻辑错误密度从未过滤时的约 20–30%（基于人工抽检估算）降低到 5–10%，这对中训练质量是有实际意义的提升，但不是一个完美解。

过度乐观地期待「形式化验证 = 完全干净的推理链」是危险的。更务实的定位是：这是一套工程上可行、效果有限但成本可控的数据质量提升方案，在等待 autoformalization 技术成熟之前，它是数据工程师手头最靠谱的推理链清洗工具之一。

---

注：本文为工作中草稿（WIP），部分规模估算基于公开数据集的粗略测算，实验验证尚未完成。