Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs

Azim Ospanov; Zijin Feng; Ding Ding; Chengwu Liu; Haoli Bai; Jiacheng Sun; Lifeng Shang; Farzan Farnia

cs.AIOct 27, 2026

Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs

Authors: Azim Ospanov, Zijin Feng, Ding Ding, Chengwu Liu, Haoli Bai, Jiacheng Sun, Lifeng Shang, Farzan Farnia

Organizations: Huawei Foundation Model Department · The Chinese University of Hong Kong · The Hong Kong University of Science and Technology

Abstract

Large Language Models (LLMs) have made remarkable progress on solving competition-level mathematics, yet their ability to verify natural-language mathematical proofs remains relatively underexplored. This gap is especially pronounced for Olympiad-level proofs, which require meticulous assessment of each claim in a long reasoning chain. Current proof verification thus primarily relies on expert inspection, which is costly to scale. In this paper, we present a systematic study of LLM-based verification in this setting. Specifically, we introduce a human-curated dataset of USAMO 2025 candidate solutions with expert grading, and conduct a broad evaluation of existing LLM verifiers across frontier models. We also propose TROJAN, an iterative self-critique pipeline for generating high-fidelity adversarial proofs at scale. Our comprehensive evaluation covers 20 models spanning seven metrics, two prompt styles, three inference methods, and three prompt templates, showing that state-of-the-art models still leave considerable room for improvement. To narrow this gap, we propose MABGrader, a Multi-Armed Bandit framework that reframes grading as arm selection over the discrete score space. MABGrader outperforms the SOTA ProofGrader by 26.4% in Quadratic Weighted Kappa and reduces grading error by 14%. Code and dataset are available at https://github.com/aziksh-ospanov/TROJAN.

Figures & tables

Figure 1: Performance of models on Trojan-Bench(H) , comparing Majority@16 with our MABGr. inference method across 4 metrics. Color and marker size denotes the model and parameter scale, resp. The spread indicates considerable room for improvement, while MABGr. show consistent gains.

Panel of Figure 2 — Figure 2: Example verification inputs for USAMO 2025 Problem 1 under the Full and Blind settings. In the Full setting, the verifier receives the problem, reference solution, marking scheme, and candidate solution. In the Blind setting, the verifier receives only the problem and candidate solution.

Metric	QWK	Pearson $r$	RMSE	MAE	WTA ≤1	WTA ≤2	Exact Match	Bias
Value	0.76	0.89	1.09	0.62	0.85	0.94	0.58	$\pm 0.08$

Table 1: Inter-annotator agreement on our human-curated benchmark Trojan-Bench(H)

Figure 3: Overview of our synthetic data generation pipeline TROJAN . Given a problem, reference solution, marking scheme, and target score profile, the pipeline injects rubric-aligned errors, performs iterative self-critique and refinement, and outputs an adversarial proof with a grade justification.

Metric	QWK	Pearson $r$	RMSE	MAE	WTA ≤1	WTA ≤2	Exact Match	Bias
Value	0.78	0.87	1.20	0.77	0.83	0.90	0.67	0.11

Table 2: Correlation and agreement of the synthetically-generated benchmark Trojan-Bench(S) with expert graders.

Metric	QWK	Pearson $r$	RMSE	MAE	WTA ≤1	WTA ≤2	Exact Match	Bias
Value	0.78	0.94	0.70	0.49	1.00	1.00	0.51	$\pm 0.00$

Table 3: Inter-annotator agreement on the synthetically-generated benchmark Trojan-Bench(S) .

Figure 4: Model correlation with human labels using QWK across Full and Blind settings. The bar plots report CoT@1, MeanCoT@16, and MajorityVote@16 for each tested model.

Figure 5: Grading performance on human and synthetic USAMO 2025 subsets ( $N=48$ ). Reported values represent the outcome of MajorityVote@16 across QWK, RMSE, and Bias metrics.

	Full Setting			Blind Setting
	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )
Qwen3.5-9B (Base)	0.02	4.00	3.23	0.06	2.52	0.63
Qwen3.5-9B (SFT)	0.35	2.08	0.27	0.07	2.40	0.39
Qwen3.5-27B (Base)	0.36	2.98	1.54	-0.11	4.12	-3.40
Qwen3.5-27B (SFT)	0.47	2.10	0.77	0.06	2.50	0.21

Table 4: Comparative performance of base and fine-tuned models on TROJAN synthetic samples.

		QWK $\uparrow$			RMSE $\downarrow$			Bias
	$n_{\text{align}}\!\rightarrow$	1	2	3	1	2	3	1	2	3
