FormalMATH: Benchmarking des formalen mathematischen Denkens von großen Sprachmodellen

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

May 5, 2025

Autoren: 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

Zusammenfassung

Formales mathematisches Denken bleibt eine entscheidende Herausforderung für künstliche Intelligenz, die durch die begrenzte Reichweite und den Umfang bestehender Benchmarks behindert wird. Um dies zu adressieren, präsentieren wir FormalMATH, einen groß angelegten Lean4-Benchmark, der 5.560 formal verifizierte Probleme umfasst, die von Herausforderungen auf dem Niveau von Schulolympiaden bis hin zu Theoremen auf Universitätsniveau in verschiedenen Domänen (z. B. Algebra, angewandte Mathematik, Analysis, Zahlentheorie und diskrete Mathematik) reichen. Um die Ineffizienz der manuellen Formalisierung zu verringern, führen wir eine neuartige Autoformalisierungs-Pipeline mit menschlicher Beteiligung ein, die Folgendes integriert: (1) spezialisierte Large Language Models (LLMs) für die Autoformalisierung von Aussagen, (2) semantische Verifizierung durch mehrere LLMs und (3) Negations-basierte Widerlegungsfilterungsstrategien unter Verwendung von Standard-LLM-basierten Beweisern. Dieser Ansatz reduziert die Kosten für Expertenannotationen, indem 72,09 % der Aussagen vor der manuellen Überprüfung beibehalten werden, während gleichzeitig die Treue zu den ursprünglichen natürlichen Sprachproblemen gewährleistet wird. Unsere Bewertung von state-of-the-art LLM-basierten Theorembeweisern zeigt erhebliche Einschränkungen: Selbst die stärksten Modelle erreichen nur eine Erfolgsquote von 16,46 % unter praktischen Sampling-Budgets und weisen eine ausgeprägte Domänenverzerrung auf (z. B. hervorragende Leistungen in der Algebra, aber Versagen in der Analysis) sowie eine übermäßige Abhängigkeit von vereinfachten Automatisierungstaktiken. Bemerkenswerterweise identifizieren wir einen kontraintuitiven umgekehrten Zusammenhang zwischen natürlicher Sprachlösungsführung und Beweiserfolg in Chain-of-Thought-Szenarien, was darauf hindeutet, dass von Menschen verfasste informale Argumentation in formalen Denksettings eher Rauschen als Klarheit einführt. Wir glauben, dass FormalMATH einen robusten Benchmark für die Bewertung formalen mathematischen Denkens bietet.

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.