FormalMATH: Avaliação do Raciocínio Matemático Formal em Modelos de Linguagem de Grande Escala

Resumo

O raciocínio matemático formal continua sendo um desafio crítico para a inteligência artificial, prejudicado pelas limitações dos benchmarks existentes em escopo e escala. Para enfrentar esse problema, apresentamos o FormalMATH, um benchmark em larga escala para o Lean4, composto por 5.560 problemas formalmente verificados, que abrangem desde desafios de olimpíadas de ensino médio até teoremas de nível universitário em diversos domínios (por exemplo, álgebra, matemática aplicada, cálculo, teoria dos números e matemática discreta). Para mitigar a ineficiência da formalização manual, introduzimos um novo pipeline de autoformalização com intervenção humana que integra: (1) modelos de linguagem de grande escala (LLMs) especializados para autoformalização de enunciados, (2) verificação semântica multi-LLM e (3) estratégias de filtragem por refutação baseadas em negação usando provadores LLM prontos para uso. Essa abordagem reduz os custos de anotação especializada, retendo 72,09% dos enunciados antes da verificação manual, ao mesmo tempo que garante fidelidade aos problemas originais em linguagem natural. Nossa avaliação dos melhores provadores de teoremas baseados em LLMs revela limitações significativas: mesmo os modelos mais fortes alcançam apenas 16,46% de taxa de sucesso sob orçamentos práticos de amostragem, exibindo um viés de domínio pronunciado (por exemplo, excelência em álgebra, mas falhas em cálculo) e uma dependência excessiva de táticas de automação simplificadas. Notavelmente, identificamos uma relação inversa contraintuitiva entre a orientação de soluções em linguagem natural e o sucesso das provas em cenários de raciocínio em cadeia de pensamento, sugerindo que o raciocínio informal escrito por humanos introduz ruído em vez de clareza em contextos de raciocínio formal. Acreditamos que o FormalMATH fornece um benchmark robusto para avaliar o raciocínio matemático formal.

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: Avaliação do Raciocínio Matemático Formal em Modelos de Linguagem de Grande Escala

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

Resumo

Support