$n_{\text{iter}}$	1	0.583	—	—	1.414	—	—	0.400	—	—
	3	0.579	0.833	0.776	1.265	0.894	1.049	0.400	0.000	0.100
	5	0.757	0.884	0.818	0.949	0.707	0.894	0.300	0.100	0.000
	7	0.694	0.683	0.717	1.225	1.140	1.342	0.700	0.500	0.600
	9	0.571	0.735	0.622	1.225	1.140	1.304	-0.300	0.100	0.700

Table 5: Sensitivity of QWK, RMSE, and Bias to

n_{\text{iter}}

and

n_{\text{align}}

	QWK ( $\uparrow$ )				RMSE ( $\downarrow$ )				Bias ( $\approx 0$ )
	DS V4F	Kimi K2.5	Gem. 3P	Q3.5 27B	DS- V4F	Kimi K2.5	Gem. 3P	Q3.5 27B	DS- V4F	Kimi K2.5	Gem. 3P	Q3.5 27B
Chain-of-Thought (CoT@1)
MathArena [ 4 ]	0.59	0.20	0.45	0.33	2.28	3.29	2.50	3.37	-0.69	2.24	1.35	1.73
ProofGr. [ 33 ]	0.64	0.24	0.46	0.36	2.15	3.06	2.51	3.10	-0.81	2.14	1.59	2.02
ProofAGr. [ 32 ]	0.52	0.19	0.42	0.32	2.47	3.47	2.84	3.60	-1.15	2.86	1.78	1.97
Chain-of-Thought with Majority Vote Selection (MajorityVote@16)

Table 6: Performance on the manually annotated USAMO 2025 dataset in the Full setting, where models are given a reference solution and marking scheme. We report QWK, RMSE, and Bias for four base models: DeepSeek-V4-Flash, Kimi-K2.5, Gemini-3-Pro-Preview, and Qwen3.5-27B.

Appendix figures & tables61 assets

Supplementary material from the paper’s appendix.

Appendix

Questions	Answers
Motivation
For what purpose was the dataset created?	The dataset was developed to benchmark the performance of current Large Language Models in grading and evaluating Olympiad-level mathematical proofs.
Who created the dataset and on behalf of which entity?	The authors of this paper.
Who funded the creation of the dataset?	The company where the authors work.
Any other comment?	None.
Composition

Appendix

Table 7: Datasheet for our expert annotated dataset

Questions	Answers
Motivation
For what purpose was the dataset created?	The dataset was developed to benchmark the performance of current Large Language Models in grading and evaluating Olympiad-level mathematical proofs.
Who created the dataset and on behalf of which entity?	The authors of this paper.
Who funded the creation of the dataset?	The company where the authors work.
Any other comment?	None.
Composition

Appendix

Table 8: Datasheet for our synthetically generated dataset using TROJAN .

Error Type	Count	Percentage
Logical gap	27	35.06%
Misapplied theorem	18	23.38%
Conceptual error	12	15.58%
Computational slip	8	10.39%
Incomplete justification	6	7.79%
None	6	7.79%

Appendix

Table 9: Distribution of injected error types in Trojan-Bench(H) . We report them as absolute counts and percentages.

	Trojan-Bench(H)		Trojan-Bench(S)
Model	Full	Blind	Full	Blind	Max tokens
Claude-Sonnet-4.6 [ 2 ] ( T )	✓	✓	$-$	$-$	65,536
Claude-Sonnet-4.6 [ 2 ] ( T )	✓	✓	✓	✓	23,625
DeepSeek-V3.2 [ 12 ] ( T )	✓	✓	✓	$-$	8,192
DeepSeek-V3.2 [ 12 ] ( T )	✓	✓	✓	$-$	65,536
DeepSeek-V4-Flash [ 11 ] ( T )	✓	✓	$-$	$-$	65,536

Appendix

Table 10: The list of all 20 evaluated models. A ✓ marks the presence of a sampling_grades.csv-producing run for the indicated (dataset, style) pair. In total 52 model

\times

(dataset, style) runs are reported. The last column reports the maximum completion_tokens .

