paper web signal

AdvancedMathBench: top model verifies proofs at only F1 65.1

TL;DR

  • On ProverBench's 296 problems, the best model GPT-5.5-xhigh reached 75.8 on the undergraduate split and 66.1 on the qualifying-exam split.
  • On VerifierBench's 888 expert-annotated proof trajectories, the best model attained a Balanced F1 of only 65.1 for judging proof correctness.
  • Models generally exhibited low true negative rates, meaning identifying invalid proofs is the specific bottleneck rather than solving the problem.

A new benchmark posted to arXiv tries to answer a question that usually gets skipped in the leaderboard chase: not "can the model solve a hard math problem," but "can the model tell whether a proof is actually correct." The answer, at least on these tests, is not really.

The benchmark, AdvancedMathBench, has two pieces. ProverBench is 296 problems spanning undergraduate and doctoral qualifying-exam levels. VerifierBench is a different thing entirely: 888 model-generated proof trajectories paired with expert ground truth. One tests whether the model can write a proof. The other tests whether it can grade one. The authors frame the split as a response to prior benchmarks that "often rely on final-answer correctness or coarse judgments," which leaves the validity of the reasoning process itself under-tested.

The numbers are the interesting part. The best model in their evaluation, which they label GPT-5.5-xhigh, scored 75.8 on the undergraduate split and 66.1 on the qualifying-exam split. Those are not embarrassing for advanced mathematics, but they are a long way from "reliable." The verification result is starker. On VerifierBench the best model reached a Balanced F1 of only 65.1, and the authors flag that models "generally exhibit low true negative rates," which means the specific weakness is catching proofs that are actually wrong rather than the arithmetic of scoring.

The honest caveat is that this is one paper, one benchmark, and the model naming is the authors' own label rather than a vendor-verifiable identifier. What the reporting doesn't give you is a per-topic breakdown, or how tool-augmented approaches like Lean or Coq integration would move the verifier score.

If you are building anything that leans on an LLM to grade mathematical or logical reasoning — tutoring products, research pipelines, curated proof datasets — this is the number that matters more than the prover score. Formal-methods tooling looks better positioned this week than it did last.