REVIEW 14 cited by
FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 14 Pith papers
-
FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.
-
What Current AI Benchmarks Leave Unmeasured: Modality, Search, Citations, and Implications (for Safety Evaluations)
Chat UI and API access to the same chatbot produce different accuracy, consistency, citation, and refusal behaviors on safety benchmarks, and web search changes these patterns further.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
StatEval: A Comprehensive Benchmark for Large Language Models in Statistics
StatEval is a new 16,000-question statistics benchmark showing that even strong LLMs score below 60% on research-level statistical proof tasks.
-
When Cars Have Stereotypes: Auditing Demographic Bias in Objects from Text-to-Image Models
A new audit framework, SODA, measures demographic bias in objects generated by text-to-image models and finds strong default-to-majority and stereotype-collapse patterns across five models.
-
CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
A critic model trained with reinforcement learning judges semantic correctness of Lean 4 formalizations, and using it as a filter sharply improves autoformalization accuracy.
-
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
A taxonomy-guided ensemble of LLM judges correlates with human ratings of autoformalizations (up to 0.662 on Isabelle/HOL) better than coarse-grained judges and reference metrics, but validation is partly in-sample an...
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
FMC: Formalization of Natural Language Mathematical Competition Problems
An LLM-based error-feedback pipeline produces FMC, a dataset of 3,922 Olympiad problems aligned with 9,787 Lean statements, claimed to be a challenging ATP benchmark.
-
Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
The paper advocates complete four-part benchmarks (formal/informal statements and proofs) for formal reasoning and reports that a published 97% autoformalization accuracy is actually 67% on expert review.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
-
GSM-Plus-BN: A Perturbation-Based Benchmark for Bangla Mathematical Reasoning in Large Language Models
The paper releases GSM-Plus-BN, a human-verified Bengali translation of the GSM-Plus perturbed math benchmark, and reports accuracy baselines for six open LLMs under standard and CoT prompting.
-
LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis
The paper's claim of pipeline-validated 'major conjecture' discovery is unsupported: the Lean statements are uninterpreted placeholders and the quality scores are self-assigned by the generating model.
-
Survey of Specialized Large Language Model
A survey of 24 specialized LLMs (2022-2025) claims a shift from domain fine-tuning to native architectures, but the synthesis is undermined by citation errors and selection bias.
Discussion (0). Continue with ORCID to comment.