Model	Pearson $r$	Kendall $\tau$	QWK	MAE
Claude-Sonnet-4.6 ( T )	0.554 $\pm$ 0.025	0.451 $\pm$ 0.026	0.446 $\pm$ 0.024	1.785 $\pm$ 0.070
Claude-Sonnet-4.6 ( T )	0.604 $\pm$ 0.046	0.506 $\pm$ 0.043	0.513 $\pm$ 0.043	1.623 $\pm$ 0.087
DeepSeek-V3.2 ( T )	0.435 $\pm$ 0.011	0.342 $\pm$ 0.009	0.289 $\pm$ 0.008	2.292 $\pm$ 0.025
DeepSeek-V3.2 ( T )	0.622 $\pm$ 0.065	0.526 $\pm$ 0.058	0.613 $\pm$ 0.066	1.357 $\pm$ 0.136
deepseek-v4-flash-nothinking	0.347 $\pm$ 0.014	0.286 $\pm$ 0.020	0.228 $\pm$ 0.010	2.363 $\pm$ 0.030
DeepSeek-V4-Flash ( T )	0.656 $\pm$ 0.012	0.544 $\pm$ 0.015	0.631 $\pm$ 0.021	1.375 $\pm$ 0.029

Appendix

Table 11: Mean

\pm

standard deviation of Pearson

r

, Kendall

\tau

, QWK, and MAE across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset against a standard markscheme and golden solution.

Model	RMSE	Bias	Exact
Claude-Sonnet-4.6 ( T )	2.408 $\pm$ 0.050	1.349 $\pm$ 0.085	0.228 $\pm$ 0.045
Claude-Sonnet-4.6 ( T )	2.227 $\pm$ 0.096	1.177 $\pm$ 0.110	0.277 $\pm$ 0.038
DeepSeek-V3.2 ( T )	3.068 $\pm$ 0.022	2.073 $\pm$ 0.035	0.238 $\pm$ 0.011
DeepSeek-V3.2 ( T )	2.117 $\pm$ 0.201	0.260 $\pm$ 0.207	0.414 $\pm$ 0.039
deepseek-v4-flash-nothinking	3.158 $\pm$ 0.029	2.058 $\pm$ 0.036	0.232 $\pm$ 0.022
DeepSeek-V4-Flash ( T )	2.111 $\pm$ 0.061	-0.615 $\pm$ 0.165	0.380 $\pm$ 0.020

Appendix

Table 12: Mean

\pm

standard deviation of RMSE, bias, and exact-match accuracy across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE
Claude-Sonnet-4.6 ( T )	0.379 $\pm$ 0.043	0.293 $\pm$ 0.061	0.349 $\pm$ 0.049	1.797 $\pm$ 0.057
Claude-Sonnet-4.6 ( T )	0.584 $\pm$ 0.100	0.481 $\pm$ 0.131	0.497 $\pm$ 0.100	1.646 $\pm$ 0.188
DeepSeek-V3.2 ( T )	0.151 $\pm$ 0.115	0.089 $\pm$ 0.079	0.053 $\pm$ 0.045	3.012 $\pm$ 0.097
DeepSeek-V3.2 ( T )	0.514 $\pm$ 0.072	0.399 $\pm$ 0.064	0.456 $\pm$ 0.069	1.699 $\pm$ 0.111
deepseek-v4-flash-nothinking	0.164 $\pm$ 0.125	0.112 $\pm$ 0.124	0.071 $\pm$ 0.058	2.776 $\pm$ 0.036
DeepSeek-V4-Flash ( T )	0.468 $\pm$ 0.072	0.361 $\pm$ 0.054	0.396 $\pm$ 0.058	2.146 $\pm$ 0.143

Appendix

Table 13: Mean

\pm

standard deviation of Pearson

r

, Kendall

\tau

Model	RMSE	Bias	Exact
Claude-Sonnet-4.6 ( T )	2.292 $\pm$ 0.052	-0.422 $\pm$ 0.086	0.214 $\pm$ 0.046
Claude-Sonnet-4.6 ( T )	2.006 $\pm$ 0.238	-0.609 $\pm$ 0.437	0.146 $\pm$ 0.055
DeepSeek-V3.2 ( T )	3.683 $\pm$ 0.107	-2.832 $\pm$ 0.103	0.133 $\pm$ 0.020
DeepSeek-V3.2 ( T )	2.243 $\pm$ 0.128	-0.871 $\pm$ 0.139	0.227 $\pm$ 0.048
deepseek-v4-flash-nothinking	3.476 $\pm$ 0.067	-2.505 $\pm$ 0.075	0.156 $\pm$ 0.036
DeepSeek-V4-Flash ( T )	2.798 $\pm$ 0.151	-1.406 $\pm$ 0.027	0.229 $\pm$ 0.017

Appendix

