internlm/AdvancedMathBench-AutoVerifier

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; requires sentencepiece and trust_remote_code=True after 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}
}