FormalMATH: Оценка способности крупных языковых моделей к формальному математическому рассуждению

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

May 5, 2025

Авторы: 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

Аннотация

Формальное математическое рассуждение остается важной задачей для искусственного интеллекта, ограниченной недостатками существующих тестовых наборов в плане охвата и масштаба. Чтобы решить эту проблему, мы представляем FormalMATH — крупномасштабный тестовый набор на основе Lean4, включающий 5 560 формально верифицированных задач, охватывающих от олимпиадных задач уровня старшей школы до теорем уровня бакалавриата в различных областях (например, алгебра, прикладная математика, математический анализ, теория чисел и дискретная математика). Для снижения неэффективности ручной формализации мы предлагаем новый подход с участием человека в цикле автоматической формализации, который включает: (1) специализированные большие языковые модели (LLM) для автоматической формализации утверждений, (2) семантическую проверку с использованием нескольких LLM и (3) стратегии фильтрации опровержений на основе отрицания с использованием готовых LLM-доказывателей. Этот подход снижает затраты на экспертные аннотации, сохраняя 72,09% утверждений до ручной проверки, при этом обеспечивая точность по отношению к исходным задачам на естественном языке. Наша оценка современных LLM-доказывателей выявила значительные ограничения: даже самые мощные модели достигают успеха только в 16,46% случаев при практических бюджетах выборки, демонстрируя выраженную предвзятость в зависимости от области (например, успехи в алгебре, но провалы в анализе) и чрезмерную зависимость от упрощенных тактик автоматизации. Примечательно, что мы обнаружили неожиданную обратную зависимость между руководством по решению на естественном языке и успехом доказательства в сценариях рассуждения с цепочкой мыслей, что указывает на то, что неформальные рассуждения, написанные человеком, вносят шум, а не ясность в формальные рассуждения. Мы считаем, что FormalMATH предоставляет надежный тестовый набор для оценки формального математического рассуждения.

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.