TPTP axiom library

该数据集是TPTP公理库，包含大量的公理，用于生成数学推理任务。数据集通过饱和引擎E-prover生成，保证了所有定理的数学有效性。数据集被用于构建三个难度可控的挑战：蕴涵验证、前提选择和证明重构。数据集的访问地址为https://github.com/sileod/reasoning_core。This dataset is the TPTP axiom library containing a large number of axioms for generating mathematical reasoning tasks. It is generated by the saturation-based theorem prover E-prover, which guarantees the mathematical validity of all included theorems. This dataset is utilized to construct three difficulty-controllable challenges: implication verification, premise selection, and proof reconstruction. The access URL of this dataset is https://github.com/sileod/reasoning_core.

原始信息汇总

数据集概述

基本信息

• 数据集名称: reasoning core ◉
• 核心功能: 基于文本的RLVR（强化学习与验证推理）用于LLM（大语言模型）推理训练
• 核心任务类型: 符号化任务，包括完整的一阶逻辑（FOL）、基于TPTP的形式数学、新型领域的正式规划以及语法任务

安装与使用

主要环境安装

python #!pip install uv #install uv if needed !uv tool install prime --with openai -q !uv tool run prime -- env install sileod/reasoning-core-env

from verifiers import load_environment import os; from openai import OpenAI

env = load_environment("reasoning-core-env")

os.environ["OPENROUTER_API_KEY"] = "" #✍️ write your key client = OpenAI( base_url="https://openrouter.ai/api/v1", api_key=os.getenv("OPENROUTER_API_KEY")) results = env.evaluate(client=client, model="gpt-4.1-mini", num_examples=20, rollouts_per_example=1) df=env.make_dataset(results).to_pandas()

独立安装方式

python pip install reasoning_core

from reasoning_core import list_tasks, get_task, score_answer

T = get_task(arith)() x = T.generate_example() assert score_answer(x.answer, x)==1

数据生成

• 生成方式: 运行 bash run_generate.sh 进行多线程生成到json文件
• 兼容性: 生成的文件可由Huggingface Datasets读取

与Reasoning Gym集成

• 接口特性: 使用比reasoning-gym（RG）更精简的自定义接口
• 任务正交性: 所有任务与RG正交，但可导入到RG中使用
• 集成示例: python import reasoning_gym

from reasoning_core import register_to_reasoning_gym register_to_reasoning_gym()

specs = [ # here, leg_counting tasks will make up two thirds of tasks DatasetSpec(name=leg_counting, weight=2, config={}), #from reasoning_gym 🏋 DatasetSpec(name=arith, weight=2, config={}), #from reasoning_core ◉ ] D=reasoning_gym.create_dataset(composite, size=10, seed=42, datasets=specs)

搜集汇总

数据集介绍

构建方式

该数据集构建于自动定理证明领域的成熟生态之上，采用纯符号化方法确保数学有效性。其核心流程分为三个阶段：首先利用E定理证明器对TPTP公理库进行饱和推导，生成完整的逻辑推导有向无环图；随后通过AGInTRater系统基于复杂性、惊奇性和有用性等启发式指标对推导结果进行筛选，保留数学意义显著的定理；最后借助Vampire定理证明器对所有输出进行验证，形成结构化的推理任务集合。整个过程完全自动化且可重现，无需依赖大型语言模型即可保证逻辑正确性。

使用方法

该数据集的使用遵循严格的零样本评估范式。对于蕴涵验证任务，模型需基于给定的前提集判断目标定理是否可推导；最小前提选择任务要求从包含干扰项的候选池中识别出必要且充分的前提子集；证明图重构任务则需要模型根据乱序的条款列表重建完整的推导依赖结构。所有任务均提供领域公理作为背景知识，但明确限定仅允许使用指定前提进行推理。评估时采用结构连贯性和逻辑正确性双重检验标准，确保对模型推理能力的精准测量。

背景与挑战

背景概述

在人工智能领域，提升大型语言模型的数学推理能力一直是核心研究目标，然而高质量逻辑数据的稀缺严重制约了该领域的发展。2025年，法国里尔大学CRIStAL实验室的Valentin Quesnel与Damien Sileo基于TPTP公理库构建了饱和驱动的数据集生成框架，旨在解决形式化数学证明数据规模小、人工标注成本高的问题。该工作通过Eprover的饱和推导能力，从代数、域论、几何等数学子领域中系统生成保证逻辑有效性的定理库，为符号推理任务提供了可扩展的数据引擎，显著推动了自动定理证明与神经符号推理的交叉研究。

当前挑战

该数据集需解决数学推理中多步演绎的结构化挑战，包括蕴含验证的最小前提判定、干扰环境下的前提选择、以及证明图重构的全局依赖关系还原。构建过程中面临组合爆炸问题：饱和推导产生的子句数量随深度指数增长，需通过AGInTRater兴趣度指标筛选非平凡定理；同时需保证生成任务的逻辑严谨性，依赖Vampire定理证明器对数千条推导关系进行语义验证，以避免形式系统下的隐含错误。

常用场景

经典使用场景

在自动定理证明领域，TPTP axiom library作为基础逻辑公式库，其经典使用场景集中于为大型语言模型的数学推理能力提供结构化评估。该数据集通过E-prover的饱和推导机制，系统生成包含代数、几何与拓扑等多领域的定理证明任务，研究者可据此构建蕴含验证、前提选择与证明图重构三类核心任务，精确测量模型在符号逻辑层面的演绎深度。

解决学术问题

该数据集有效解决了形式化数学数据稀缺导致的模型推理能力瓶颈问题。通过保证生成定理的数学正确性，它消除了传统LLM生成数据存在的事实性错误风险，为研究多步演绎、结构推理等核心能力提供了纯净的实验环境。其意义在于建立了可量化评估逻辑推理深度的标准框架，推动了符号推理与神经网络结合的跨领域研究。

实际应用

在实际应用中，该数据集支撑了数学教育智能系统的开发，通过生成难度可控的推理题目辅助逻辑思维训练。在自动定理证明领域，其衍生的任务框架可用于增强证明辅助工具的前提推荐功能，提升交互式证明效率。此外，它为金融、信息安全等需高可靠性验证的领域提供了逻辑一致性检验的基准数据源。

数据集最近研究

最新研究方向

在自动定理证明领域，TPTP公理库正成为推动大语言模型数学推理能力突破的关键基础设施。最新研究聚焦于利用E-prover的饱和推导技术，从该库中系统生成大规模、逻辑保证正确的定理数据集，彻底规避了传统LLM生成方法的事实错误风险。研究热点体现在三个结构化任务设计：蕴涵验证测试演绎推理的精确性，最小前提选择评估噪声环境下的假设筛选能力，而证明图重构任务则揭示了当前模型在全局结构性推理上的根本缺陷。这一范式不仅为数学推理提供了可扩展的符号数据源，更通过粒度化的任务拆解建立了诊断模型逻辑深度的新标准，对推动形式化推理与自然语言处理的融合具有深远意义。

相关研究论文

• Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem

  法国里尔大学,Inria,CNRS,Centrale Lille,UMR 9189-CRIStAL · 2025年