Table 14: Mean

\pm

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.54	0.44	0.44	1.79	2.43	1.33	0.56
Claude-Sonnet-4.6 ( T )	0.55	0.45	0.47	1.73	2.40	1.24	0.58
DeepSeek-V3.2 ( T )	0.43	0.35	0.29	2.27	3.04	2.02	0.48
DeepSeek-V3.2 ( T )	0.60	0.53	0.59	1.35	2.26	0.27	0.71
DeepSeek-V4-Flash ( T )	0.66	0.54	0.64	1.33	2.08	-0.50	0.69
Gemini-2.5-Flash	0.62	0.50	0.59	1.54	2.23	0.63	0.58

Appendix

Table 15: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.57	0.47	0.46	1.69	2.35	1.31	0.60
Claude-Sonnet-4.6 ( T )	0.65	0.53	0.55	1.54	2.13	1.17	0.60
DeepSeek-V3.2 ( T )	0.44	0.34	0.29	2.29	3.06	2.08	0.48
DeepSeek-V3.2 ( T )	0.65	0.53	0.65	1.35	1.93	0.23	0.67
DeepSeek-V4-Flash ( T )	0.72	0.59	0.69	1.25	1.87	-0.67	0.69
Gemini-2.5-Flash	0.69	0.57	0.68	1.23	1.76	0.44	0.73

Appendix

Table 16: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.58	0.47	0.46	1.75	2.37	1.38	0.58
Claude-Sonnet-4.6 ( T )	0.61	0.53	0.52	1.65	2.25	1.23	0.56
DeepSeek-V3.2 ( T )	0.44	0.34	0.29	2.29	3.08	2.08	0.48
DeepSeek-V3.2 ( T )	0.66	0.57	0.65	1.27	2.05	0.10	0.67
DeepSeek-V4-Flash ( T )	0.65	0.54	0.63	1.38	2.13	-0.54	0.65
Gemini-2.5-Flash	0.67	0.57	0.64	1.38	2.14	0.63	0.69

Appendix

Table 17: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.40	0.32	0.38	1.77	2.24	-0.31	0.44
Claude-Sonnet-4.6 ( T )	0.49	0.34	0.46	1.60	1.97	0.16	0.56
DeepSeek-V3.2 ( T )	0.15	0.04	0.06	2.96	3.64	-2.71	0.29
DeepSeek-V3.2 ( T )	0.57	0.50	0.51	1.54	2.12	-0.88	0.56
DeepSeek-V4-Flash ( T )	0.40	0.31	0.34	2.25	2.94	-1.38	0.46
Gemini-2.5-Flash	0.42	0.32	0.43	1.86	2.39	-0.01	0.46

Appendix

Table 18: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.39	0.31	0.35	1.77	2.22	-0.40	0.44
Claude-Sonnet-4.6 ( T )	0.48	0.36	0.40	1.63	2.03	-0.21	0.50
DeepSeek-V3.2 ( T )	0.20	0.12	0.06	3.00	3.63	-2.83	0.31
DeepSeek-V3.2 ( T )	0.61	0.48	0.52	1.52	2.03	-0.85	0.60
DeepSeek-V4-Flash ( T )	0.51	0.39	0.42	2.04	2.67	-1.46	0.50
Gemini-2.5-Flash	0.44	0.33	0.43	1.75	2.29	-0.25	0.54

Appendix

Table 19: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.46	0.38	0.42	1.67	2.15	-0.46	0.48
Claude-Sonnet-4.6 ( T )	0.47	0.35	0.40	1.63	2.03	-0.13	0.54
DeepSeek-V3.2 ( T )	0.09	0.06	0.02	3.15	3.83	-3.02	0.29
DeepSeek-V3.2 ( T )	0.59	0.48	0.49	1.58	2.18	-1.08	0.58
DeepSeek-V4-Flash ( T )	0.49	0.39	0.42	2.10	2.74	-1.35	0.48
Gemini-2.5-Flash	0.38	0.29	0.38	1.85	2.56	-0.06	0.52

Appendix

