Geração de Conjuntos de Dados Orientada por Saturação para Raciocínio Matemático de LLMs no Ecossistema TPTP
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
Autores: Valentin Quesnel, Damien Sileo
cs.AI
Resumo
A escassez de dados de alta qualidade e logicamente sólidos é um gargalo crítico para o avanço do raciocínio matemático dos Modelos de Linguagem de Grande Escala (LLMs). Nosso trabalho enfrenta esse desafio transformando décadas de pesquisa em provas de teoremas automatizadas em um mecanismo escalável de geração de dados. Em vez de depender de LLMs propensos a erros ou de sintaxes complexas de assistentes de prova como Lean e Isabelle, nosso framework aproveita as capacidades de saturação do E-prover na vasta biblioteca de axiomas TPTP para derivar um corpus massivo de teoremas garantidamente válidos. Nosso pipeline é fundamentado e simples: saturar axiomas, filtrar teoremas "interessantes" e gerar tarefas. Sem LLMs no processo, eliminamos erros factuais por construção. Esses dados puramente simbólicos são então transformados em três desafios com dificuldade controlada: verificação de implicação, seleção de premissas e reconstrução de provas. Nossos experimentos zero-shot em modelos de ponta revelam uma clara fraqueza: o desempenho entra em colapso em tarefas que exigem raciocínio profundo e estrutural. Nosso framework fornece tanto a ferramenta de diagnóstico para medir essa lacuna quanto uma fonte escalável de dados simbólicos de treinamento para abordá-la. Disponibilizamos o código e os dados publicamente.
https://github.com/sileod/reasoning_core
https://hf.co/datasets/reasoning-core/rc1
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