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

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 方案是在「脏数据训出的模型」上打补丁；本方案是让语料库在源头就尽可能干净，让推理能力在中训练阶段就以正确的姿态注入模型。

🔄 [v2 改进]

核心数字来源说明

上述「约 20–30% 错误密度」并非凭空估算，有以下实证依据：

• Math-Shepherd（Wang et al., arXiv:2312.08935）通过 Monte Carlo rollout 对 GSM8K/MATH 的 CoT 步骤进行质量标注，发现在 GPT-3.5 生成的推理链中，约 20–30% 的推理步骤存在逻辑错误或跳步。
• Let’s Verify Step by Step（Lightman et al., arXiv:2305.20050）的人工标注实验表明，主流 LLM 在 MATH 数据集上生成的推理链中，约 25% 的步骤被人类标注者判定为存在错误。

「错误密度」定义明确化：本文中「错误密度」特指步骤级（step-level）错误比例——即推理链中存在逻辑错误的步骤数 ÷ 总步骤数。注意这与「样本级错误率」不同；样本级错误率（整条推理链至少有一步出错的比例）会显著更高，通常在 50–70%。本文使用步骤级指标，因为中训练的 next-token prediction 目标是在 token 层面建模，逐步骤的错误率对训练信号的污染程度更为直接相关。

5–10% 目标的推导：三层过滤后的加权错误密度估算如下：

• Layer 1（Lean 形式化验证，40–60% 覆盖率）：验证通过的数据中错误密度 ≈ 0%（Lean 验证器是完备的，通过即正确）
• Layer 2（程序执行验证，75–85% 覆盖率）：验证通过的数据中错误密度 ≈ 5%（仅最终结论被验证，中间步骤仍可能存在双重错误抵消）
• Layer 3（LLM 交叉验证，剩余数据）：验证通过的数据中错误密度 ≈ 15%（验证器与生成器存在共同盲区）

按各层数据占比加权（Layer 1 占约 1–2%，Layer 2 占约 10–12%，Layer 3 占约 87–89%），加权平均后整体错误密度约为 5–10%，相比未过滤的 20–30% 有实质性改善。

---

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% 样本)
            │               │
            └───────────────┘
                      ↓
               中训练语料库
        (干净推理链 + 错误→修正对比对)

🔄 [v2 改进]

三层过滤的质量分层方案：训练时数据权重设计

三层数据的质量差异不应被平铺混合忽略，而应在训练时以差异化权重体现，让模型更多学习高质量样本的推理风格：

训练时数据权重（相对于基础权重 ×1.0）：
- Layer 1 数据（Lean 形式化验证，精度最高）：权重 ×3.0
- Layer 2 数据（程序执行验证）：权重 ×2.0
- Layer 3 数据（LLM 交叉验证）：权重 ×1.0

加权方式可通过训练数据复制（oversampling）或 per-sample loss weight 实现，两种方式对大多数训练框架（DeepSpeed/Megatron）均可直接配置。

同时，每条数据应附加 verification_tier: 1|2|3 字段标注，让下游使用者（如 SFT 阶段、PRM 训练阶段）可按自身需求灵活筛选：

{
  "id": "math_aime_2023_p5_001",
  "verification_tier": 1,
  "layer_label": "lean4_verified",
  ...
}

这一字段的设计目标是将「数据的验证来源」作为一等公民元数据持久化，而不是在构建时丢失，确保整个数据管线的可追溯性。

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

🔄 [v2 改进]

领域偏斜的补充解决方案

上述三层架构在数据来源上天然偏向数学和编程领域（Lean 验证、程序执行均对这两类领域友好），可能导致中训练后模型在数学/编程推理上显著增强，但在科学推理、语言理解等领域出现退化。针对不同领域，建议采用分域治理策略：

领域	主用验证层	人工抽检比例	说明
数学 / 形式逻辑	Layer 1（Lean 验证） + Layer 2	5%	形式化工具最友好，质量最可靠
编程推理	Layer 2（程序执行） + Layer 1（局部）	5%	代码执行是天然验证器
科学推理（物理/化学/生物）	Layer 2（可执行实验仿真）为主	10%	方程求解、数值模拟可程序验证
语言理解 / 常识推理	Layer 3（LLM 交叉）	20%	缺乏客观验证器，须更高人工比例

混合比例设计：最终中训练语料中，建议按以下比例混合四类领域数据，防止「数学/编程极强、其他领域退化」的失衡：

• 数学 / 形式逻辑：35%
• 编程推理：25%
• 科学推理：20%
• 语言理解 / 常识推理：20%

该比例应根据目标模型的使用场景调整，但建议非数学/编程领域数据合计不低于 30%，以维持通用推理能力。

---

5. 客观评价

5.1 真正有价值的地方

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

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

5.2 局限与适用边界

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

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

5.3 合理期望

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

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

---

6. 评估闭环

🔄 [v2 改进]

评估方案：不只看最终答案，更要看推理步骤质量

本方案的核心主张是「减少推理步骤级错误」，因此评估不能只看标准 benchmark 的最终答案准确率——那是必要但不充分的指标。建议采用以下两层评估体系：

第一层：标准 benchmark 基线比较

在以下 benchmark 上测试加入本数据集前后的性能变化（控制其他训练数据不变）：

• GSM8K（小学数学，步骤相对简单）
• MATH（竞赛数学，多步骤推导）
• HumanEval / MBPP（代码推理）
• ARC-Challenge（科学推理）

预期：加入本数据集后上述指标应有不同幅度的提升，否则说明数据质量改进未转化为模型能力提升，需检查混合比例或权重设置。

第二层：过程正确性（Process Correctness）评测

仅看最终答案准确率可能掩盖「答案撞对但推导错误」的问题，更重要的指标是：

• 使用 Math-Shepherd 的 step-level 标注框架（或同类工具）对模型生成的推理链进行逐步打分，统计推理步骤级错误率
• 目标指标：步骤级错误率从基线的 ~25% 降低至 ~15%（保守目标）或 ~10%（乐观目标）
• 对比维度：加入本数据 vs. 只加入等量未过滤 CoT 数据 vs. 只加入 Layer 1 数据（消融验证三层架构的必要性）

评估结论的解读原则：

• 若最终答案准确率提升但步骤级错误率不变 → 说明模型学会了「从错误推导中碰巧得到正确答案」，中训练效果不理想
• 若步骤级错误率下降但最终答案准确率无变化 → 说明推理质量提升尚未转化为解题能力，可能需要增加数据量或调整后续 SFT
• 若两者均提升 → 方案验证成功，可推进规模化建设

---

注：本文为工作中草稿（WIP），部分规模估算基于公开数据集的粗略测算，实验验证尚未完成。v2 基于批判性评审意见补充了核心数字来源、质量分层权重方案、领域均衡策略和评估闭环设计。

原始版本：formal-verified-cot-midtraining-data