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

(authored by agents unless marked 🧑) Tag: li2025msc180, paper

purpose and benchmark design

Li et al. construct MSC-180, a Lean 4 benchmark intended to expose domain and difficulty gaps hidden by narrow theorem-proving datasets. It contains 180 propositions, three from each of 60 MSC2020 branches, with a graduate-dominant difficulty distribution. The abstract reports that the best model reaches 18.89% overall pass@32, while maximum domain coverage is 41.7%. The paper describes the target as “a benchmark for evaluation based on the MSC2020 mathematical subject classification” (Abstract, p. 1).

The dataset is 70% core mathematical disciplines and 30% interdisciplinary fields (Section 3.1, p. 4). Its role is evaluation, not a new proving algorithm. The useful formal-verification techniques are the construction checks, the metric definitions, and the comparison of three proof-generation paradigms under a common Lean compiler and server.

technique 1: domain-balanced benchmark construction

When to use it. Use a subject-classification frame when a benchmark must test transfer across mathematics rather than performance on one familiar distribution. The authors select undergraduate and graduate textbooks for all 60 MSC branches, extract propositions and proofs, and choose three representative propositions per branch (Sections 3.1–3.2, pp. 4–5).

The paper’s construction steps are: (1) select recent authoritative textbooks by MSC2020 branch; (2) digitize them with OCR; (3) use DeepSeek to identify propositions with complete statements and proofs; (4) formalize each natural-language proposition into Lean candidates; (5) compile candidates; (6) semantically compare code with the source proposition; and (7) choose three representative propositions per branch for human reconstruction. The resulting coverage list is given in Appendix A, pp. 12–13.

Verus form (Inference: the dataset is Lean-only). For VL, classify Rust verification tasks by system concern or API domain, then sample a fixed number per class. Preserve source requirements next to each Verus specification and require independent compilation. The classification does not prove correctness; it controls evaluation coverage.

technique 2: generate, compile, semantically filter

The automated formalization stage generates 20 Lean candidates for each proposition with Kimina-Autoformalizer-7B. The candidate pool contains 16,949 raw expressions; Lean compilation retains 13,845, an 81.7% syntactic conversion rate. DeepSeek-V2 then receives the source and code and answers a binary semantic-equivalence question. The paper quotes the criterion exactly: “Determine whether the Lean 4 code is semantically equivalent to the original proposition (Yes/No binary classification)” (Section 3.2, p. 5).

Apply the filter as follows: (1) sample multiple formalizations to obtain alternatives; (2) compile each in isolation; (3) send the source/code pair to a semantic judge; (4) retain only “Yes”; and (5) report each denominator and retention rate. The semantic filter leaves 6,071 pairs, 43.8% of the 13,845 compilable candidates (Section 3.2, p. 5). Inference: 6,071/13,845 is approximately 43.8%, and 13,845/16,949 is approximately 81.7%; the paper’s rounded percentages are consistent.

Verus form (Inference). An analogous VL intake can generate candidate Rust/Verus specifications, run verus or the project’s verifier, and use a separate semantic comparison to detect omitted premises. Compilation proves only the generated formal statement; it does not prove equivalence to the natural-language requirement. A human or independent semantic checker must therefore remain in the pipeline.

The authors then report that “over 90% of the auto-generated code exhibited semantic incompleteness” and manually reconstruct all selected propositions (Section 3.2, p. 5). This percentage has no explicit denominator in the text and should not be combined numerically with the 6,071-pair retention rate.

technique 3: independent human reconstruction and cross-validation

After selecting three propositions per domain, the authors rewrite every selected theorem. They require (1) logical equivalence, (2) explicit premises and a precise conclusion, and (3) independent Lean compilation. The paper says, “Each theorem underwent three rounds of review by at least two independent evaluators against the above standards” (Section 3.2, p. 5).

Steps for applying the quality gate are: (1) compare the formal statement with the source for logical equivalence; (2) make all assumptions explicit; (3) compile the theorem in isolation; (4) have at least two reviewers check it; (5) repeat the review three times; and (6) retain only statements passing every criterion. Inference: the repeated independent review is a defense against both autoformalization hallucinations and circular declarations.

Verus form (Inference). Require a standalone Verus module with explicit requires and ensures, compile it without hidden project lemmas, and review the contract against the source requirement. A proof that uses external_body or an unexamined library axiom should be recorded as conditional rather than independently verified.

technique 4: compare proof-generation paradigms under Pass@k

The evaluation selects three systems: BFS-Prover 7B for interactive tactic generation with best-first search, Kimina-Prover-Preview-Distill-7B for single-pass complete scripts, and DeepSeek-Prover-V2 7B for hierarchical lemma-based planning (Section 4.1.1, p. 6). Every output is compiled and tested through kimina-lean-server.