Table 20: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the human-labelled Trojan-Bench(H) dataset without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE
Claude-Sonnet-4.6 ( T )	0.772 $\pm$ 0.067	0.677 $\pm$ 0.079	0.713 $\pm$ 0.075	0.843 $\pm$ 0.157
DeepSeek-V3.2 ( T )	0.729 $\pm$ 0.007	0.630 $\pm$ 0.007	0.423 $\pm$ 0.007	2.008 $\pm$ 0.018
DeepSeek-V3.2 ( T )	0.768 $\pm$ 0.019	0.652 $\pm$ 0.021	0.724 $\pm$ 0.019	1.020 $\pm$ 0.039
DeepSeek-V4-Flash ( T )	0.587 $\pm$ 0.042	0.488 $\pm$ 0.037	0.533 $\pm$ 0.036	1.380 $\pm$ 0.051
GPT-4o	0.527 $\pm$ 0.007	0.454 $\pm$ 0.004	0.120 $\pm$ 0.003	3.371 $\pm$ 0.009
GPT-5	0.745 $\pm$ 0.018	0.626 $\pm$ 0.017	0.658 $\pm$ 0.012	1.121 $\pm$ 0.039

Appendix

Table 21: Mean

\pm

standard deviation of Pearson

r

, Kendall

\tau

, QWK, and MAE across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , against a standard markscheme and golden solution.

Model	RMSE	Bias	Exact
Claude-Sonnet-4.6 ( T )	1.256 $\pm$ 0.189	0.609 $\pm$ 0.093	0.436 $\pm$ 0.080
DeepSeek-V3.2 ( T )	2.337 $\pm$ 0.020	1.978 $\pm$ 0.018	0.080 $\pm$ 0.005
DeepSeek-V3.2 ( T )	1.398 $\pm$ 0.052	0.093 $\pm$ 0.037	0.312 $\pm$ 0.016
DeepSeek-V4-Flash ( T )	1.848 $\pm$ 0.068	-0.530 $\pm$ 0.041	0.237 $\pm$ 0.006
GPT-4o	3.628 $\pm$ 0.010	3.371 $\pm$ 0.009	0.005 $\pm$ 0.000
GPT-5	1.549 $\pm$ 0.022	0.769 $\pm$ 0.038	0.312 $\pm$ 0.019

Appendix

Table 22: Mean

\pm

standard deviation of RMSE, bias, and exact-match accuracy across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE
Claude-Sonnet-4.6 ( T )	0.507 $\pm$ 0.067	0.411 $\pm$ 0.058	0.493 $\pm$ 0.058	1.188 $\pm$ 0.066
DeepSeek-V4-Flash ( T )	0.464 $\pm$ 0.044	0.367 $\pm$ 0.044	0.432 $\pm$ 0.041	1.561 $\pm$ 0.054
GPT-4o	0.427 $\pm$ 0.005	0.368 $\pm$ 0.015	0.120 $\pm$ 0.003	3.034 $\pm$ 0.010
GPT-5	0.490 $\pm$ 0.024	0.397 $\pm$ 0.031	0.459 $\pm$ 0.025	1.341 $\pm$ 0.079
GPT-5-Mini	0.503 $\pm$ 0.013	0.394 $\pm$ 0.014	0.423 $\pm$ 0.012	1.538 $\pm$ 0.029
Kimi-K2.5	0.452 $\pm$ 0.035	0.352 $\pm$ 0.018	0.391 $\pm$ 0.031	1.590 $\pm$ 0.052

Appendix

Table 23: Mean

\pm

standard deviation of Pearson

r

, Kendall

\tau

, QWK, and MAE across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , without access to a standard markscheme and golden solution.

Model	RMSE	Bias	Exact
Claude-Sonnet-4.6 ( T )	1.563 $\pm$ 0.065	0.267 $\pm$ 0.235	0.264 $\pm$ 0.029
DeepSeek-V4-Flash ( T )	1.994 $\pm$ 0.082	-0.374 $\pm$ 0.058	0.203 $\pm$ 0.037
GPT-4o	3.332 $\pm$ 0.011	2.986 $\pm$ 0.013	0.031 $\pm$ 0.003
GPT-5	1.709 $\pm$ 0.067	0.576 $\pm$ 0.043	0.212 $\pm$ 0.033
GPT-5-Mini	1.943 $\pm$ 0.031	0.990 $\pm$ 0.045	0.193 $\pm$ 0.030
Kimi-K2.5	1.978 $\pm$ 0.076	0.892 $\pm$ 0.016	0.175 $\pm$ 0.018

Appendix

Table 24: Mean

\pm

standard deviation of RMSE, bias, and exact-match accuracy across individual CoT sampling attempts per problem. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.81	0.73	0.75	0.78	1.12	0.61	0.80
DeepSeek-V3.2 ( T )	0.72	0.62	0.42	2.01	2.35	1.98	0.36
DeepSeek-V3.2 ( T )	0.77	0.65	0.73	1.00	1.37	0.05	0.79
DeepSeek-V4-Flash ( T )	0.57	0.47	0.52	1.43	1.89	-0.48	0.63
GPT-4o	0.53	0.45	0.12	3.37	3.63	3.37	0.10
GPT-5	0.73	0.61	0.64	1.18	1.58	0.78	0.67

