[Paper] 推理核心：可扩展的过程式数据生成套件，用于符号预训练和后训练

Source: arXiv - 2603.02208v1

（请提供您希望翻译的具体文本内容，我将为您翻译成简体中文，并保持原有的格式、Markdown 语法以及技术术语不变。）

概述

本文介绍了 Reasoning Core，一个全新的开源套件，能够在运行时生成海量 可验证 的符号推理数据。通过程序化创建诸如规划问题、一阶逻辑陈述、语法解析、贝叶斯网络因果关系以及方程组等任务，作者为语言模型研究者提供了一种在完全可检验且持续可扩展的数据上进行预训练或微调的方法。他们的实验表明，在模型的预训练混合中加入这些数据可以提升下游推理能力，同时不会削弱（甚至有时还能提升）模型的原始语言性能。

关键贡献

• Procedural generator suite covering five core formal domains (PDDL planning, FOL with equality, CFG parsing, Bayesian‑network causal reasoning, and linear equation solving).
• External solvers attached to each generator for automatic, rigorous verification of every sample.
• Difficulty‑curriculum control that lets users dial the complexity of generated instances on a smooth scale.
• Optional reasoning traces (step‑by‑step solver outputs) that can be used for supervised learning from the earliest pre‑training stages.
• Unified API that also supplies verifiable reward functions for reinforcement‑learning experiments.
• Empirical evidence that mixing Reasoning Core data into large‑scale pre‑training improves zero‑shot reasoning on benchmark tasks while preserving language‑model perplexity.

方法论

1. 任务生成 – 对于每个形式化领域，轻量级过程引擎随机实例化问题参数（例如，对象、谓词、文法规则、网络拓扑）。随机性使用种子，使得相同的“难度级别”在不同运行之间产生可比的挑战。
2. 求解器验证 – 使用现成的精确求解器（例如 PDDL 规划器、一阶定理证明器、CFG 解析器、贝叶斯推理引擎、线性系统求解器）对生成的实例进行求解。如果求解器找到解，则保留该实例；否则丢弃，从而保证每个保留的示例都是 真实正确 的。
3. 轨迹提取（可选） – 求解器可以输出详细的证明或执行轨迹（例如，计划步骤、消解步骤、解析树、变量赋值）。这些轨迹与原始问题陈述一起存储，提供监督信号。
4. 课程调度 – 难度被编码为数值旋钮（例如，对象数量、逻辑公式深度、贝叶斯网络规模）。研究者可以均匀采样、偏向更难的示例，或采用随训练进展逐步提升难度的课程安排。
5. 与语言模型训练的集成 – 生成的（问题，解答）对被分词后混入常规的下一个 token 预测目标。对于强化学习风格的实验，套件还会返回确定性的奖励（例如，模型答案与求解器一致则为 1，否则为 0）。

结果与发现

总体而言，数据 不会降低 模型生成流畅文本的能力，并且 显著提升 在纯语言模型预训练难以处理的符号推理基准上的表现。

实际意义

• 更好的下游工具推理 – 开发代码助手、自动定理证明器或规划机器人的开发者现在可以在与目标任务逻辑结构相匹配的数据上进行预训练，从而产生更可靠的输出。
• 基于课程的微调 – 难度旋钮实现了“渐进超负荷”策略：先从简单谜题开始，随后逐步引入更难的题目，类似于人类学习。这可以减少达到目标准确率所需的微调步骤数量。
• 强化学习环境 – 由于每个实例都附带确定性的奖励，该套件可作为符号推理强化学习研究的沙盒（例如，教会智能体进行规划或求解方程）。
• 开源且可扩展 – 基于 MIT 许可证的代码可以直接嵌入现有数据流水线，模块化设计也使得添加新领域（例如图论问题、类型理论练习）变得简便。
• 基准生成 – 研究人员可以按需生成自定义、可验证的测试集，免去手动策划或手动验证符号数据集的需求。

限制与未来工作

• Solver bottleneck – 生成和验证大量数据计算密集；将规模扩展到万亿级 token 可能需要分布式求解器集群或近似验证。
• Domain coverage – 虽然五个核心领域已经很广，但许多实际推理任务（例如概率编程、高阶逻辑）尚未涵盖。
• Transfer gap – 虽然观察到的提升一致，但对非常大的模型（例如 GPT‑5）而言提升有限，表明随着模型容量增长收益递减。
• Human‑readability – 某些生成的实例（尤其是大型贝叶斯网络）对人类检查来说可能笨重，限制了手动调试。

未来工作可以探索由模型性能驱动的adaptive difficulty scheduling，整合用于更快数据生成的approximate solvers，并将套件扩展到覆盖domain‑specific reasoning（例如安全策略分析、硬件验证）。

Reasoning Core 为开发者提供了一条实用路径，能够将严格验证的符号推理注入驱动当今语言模型的海量预训练流水线，弥合原始文本流畅性与逻辑能力之间的差距。

作者

• Valentin Lacombe
• Valentin Quesnel
• Damien Sileo

论文信息

• arXiv ID: 2603.02208v1
• 分类: cs.CL
• 出版日期: 2026年3月2日
• PDF: 下载 PDF