FormalMATH : Évaluation du raisonnement mathématique formel des modèles de langage à grande échelle

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

May 5, 2025

Auteurs: Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, Weiyang Liu

cs.AI

Résumé

Le raisonnement mathématique formel reste un défi majeur pour l'intelligence artificielle, entravé par les limites des benchmarks existants en termes de portée et d'échelle. Pour y remédier, nous présentons FormalMATH, un benchmark à grande échelle basé sur Lean4, comprenant 5 560 problèmes formellement vérifiés, allant des défis olympiques du lycée aux théorèmes de niveau universitaire couvrant divers domaines (par exemple, algèbre, mathématiques appliquées, calcul, théorie des nombres et mathématiques discrètes). Pour atténuer l'inefficacité de la formalisation manuelle, nous introduisons un nouveau pipeline d'autoformalisation en boucle humaine qui intègre : (1) des modèles de langage spécialisés (LLMs) pour l'autoformalisation des énoncés, (2) une vérification sémantique multi-LLM, et (3) des stratégies de filtrage par réfutation basées sur la négation utilisant des prouveurs LLM prêts à l'emploi. Cette approche réduit les coûts d'annotation experts en conservant 72,09 % des énoncés avant vérification manuelle tout en garantissant la fidélité aux problèmes originaux en langage naturel. Notre évaluation des prouveurs de théorèmes basés sur les LLM les plus avancés révèle des limitations significatives : même les modèles les plus performants n'atteignent qu'un taux de réussite de 16,46 % dans des budgets d'échantillonnage pratiques, montrant un biais de domaine prononcé (par exemple, excellant en algèbre mais échouant en calcul) et une dépendance excessive aux tactiques d'automatisation simplifiées. Notamment, nous identifions une relation inverse contre-intuitive entre les indications de solutions en langage naturel et le succès des preuves dans les scénarios de raisonnement en chaîne de pensée, suggérant que le raisonnement informel écrit par les humains introduit du bruit plutôt que de la clarté dans les contextes de raisonnement formel. Nous croyons que FormalMATH fournit un benchmark robuste pour évaluer le raisonnement mathématique formel.

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.