用自动定理证明生成高质量数学推理数据，解决LLM训练数据匮乏问题。
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
- 基于TPTP库与E-prover饱和机制自动生成逻辑有效定理
- 构建三类可控难度的数学推理任务，零样本测试发现深层推理缺陷
- 纯符号数据无错误，适合研究和训练需要严谨逻辑的模型
大型语言模型（LLMs）在数学推理方面面临高质量、逻辑正确的数据稀缺瓶颈。本文将数十年自动化定理证明研究成果转化为可扩展的数据引擎，不依赖易出错的LLMs或复杂证明助手语法（如Lean、Isabelle），而是利用E-prover在庞大的TPTP公理库上进行饱和运算，生成大规模且保证有效的定理语料库。其流程简洁：饱和公理 → 筛选‘有趣’定理 → 生成任务。全程无LLMs参与，从源头杜绝事实性错误。该纯符号数据被转化为三类难度可控的任务：蕴含验证、前提选择与证明重构。对前沿模型的零样本实验揭示明显弱点：需深层结构推理的任务性能急剧下降。本框架既可诊断此差距，也可提供可扩展的符号化训练数据以弥补。代码与数据已公开：https://github.com/sileod/reasoning_core https://hf.co/datasets/reasoning-core/rc1。
原文摘要 · Abstract (English)
The scarcity of high-quality, logically sound data is a critical bottleneck for advancing the mathematical reasoning of Large Language Models (LLMs). Our work confronts this challenge by turning decades of automated theorem proving research into a scalable data engine. Rather than relying on error-prone LLMs or complex proof-assistant syntax like Lean and Isabelle, our framework leverages E-prover's saturation capabilities on the vast TPTP axiom library to derive a massive, guaranteed-valid corpus of theorems. Our pipeline is principled and simple: saturate axioms, filter for "interesting" theorems, and generate tasks. With no LLMs in the loop, we eliminate factual errors by construction. This purely symbolic data is then transformed into three difficulty-controlled challenges: entailment verification, premise selection, and proof reconstruction. Our zero-shot experiments on frontier models reveal a clear weakness: performance collapses on tasks requiring deep, structural reasoning. Our framework provides both the diagnostic tool to measure this gap and a scalable source of symbolic training data to address it. We make the code and data publicly available. https://github.com/sileod/reasoning_core https://hf.co/datasets/reasoning-core/rc1
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。