Appendix

Table 25: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.74	0.65	0.66	0.86	1.36	0.70	0.78
DeepSeek-V3.2 ( T )	0.73	0.63	0.42	2.01	2.32	1.98	0.35
DeepSeek-V3.2 ( T )	0.81	0.69	0.77	0.92	1.23	0.05	0.83
DeepSeek-V4-Flash ( T )	0.63	0.53	0.59	1.23	1.65	-0.51	0.69
GPT-4o	0.53	0.46	0.12	3.37	3.63	3.37	0.10
GPT-5	0.77	0.66	0.69	1.02	1.45	0.73	0.75

Appendix

Table 26: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.72	0.62	0.64	0.90	1.44	0.74	0.76
DeepSeek-V3.2 ( T )	0.73	0.63	0.42	2.01	2.33	1.98	0.35
DeepSeek-V3.2 ( T )	0.77	0.65	0.72	1.03	1.41	0.08	0.77
DeepSeek-V4-Flash ( T )	0.59	0.49	0.54	1.36	1.83	-0.50	0.66
GPT-4o	0.52	0.45	0.12	3.38	3.64	3.38	0.10
GPT-5	0.77	0.65	0.67	1.09	1.52	0.79	0.73

Appendix

Table 27: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , against a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.49	0.37	0.46	1.16	1.55	0.48	0.71
DeepSeek-V4-Flash ( T )	0.50	0.41	0.47	1.50	1.90	-0.36	0.60
GPT-4o	0.43	0.36	0.12	3.03	3.32	2.98	0.14
GPT-5	0.50	0.40	0.46	1.36	1.72	0.62	0.63
GPT-5-Mini	0.51	0.40	0.44	1.52	1.90	0.93	0.56
Kimi-K2.5	0.41	0.33	0.36	1.64	2.05	0.91	0.52

Appendix

Table 28: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.50	0.41	0.50	1.18	1.55	0.09	0.70
DeepSeek-V4-Flash ( T )	0.48	0.38	0.46	1.47	1.86	-0.35	0.61
GPT-4o	0.43	0.38	0.12	3.04	3.33	2.99	0.14
GPT-5	0.49	0.41	0.46	1.30	1.68	0.53	0.66
GPT-5-Mini	0.53	0.43	0.45	1.45	1.85	0.99	0.59
Kimi-K2.5	0.52	0.41	0.44	1.45	1.78	0.91	0.58

Appendix

Table 29: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , without access to a standard markscheme and golden solution.

Model	Pearson $r$	Kendall $\tau$	QWK	MAE	RMSE	Bias	WTA ≤1
Claude-Sonnet-4.6 ( T )	0.47	0.37	0.47	1.25	1.63	0.07	0.67
DeepSeek-V4-Flash ( T )	0.51	0.41	0.47	1.50	1.91	-0.34	0.58
GPT-4o	0.42	0.36	0.12	3.06	3.35	3.01	0.14
GPT-5	0.49	0.40	0.46	1.35	1.72	0.57	0.64
GPT-5-Mini	0.53	0.41	0.45	1.51	1.89	0.96	0.55
Kimi-K2.5	0.49	0.39	0.44	1.54	1.89	0.80	0.55

Appendix

Table 30: Performance of language models across multiple correlation and error metrics. Thinking-enabled and non-thinking model variants are denoted by T and T , respectively. Results are evaluated on the synthetically-generated dataset, Trojan-Bench(S) , without access to a standard markscheme and golden solution.

	QWK ( $\uparrow$ )				RMSE ( $\downarrow$ )				Bias ( $\approx 0$ )
	DS V4F	Kimi K2.5	Gem. 3P	Q3.5 27B	DS- V4F	Kimi K2.5	Gem. 3P	Q3.5 27B	DS- V4F	Kimi K2.5	Gem. 3P	Q3.5 27B
Chain-of-Thought (CoT@1)
MathArena [ 4 ]	0.52	0.35	-	0.40	1.89	2.59	-	2.60	-0.48	2.20	-	2.10
Chain-of-Thought with Majority Vote Selection (MajorityVote@16)
MathArena [ 4 ]	0.54	0.36	-	0.41	1.83	2.56	-	2.55	-0.50	2.25	-	2.20
Chain-of-Thought with Best-of-N Selection (BoN@16)