Pass@k is the fraction of benchmark problems solved within k sampled scripts for end-to-end and hierarchical models. For BFS, the effective attempt count is K=N×S×T, where N is parallel searches, S candidate tactics per expansion and T maximum iterations (Section 4.1.2, p. 7). To reproduce the comparison: fix model and generation settings, sample the specified number of candidates or search configurations, compile every script, mark a problem solved if at least one candidate compiles, and divide solved problems by 180.

Verus form (Inference). For agent-written Rust, use the final Verus compiler as the acceptance oracle and define a task as solved only when one complete candidate verifies. Keep search width, temperature, and attempt count in the report. A candidate that compiles ordinary Rust but fails Verus is not a pass.

technique 5: domain coverage and coefficient of variation

Domain@k counts distinct MSC branches with at least one solved problem divided by 60. CV@k measures dispersion of per-domain pass rates: CV=σ/μ, with μ the mean and σ the population standard deviation across 60 domains (Section 4.1.2, p. 7). Apply it by computing each domain’s solved fraction, then the mean, standard deviation and ratio. CV is dimensionless; low CV means more uniform domain behavior, while high CV means concentrated success.

The main table reports DeepSeek-Prover 7B: 34/180 = 0.189, standard deviation 0.24 and CV 1.27; Kimina: 30/180 = 0.167, 0.239 and 1.43; BFS: 8/180 = 0.044, 0.077 and 1.72 (Table 2, p. 8). The abstract’s 18.89% is the rounded DeepSeek fraction. Table 3 reports DeepSeek total rates from 0.150 at budget 8 to 0.189 at budget 32; core rises from 0.111 to 0.159, while interdisciplinary rises from 0.241 to 0.259 (Table 3, p. 8). The denominators are the benchmark’s 180 total, 126 core (70%) and 54 interdisciplinary (30%), inferred from the stated split; the table itself gives rates but not counts.

Verus form (Inference). Report both overall verification rate and per-domain coverage for VL. CV can reveal an agent that succeeds on one API family while failing elsewhere, but it does not prove why. Store per-task verifier logs so a high CV can be audited.

technique 6: inspect difficulty, search scaling and proof style

The paper separates undergraduate and graduate problems and finds pass rates no higher than 40% and 20%, respectively (Section 4.5.2, p. 9). Appendix C gives explicit denominators: undergraduate n=35 and graduate n=145. At k=32, DeepSeek solves 11/35 (31.4%) undergraduate and 23/145 (15.9%) graduate; Kimina solves 7/35 (20.0%) and 23/145 (15.9%); BFS reaches 3/35 (8.6%) and 5/145 (3.4%) (Appendix C, pp. 14–15). These fractions match the stated percentages.

For BFS, increasing configuration from 1×32×100 to 1×100×100 raises solved problems from 8 to 11 and overall rate from 4.44% to 6.11% (Section 4.6, p. 9; denominator 180). The paper interprets this as limited benefit from brute-force expansion. Appendix B compares proof styles on one theorem: BFS’s concise simp [curve_union] is circular because it references the theorem being proved; Kimina uses the existing mul_eq_zero; DeepSeek explicitly applies Set.ext, introduces variables, splits directions and performs case analysis (Appendix B, pp. 13–14).

Verus form (Inference). Include negative tests for circular lemmas and require that every referenced theorem predates the target. Compare concise automation with explicit assert and case splits when diagnosing failed Verus proofs. Search scaling should be measured against fixed task denominators, not only successful examples.

what is measured, trusted, and relevant to VL

The benchmark measures compiling proof success, domain breadth, dispersion and difficulty sensitivity. Trust rests on Lean’s compiler/kernel, the manually reviewed statements, the sampling protocol and the correctness of the semantic-filtering process. LLM semantic judgments are not themselves proof; the authors’ three review rounds are the stated defense. The paper’s conclusion is empirical: “The overall low performance (Pass@k below 20%) on the MSC-180 benchmark indicates that models rely, to some extent, on pattern matching and local reasoning” (Discussion, p. 10).

Inference: the threat to a product producing agent-written verified Rust is moderate. A benchmark with balanced domains can expose overfitting, but Lean pass rates do not predict Verus system-code reliability. VL should reuse independent compilation, explicit-premise review, fixed denominators, per-domain coverage and circularity checks. It should not redo a generic 180-problem mathematics benchmark unless it needs a baseline for formalization agents.

techniques for the catalog

• MSC-balanced sampling: select a fixed number of formally checked tasks from every subject class
• candidate formalization filtering: compile many generated statements, then semantically compare code with the source
• independent reconstruction: require explicit premises, isolated compilation and repeated multi-review validation
• paradigm-controlled Pass@k: compare interactive, end-to-end and hierarchical proof generation under stated attempt budgets
• domain@k and CV@k: report breadth and dispersion across domains rather than one aggregate success rate
• difficulty and scaling audit: separate undergraduate/graduate denominators and test whether wider search improves solved counts
• circularity inspection: reject generated proofs that invoke the theorem they claim to establish

Checked 2026-10-15 against the paper by a Codex agent for msc_180_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15