InternLM 发布 AdvancedMathBench：评估大模型高等数学证明构建与验证能力

InternLM; AdvancedMathBench

Repository navigation

NotificationsYou must be signed in to change notification settings; Fork0 (0); Star0 (0)You must be signed in to star a repository

Repository files navigation

AdvancedMathBench evaluates whether language models can construct and verify natural-language proofs in advanced mathematics. It covers undergraduate-level (UG) and qualifying-examination-level (QE) mathematics, with problems drawn from examinations, mathematics competitions, and textbooks.

ProverBench contains 245 expert-reviewed problems for proof generation; VerifierBench contains 888 proof trajectories with full-chain expert annotations, including fatal errors, recoverable errors, and explanations; AutoVerifier is a trained proof verifier for automated ProverBench evaluation. The default pessimistic protocol accepts a proof only when all eight judgments accept it. VerifierBench additionally uses meta-verification to assess whether a model's error analysis agrees with expert annotations

Figure 1. Model performance on AdvancedMathBench. Left: proof-generation performance compared with HMMT and USAMO. Right: meta-verification TPR and TNR; marker labels show Balanced F1.

Figure 2. Overview of benchmark construction and the automatic verification pipeline.

The overview and results below follow the final manuscript dated September 28, 2026. The initial arXiv version describes an earlier ProverBench revision; see release notes for version details.

Main results (Table 1)

Main results on ProverBench and VerifierBench from the final manuscript, in percent. ProverBench uses pessimistic proof acceptance. VerifierBench reports both correct/incorrect polarity (Rough) and agreement with expert error analyses (Meta-Verification). Bal. F1 is the harmonic mean of TPR and TNR.

Strong proof generation does not necessarily imply strong proof verification. Binary verdict accuracy can also hide incorrect error explanations. See the results notes for metric definitions and reproduction scope.

Quick start

Python 3.10+ is required. Run the following commands from this repository's root. The API evaluator has no internal-repository dependencies and uses the Python standard library; the hub extra installs the Hugging Face download tools.

This downloads both benchmark files at a pinned revision and checks their SHA256 hashes. If access requires authentication, run hf auth login first with an authorized account. See data documentation.

ProverBench

Configure an API prover and an AutoVerifier endpoint:

--dry-run validates inputs and shows the call budget without calling models. Remove it to run evaluation. Each of the four generated proofs per problem receives eight independent verifier judgments. The example requires a deployed AutoVerifier; it does not start a model server.

VerifierBench

Configure the model to evaluate as a verifier:

Remove --dry-run to run. For explanation-quality evaluation, use configs/verifier_meta.example.json with --meta; the manuscript uses gpt-oss-120b as the meta-verifier.

See the evaluation guide for meta-verification, local model loading, domain filters, outputs, and resuming. The metrics reference defines scoring and invalid-output handling. CLI scores are on 0–1; paper tables use percentages. Example settings are not a turnkey reproduction of paper results.

AutoVerifier

The model repository contains the checkpoint, tokenizer, and proof-verification prompt. To download the pinned checkpoint separately:

The checkpoint is approximately 68 GiB. Optional local inference uses public Transformers; see the setup and compatibility notes before loading it. Full GPU inference has not been validated by the offline tests.

Repository layout

Run tests with python -m unittest discover -s tests -v. See validation for the tested scope.

Licensing

No code license is declared at this time. Dataset and model terms are separate; see licensing notes and the respective Hugging Face repositories.

Citation

If you use AdvancedMathBench, please cite the paper. The citation below follows the current arXiv author list. Also available as BibTeX and CITATION.cff.