Appendix

Table 31: Comparative analysis of model inference performance on synthetically generated data across QWK, RMSE, and Bias metrics for DeepSeek-V4-Flash, Kimi-K2.5, Gemini-3-Pro-Preview, and Qwen3.5-27B. Evaluation is performed with a reference solution and a corresponding marking scheme.

Figure 6: Trojan-Bench(H) (Full): Correlation metrics (Pearson $r$ , QWK, Kendall $\tau$ ) by model and sampling method.

Figure 7: Trojan-Bench(H) (Full): Error metrics (MAE, RMSE, Bias) by model and sampling method.

Figure 8: Trojan-Bench(H) (Full): Agreement metrics (Exact Match, WTA $\leq 1$ ) by model and sampling method.

Figure 9: Trojan-Bench(H) (Blind): Correlation metrics (Pearson $r$ , QWK, Kendall $\tau$ ) by model and sampling method.

Figure 10: Trojan-Bench(H) (Blind): Error metrics (MAE, RMSE, Bias) by model and sampling method.

Figure 11: Trojan-Bench(H) (Blind): Agreement metrics (Exact Match, WTA $\leq 1$ ) by model and sampling method.

Figure 12: Trojan-Bench(S) (Full): Correlation metrics (Pearson $r$ , QWK, Kendall $\tau$ ) by model and sampling method.

Figure 13: Trojan-Bench(S) (Full): Error metrics (MAE, RMSE, Bias) by model and sampling method.

Figure 14: Trojan-Bench(S) (Full): Agreement metrics (Exact Match, WTA $\leq 1$ ) by model and sampling method.

Figure 15: Trojan-Bench(S) (Blind): Correlation metrics (Pearson $r$ , QWK, Kendall $\tau$ ) by model and sampling method.

Figure 16: Trojan-Bench(S) (Blind): Error metrics (MAE, RMSE, Bias) by model and sampling method.

Figure 17: Trojan-Bench(S) (Blind): Agreement metrics (Exact Match, WTA $\leq 1$ ) by model and sampling method.

Figure 18: Trojan-Bench(H) : Pearson $r$ blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 19: Trojan-Bench(H) : QWK blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 20: Trojan-Bench(H) : Kendall $\tau$ blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 21: Trojan-Bench(H) : MAE blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 22: Trojan-Bench(H) : RMSE blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 23: Trojan-Bench(H) : Bias blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 24: Trojan-Bench(H) : Exact Match blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 25: Trojan-Bench(H) : WTA ( $\leq 1$ ) blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full).

Figure 26: Trojan-Bench(S) : Pearson $r$ blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 27: Trojan-Bench(S) : QWK blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 28: Trojan-Bench(S) : Kendall $\tau$ blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 29: Trojan-Bench(S) : MAE blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 30: Trojan-Bench(S) : RMSE blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 31: Trojan-Bench(S) : Bias blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 32: Trojan-Bench(S) : Exact Match blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 33: Trojan-Bench(S) : WTA ( $\leq 1$ ) blind and full inference heatmap across evaluated models (Majority Vote; top: Blind, bottom: Full). Note that "human" in this heatmap indicates an LLM assigned grade during data generation with TROJAN and serves as a reference point when evaluating the LLMs.

Figure 34: Annotation website used by two domain experts to grade USAMO 2025 candidate solutions. The interface presents the problem statement, marking scheme, golden solution, and candidate solution side by side, and stores per-problem scores together with free-form justifications as JSON.

Setting	Value
Model
Base model	Qwen3.5-9B
Tuning regime	Full fine-tuning
Precision	bfloat16
Data
Training corpus	Synthetic data from four competitions

Appendix

Table 32: Supervised fine-tuning configuration for Qwen3.5-9B.

Setting	Value
Model
Base model	Qwen3.5-27B
Tuning regime	LoRA
LoRA rank ( $r$ )	8
Precision	bfloat16
Data

Appendix

Table 33: Supervised fine-tuning configuration for Qwen3.5-27B.

UCB exploration $c$	QWK	RMSE	Bias
$c=0.10$	0.641	2.38	-1.17
$c=0.25$	0.657	2.06	-1.04
$c=0.50$	0.634	2.59	-1.34
$c=0.75$	0.613	2.69	-1.40
$c=1.00$	0.616	2.46	-1.47

Appendix

