MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification

TL;DR

MSC-180 is a comprehensive benchmark with 180 formal problems across 60 mathematical domains, designed to evaluate and improve the reasoning capabilities of AI theorem provers beyond pattern matching.

Contribution

This paper introduces MSC-180, a new benchmark with expert-verified problems across diverse domains, and proposes the coefficient of variation as a metric to assess model generalization and domain bias.

Findings

State-of-the-art LLM provers achieve only 18.89% pass rate.

Models show significant domain bias with max coverage of 41.7%.

High variability in performance indicates reliance on pattern matching.

Abstract

Automated Theorem Proving (ATP) represents a core research direction in artificial intelligence for achieving formal reasoning and verification, playing a significant role in advancing machine intelligence. However, current large language model (LLM)-based theorem provers suffer from limitations such as restricted domain coverage and weak generalization in mathematical reasoning. To address these issues, we propose MSC-180, a benchmark for evaluation based on the MSC2020 mathematical subject classification. It comprises 180 formal verification problems, 3 advanced problems from each of 60 mathematical branches, spanning from undergraduate to graduate levels. Each problem has undergone multiple rounds of verification and refinement by domain experts to ensure formal accuracy. Evaluations of state-of-the-art LLM-based theorem provers under the pass@32 setting reveal that the best model achieves only an 18.89% overall pass rate, with prominent issues including significant domain bias (maximum domain coverage 41.7%) and a difficulty gap (significantly lower pass rates on graduate-level problems). To further quantify performance variability across mathematical domains, we introduce the coefficient of variation (CV) as an evaluation metric. The observed CV values are 4-6 times higher than the statistical high-variability threshold, indicating that the models still rely on pattern matching from training corpora rather than possessing transferable reasoning mechanisms and systematic generalization capabilities. MSC-180, together with its multi-dimensional evaluation framework, provides a discriminative and systematic benchmark for driving the development of next-generation AI systems with genuine mathematical reasoning abilities.