FormalMATH: Valutazione del Ragionamento Matematico Formale nei Modelli Linguistici di Grande Dimensione

Abstract

Il ragionamento matematico formale rimane una sfida cruciale per l'intelligenza artificiale, ostacolato dalle limitazioni degli attuali benchmark in termini di portata e scala. Per affrontare questo problema, presentiamo FormalMATH, un benchmark su larga scala basato su Lean4 che comprende 5.560 problemi formalmente verificati, che spaziano dalle sfide delle Olimpiadi di matematica delle scuole superiori ai teoremi di livello universitario in diversi ambiti (ad esempio, algebra, matematica applicata, calcolo, teoria dei numeri e matematica discreta). Per mitigare l'inefficienza della formalizzazione manuale, introduciamo una nuova pipeline di autoformalizzazione con l'uomo nel ciclo che integra: (1) modelli linguistici di grandi dimensioni (LLM) specializzati per l'autoformalizzazione delle affermazioni, (2) verifica semantica multi-LLM e (3) strategie di filtraggio delle confutazioni basate sulla negazione utilizzando dimostratori basati su LLM già disponibili. Questo approccio riduce i costi di annotazione degli esperti mantenendo il 72,09% delle affermazioni prima della verifica manuale, garantendo al contempo la fedeltà ai problemi originali in linguaggio naturale. La nostra valutazione dei dimostratori di teoremi basati su LLM all'avanguardia rivela significative limitazioni: anche i modelli più potenti raggiungono solo un tasso di successo del 16,46% con budget di campionamento pratici, mostrando un marcato bias di dominio (ad esempio, eccellendo in algebra ma fallendo in calcolo) e un'eccessiva dipendenza da tattiche di automazione semplificate. In particolare, identifichiamo una relazione inversa controintuitiva tra la guida alla soluzione in linguaggio naturale e il successo della dimostrazione negli scenari di ragionamento a catena di pensiero, suggerendo che il ragionamento informale scritto dall'uomo introduce rumore piuttosto che chiarezza nei contesti di ragionamento formale. Crediamo che FormalMATH fornisca un benchmark solido per valutare il ragionamento matematico formale.

English

Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning.

FormalMATH: Valutazione del Ragionamento Matematico Formale nei Modelli Linguistici di Grande Dimensione

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

Abstract

Support