AdvancedMathBench AutoVerifier
Paper · HF Paper · GitHub · Dataset · AutoVerifier
AutoVerifier evaluates natural-language mathematical proofs, explains errors, and identifies the earliest incorrect step. It serves as the automatic grader for AdvancedMathBench's ProverBench.
Model
- Architecture:
Qwen3_5MoeForConditionalGeneration. - Tokenizer: bundled
InternS1Tokenizer; requiressentencepieceandtrust_remote_code=Trueafter reviewing the tokenizer code. - Weights: 40 safetensors shards, approximately 68 GiB.
Input
Use proof_verifier.md with a problem, an optional reference solution, and a candidate proof split into zero-indexed steps. The following constructs the input without loading the model weights:
from pathlib import Path
from transformers import AutoTokenizer
model_dir = "." # Local model repository directory
tokenizer = AutoTokenizer.from_pretrained(model_dir, trust_remote_code=True)
steps = ["A candidate proof step.", "Another candidate proof step."]
proof = "\n\n".join(
f"<step{i}>\n\n{step}\n\n</step{i}>" for i, step in enumerate(steps)
)
template = Path(model_dir, "prompts/proof_verifier.md").read_text(encoding="utf-8")
prompt = template.format(
problem="The mathematical problem.", human_solution="", solution=proof,
)
text = tokenizer.apply_chat_template(
[{"role": "user", "content": prompt}],
tokenize=False, add_generation_prompt=True, enable_thinking=True,
)
Output and scoring
The final response contains an assessment, identified errors, and the first error index. For example, a no-error judgment is:
<assessment>The proof is correct.</assessment>
<errors></errors>
<first_error_step>-1</first_error_step>
-1 means no error was found; nonnegative indices identify the earliest error,
starting from 0. Parse the final answer after </think> when present.
ProverBench checks each proof 8 times and accepts it only when all eight
valid judgments report -1. Missing or malformed judgments do not count as
acceptance. Sampling settings are documented in
evaluation_settings.json.
Notes
AutoVerifier is a learned grader, not a formal proof checker, and can make errors. Tested package versions and validation scope are recorded in compatibility.json. License notices are provided in LICENSE and NOTICE.md.
Citation
If you use AdvancedMathBench AutoVerifier in your research, please cite:
@misc{kong2026advancedmathbenchbenchmarksuiteadvanced,
title = {AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification},
author = {Lingkai Kong and Zijian Wu and Yuzhe Gu and Haiteng Zhao and Wenyong Huang and Shuang Sun and Zhicheng Xiong and Xiaotian Zhang and Shuya Zhao and Yan Wang and Disheng Xu and Wenwei Zhang and Kai Chen},
year = {2026},
eprint = {2607.11849},
archivePrefix = {arXiv},
primaryClass = {cs.CL},
doi = {10.48550/arXiv.2607.11849},
url = {https://arxiv.org/abs/2607.11849}
}