Large language models (LLMs) are increasingly used as graders, verifiers, and process auditors, but most mathematical evaluations still emphasize final-answer accuracy. This can obscure whether a model can verify a non-canonical but valid solution trace. We introduce a controlled linear-equation benchmark for evaluating LLMs in the evaluator role. Each instance asks the model to judge final-answer correctness, step-level trace correctness, and the first incorrect step. Our evaluation of state-of-the-art open LLMs reveals a significant robustness gap: models that accurately evaluate canonical solutions often fail when presented with perturbed but logically equivalent variants. Across GPT-OSS 20B, Qwen3-14B, and Phi-4-Reasoning, base models perform well on canonical traces but degrade substantially on perturbed traces, especially for error localization. On valid perturbed traces, base-model false-rejection rates reach 75.6-85.3%, showing strong sensitivity to canonical solution form. Supervised fine-tuning, distillation, and test-time compute improve robustness in some settings, but gains are model dependent and can trade off against canonical performance. The results show that reliable process-level verification remains challenging, and evaluator robustness should be measured separately from solver accuracy, even in a simple algebraic domain with exact ground truth.
Figures & tables
Figure 1: Robustness gap for base models. Final-answer evaluation is affected by solution perturbations, but the larger degradation occurs in first-error localization, indicating that the models often fail to separate valid non-canonical transformations from true errors.
Figure 2: Benchmark taxonomy. The same equation can appear with a canonical or perturbed trace and as T1, T2, or T3. This design separates final answer from trace correctness; the evaluation prompt does not contain underlined text.
Figure 3: Perturbation families. The first four panels are equivalence-preserving in the generated domain. Multiplication by a term and squaring both sides are candidate-generating transformations; they are accepted only when all resulting candidates are explicitly checked against the original equation.
Model
Outcome Accuracy ( Q1 )
Step-Level Accuracy ( Q2 )
Localization Accuracy ( Q3 )
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Baseline
Base
97.69
98.33
98.06
96.67
98.24
98.33
98.06
98.33
98.06
98.33
97.78
98.06
Base + TTC
85.83
100
99.17
58.33
99.35
100
98.89
99.17
80.09
100
77.50
61.94
FT
81.48
96.39
61.67
86.39
82.13
75.00
88.89
82.50
74.17
74.72
70.56
77.22
FT + TTC
68.98
97.50
36.67
72.78
69.72
93.89
51.11
64.17
66.39
96.11
41.11
61.94
TABLE I: Test accuracy (%) for GPT-OSS-20B-based models
Model
Outcome Accuracy ( Q1 )
Step-Level Accuracy ( Q2 )
Localization Accuracy ( Q3 )
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Baseline
Base
83.61
96.94
82.50
71.39
86.48
93.89
82.50
83.06
86.02
93.89
82.22
81.94
Base + TTC
86.85
100
99.17
61.39
99.63
100
98.89
100
92.41
100
90.83
86.39
FT
75.65
55.56
75.56
95.83
78.33
49.17
89.17
96.67
77.87
49.17
87.78
96.67
FT + TTC
87.31
80.83
84.44
96.67
93.70
83.33
98.61
99.17
93.61
85.00
97.78
97.78
TABLE II: Test accuracy (%) for Qwen3-14b-based models
Model
Outcome Accuracy ( Q1 )
Step-Level Accuracy ( Q2 )
Localization Accuracy ( Q3 )
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Overall
T1: Correct
T2: Incorrect
T3: Tricky
Baseline
Base
96.48
92.22
97.78
99.44
96.11
92.22
97.78
98.33
95.93
92.22
97.22
98.33
Base + TTC
65.56
98.61
91.11
6.94
90.74
99.74
91.11
82.67
42.78
100
15.83
12.50
FT
68.15
100.00
4.72
99.72
72.96
99.72
48.89
70.28
38.98
99.72
8.06
9.17
FT + TTC
66.67
100
0.00
100
33.33
100
0.00
0.00
33.33
100
0.00
0.00
TABLE III: Test accuracy (%) for Phi-4-Reasoning-based models
Large Language Models (LLMs) struggle to rigorously verify complex mathematical proofs. Standard global evaluation approaches suffer from "context poisoning," in which superficially plausible statements mask subtle logical flaws, leading to hallucination or over-skepticism. To address this, we shift from global evaluation to strict step-level verification: our framework maintains detailed context for each deduction step and strictly constrains the sources of applied theorems. We evaluate on a carefully curated adversarial diagnostic suite of research-level proofs drawn from the FirstProof challenge. A systematic ablation study demonstrates that these deductive constraints are indispensable, as unconstrained global prompting consistently fails to localize subtle logical errors. Beyond outperforming global evaluation, our approach fundamentally alters the failure taxonomy. Error analysis reveals that, rather than exhibiting severe logical hallucinations, remaining rejections are primarily instances of "pedantic hyper-rigor" stemming from unstated domain conventions, effectively exposing implicit ambiguities within the expert benchmark itself. Our findings suggest that prompting agents to organize their verification notes in a cautious, human-mathematician-like manner can substantially improve their ability to distinguish rigorous proofs from flawed ones, with the potential to strengthen agentic reasoning on frontier mathematical concepts that the base model does not already know well, and to lay a theoretical foundation for future automated proof-review systems. Code and prompts are available at GitHub.
With the growing popularity of Large Reasoning Models and their results in solving mathematical problems, it becomes crucial to measure their capabilities. We introduce a pipeline for both automatic and interactive verification as a more accurate alternative to only checking the answer which is currently the most popular approach for benchmarks. The pipeline can also be used as a generator of correct solutions both in formal and informal languages. 3 AI agents, which can be chosen for the benchmark accordingly, are included in the structure. The key idea is the use of prompts to obtain the solution in the specific form which allows for easier verification using proof assistants and possible use of small models (≤8B). Experiments on several datasets suggest low probability of False Positives. The open-source implementation with instructions on setting up a server is available at https://github.com/LogicEnj/lean4_verification_pipeline.
Varvara Sazonova, Dmitri Shmelkin, Stanislav Kikot +1
Moscow State University · Huawei Technologies Co., Ltd
Recent advancements in large language models have led to significant improvements across various tasks, including mathematical reasoning, which is used to assess models' intelligence in logical reasoning and problem-solving. Models are evaluated on mathematical reasoning benchmarks by verifying the correctness of the final answer against a ground truth answer. A common approach for this verification is based on symbolic mathematics comparison, which fails to generalize across diverse mathematical representations and solution formats. In this work, we offer a robust and flexible alternative to rule-based symbolic mathematics comparison. We propose an LLM-based evaluation framework for evaluating model-generated answers, enabling accurate evaluation across diverse mathematical representations and answer formats. We present failure cases of symbolic evaluation in two popular frameworks, Lighteval and SimpleRL, and compare them to our approach, demonstrating clear improvements over commonly used methods. Our framework enables more reliable evaluation and benchmarking, leading to more accurate performance monitoring, which is important for advancing mathematical problem-solving and intelligent systems.
Erez Yosef, Oron Anschel, Shunit Haviv Hakimi +4
Tel-Aviv University · Amazon Prime Video · Ben-Gurion University