Generazione di Dataset Guidata dalla Saturazione per il Ragionamento Matematico di LLM nell'Ecosistema TPTP
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
Autori: Valentin Quesnel, Damien Sileo
cs.AI
Abstract
La scarsità di dati di alta qualità e logicamente solidi rappresenta un collo di bottiglia critico per il progresso del ragionamento matematico nei Modelli Linguistici di Grande Dimensione (LLMs). Il nostro lavoro affronta questa sfida trasformando decenni di ricerca sul teorema automatico in un motore di dati scalabile. Invece di affidarsi a LLMs soggetti a errori o a complesse sintassi di assistenti di dimostrazione come Lean e Isabelle, il nostro framework sfrutta le capacità di saturazione di E-prover sulla vasta libreria di assiomi TPTP per derivare un corpus massiccio e garantito valido di teoremi. La nostra pipeline è principiata e semplice: satura gli assiomi, filtra i teoremi "interessanti" e genera compiti. Senza LLMs nel ciclo, eliminiamo gli errori fattuali per costruzione. Questi dati puramente simbolici vengono poi trasformati in tre sfide a difficoltà controllata: verifica di implicazione, selezione delle premesse e ricostruzione della dimostrazione. I nostri esperimenti zero-shot su modelli di frontiera rivelano una chiara debolezza: le prestazioni crollano sui compiti che richiedono un ragionamento profondo e strutturale. Il nostro framework fornisce sia lo strumento diagnostico per misurare questo divario sia una fonte scalabile di dati di addestramento simbolici per affrontarlo. Rendiamo disponibili pubblicamente il codice e i dati.
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