Table 34: Parameter

c

ablation with DeepSeek-V4-Flash-Thinking base model.

	Full Setting			Blind Setting
	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )
Qwen3.5-9B (Base)	0.02	4.00	3.23	0.06	2.52	0.63
Qwen3.5-9B (SFT)	0.23	2.19	0.17	0.08	2.32	-0.52

Appendix

Table 35: SFT results with excluded USAMO 2025 datapoints

	Full Setting			Blind Setting
	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )
Qwen3.5-9B (Base)	0.02	4.00	3.23	0.06	2.52	0.63
Qwen3.5-9B (SFT-Opus-4.6)	0.35	2.08	0.27	0.07	2.40	0.39
Qwen3.5-9B (SFT-DSV4F)	0.23	2.18	0.27	0.17	2.29	-0.23
Qwen3.5-27B (Base)	0.36	2.98	1.54	-0.11	4.12	-3.40
Qwen3.5-27B (SFT-Opus-4.6)	0.47	2.10	0.77	0.06	2.50	0.21

Appendix

Table 36: Comparative performance of base and fine-tuned models on TROJAN synthetic samples coming from DeepSeek-V4-Flash (DSV4F) model and larger Claude Opus 4.6 (Opus-4.6). Best results are bolded .

	Full Setting			Blind Setting
	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )
Qwen3.5-9B (Base)	0.70	2.29	1.11	0.47	3.16	1.98
Qwen3.5-9B (SFT)	0.79	1.50	0.15	0.53	2.32	0.93
Qwen3.5-27B (Base)	0.80	1.81	0.41	0.49	3.08	1.04
Qwen3.5-27B (SFT)	0.81	1.44	-0.12	0.48	2.36	0.28

Appendix

Table 37: Comparative performance of base and fine-tuned models on TROJAN synthetic samples on ProofBench benchmark. Best results are bolded .

	QWK ( $\uparrow$ )	RMSE ( $\downarrow$ )	Bias ( $\approx 0$ )
Qwen3.5-27B (model only)	0.30	3.04	1.81
Qwen3.5-27B (uniform with $r=1$ )	0.40	2.78	-1.48
Qwen3.5-27B (uniform with $r=5$ )	0.56	2.25	-1.26
Qwen3.5-27B (UCB)	0.57	2.15	-0.98

Appendix

Table 38: Effect of the multi-armed bandit (UCB) algorithm on grading performance. Baselines include a single-model approach and a uniform sampling strategy, where each arm is pulled exactly

r

times before a final decision is made. Best results are highlighted in bold .

Automated Grading

Automated grading uses machine learning and language models to score student work against answer keys or rubrics and provide feedback.

See all 89 papers

Jun 13, 2026

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.

Jierui Zhang, Siyuan Tan, Xinhang Li +8

School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6

Mathematical Reasoning Benchmarks LLM Evaluation Automated Theorem Proving Training Data Curation LLM Mathematical Reasoning

Ask PDF

Jun 9, 2026

Evaluating Research-Level Math Proofs via Strict Step-Level Verification

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.

Yifeng Sun

Independent Researcher

LLM Answer Verification Automated Theorem Proving LLM Mathematical Reasoning Reasoning Verification

Ask PDF

May 11, 2026

Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient: mathematical proofs should also be clear, concise, insightful, and transferable to other problems. While this proof quality is subjective and depends on the reader and context, many of its components are concrete and broadly valued. In this work, we identify such components and introduce ProofRank, a benchmark curated from challenging mathematical competitions. ProofRank evaluates several scalable proxies of proof quality: (i) conciseness, measuring whether proofs avoid unnecessary steps; (ii) computational ease, measuring the extent to which a proof relies on tedious calculations; (iii) cognitive simplicity, measuring how accessible the used proof techniques are; (iv) diversity, measuring how varied a model's proofs for a single problem are; and (v) adaptivity, measuring whether a model can follow a specified proof technique. Across models, we find substantial differences in proof quality that are not captured by correctness-only benchmarks. We also observe significant trade-offs between proof-quality metrics and correctness, suggesting that future evaluations of mathematical reasoning should measure how useful LLM-generated proofs are.

Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov +1

1INSAIT, Sofia University "St. Kliment Ohridski" · 2ETH Zurich

Mathematical Reasoning Benchmarks LLM Evaluation LLM Mathematical Reasoning

Ask PDF

Abstract

Automated Grading

Explore similar work

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

Evaluating Research-Level Math Proofs via Strict Step-Level Verification

Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness