Risoluzione di Dimostrazioni di Disuguaglianze con Modelli Linguistici di Grande Scala

Abstract

La dimostrazione di disuguaglianze, cruciale in vari campi scientifici e matematici, mette alla prova abilità di ragionamento avanzato come la scoperta di limiti stretti e l'applicazione strategica di teoremi. Questo la rende una frontiera distinta e impegnativa per i grandi modelli linguistici (LLM), offrendo approfondimenti che vanno oltre la risoluzione generale di problemi matematici. Il progresso in questo ambito è ostacolato dai dataset esistenti, spesso scarsi, sintetici o rigidamente formali. Affrontiamo questo problema proponendo una formulazione del compito informale ma verificabile, trasformando la dimostrazione di disuguaglianze in due sottocompiti verificabili automaticamente: stima dei limiti e previsione delle relazioni. Basandoci su questo, rilasciamo IneqMath, un dataset curato da esperti di disuguaglianze di livello olimpico, che include un set di test e un corpus di arricchito con soluzioni passo-passo e annotazioni di teoremi. Sviluppiamo inoltre un nuovo framework di valutazione LLM-as-judge, combinando un giudice per la risposta finale con quattro giudici passo-passo progettati per rilevare errori comuni nel ragionamento. Una valutazione sistematica di 29 LLM leader su IneqMath rivela una realtà sorprendente: anche i modelli più avanzati come o1 raggiungono meno del 10% di accuratezza complessiva sotto scrutinio passo-passo; si tratta di un calo fino al 65,5% rispetto alla loro accuratezza considerando solo l'equivalenza della risposta finale. Questa discrepanza evidenzia catene deduttive fragili e un divario critico per gli attuali LLM tra il semplice trovare una risposta e la costruzione di una dimostrazione rigorosa. Aumentare le dimensioni del modello e il calcolo al momento del test produce guadagni limitati nella correttezza complessiva della dimostrazione. Invece, i nostri risultati evidenziano promettenti direzioni di ricerca come il ragionamento guidato da teoremi e l'auto-affinamento. Codice e dati sono disponibili su https://ineqmath.github.io/.

English

Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.

Risoluzione di Dimostrazioni di Disuguaglianze con Modelli Linguistici di Grande Scala

Solving Inequality Proofs with Large Language Models

Abstract

Support