PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.36767v1cs.AI

TL;DR

Olympiad proof verification is underexplored and difficult to scale because long arguments require assessing each claim and partial credit. The paper builds curated and synthetic proof-grading data and introduces MABGrader; it reports improved agreement and lower error than ProofGrader.

  • Problem

    Olympiad proofs require meticulous assessment of long reasoning chains, while expert verification is costly to scale and existing error distributions offer limited control.

    Source: §1 · pp. 1–2

  • Method

    The paper introduces an expert-graded USAMO 2025 benchmark, TROJAN for self-critique-based adversarial proof generation, and MABGrader for bandit selection among candidate grades.

    Source: §1 · pp. 2–3

  • Results

    26.4% higher QWK and 14% less error than ProofGrader are reported for MABGrader, which achieves the best overall performance.

    Source: §8 · p. 10

  • Takeaways & Limitations

    The study concludes that current LLM verifiers remain short of expert-level agreement and identifies paths toward more reliable automated verification.

    Source: §8 · p. 10

    The evaluation depends on both a marking scheme and golden reference solution, limiting its applicability to settings such as peer review of new theorems or open-ended scientific verification.

    Source: §7 · p. 10

Abstract

from arXiv · show

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.

1 Introduction

The introduction argues that Olympiad proof verification is difficult to scale and that answer correctness alone misses errors in long reasoning chains. It presents controlled error-injected data, TROJAN, and MABGrader as approaches to studying and improving LLM grading.

1 Introduction

  • Correct final answers can still conceal logical gaps or unjustified claims, while many proof problems have no final answer and require costly expert verification.Source: §1 · p. 1
  • Long Olympiad proofs require identifying how a single error affects later reasoning and partial credit, beyond judging surface plausibility.Existing datasets often rely on costly human grading of LLM-generated solutions, with limited control over error type and severity.Source: §1 · p. 2
  • MABGrader frames verification as selecting among candidate grades with error analyses, allocating computation to uncertain cases without modifying the base model.Source: §1 · pp. 2–3
  • Trojan-Bench(H) uses rubric-aligned adversarial errors in USAMO 2025 solutions to test flaw detection and partial-credit grading.Source: §1 · p. 2
  • TROJAN generates adversarial samples through self-critique, and training on its synthetic data improves alignment with expert grading.Source: §1 · p. 2
  • The study evaluates 20 models across prompts, inference methods, and metrics on Olympiad-level mathematical verification.Source: §1 · p. 2

2 Related Works

Related work spans mathematical reasoning benchmarks, LLM-based judging, formal proof verification, and standards for fair grading. The paper positions natural-language proof assessment as a distinct setting where expert grading remains common.

2 Related Works

  • Mathematical benchmarks range from foundational datasets to Olympiad-focused evaluations and systems competing in the IMO.The cited work describes recent systems as approaching top human competitors.Source: §2 · p. 3
  • LLM judges can correlate highly with human experts on standard tasks, but theorem grading still often relies on experts, limiting scalability.Source: §2 · p. 3
  • Formal proof assistants verify proofs through language kernels, offering an objective alternative to natural-language assessment.Source: §2 · p. 3
  • Fair-grading guidance treats human agreement and acceptable automated-scoring thresholds as domain-dependent rather than universal.The paper uses the cited guidance as a conservative lower bound for evaluating models.Source: §2 · p. 3

3 Problem Formulation

The task is to detect reasoning errors in a natural-language mathematical solution and assign a fair grade. The verifier may receive a reference solution and marking scheme, or work without either.

3 Problem Formulation

  • Verification takes a problem, candidate solution, and optionally a reference solution and marking scheme, then assigns a grade reflecting correctness and completeness.Source: §3 · p. 3
  • Grades range from 0 to 7, following common practice in the cited grading work.Source: §3 · p. 3
  • The Full setting provides the reference solution and marking scheme, whereas the Blind setting provides only the problem and candidate solution.Source: §3 · p. 3

4 Dataset Construction

The section constructs a human-curated USAMO benchmark through rubric-aligned error injection and scales adversarial proof generation with TROJAN. Human and audit results support the reliability of the curated and synthetic data.

4.1 Human curated dataset

  • Trojan-Bench(H) is built backward from golden solutions by mapping proof components to rubric criteria and injecting errors for targeted deductions across six USAMO 2025 problems.Grades follow the marking schemes on a 0–7 scale.Source: §4.1 · p. 4
  • Faulty solutions target sampled grades, with heavier penalties for errors in fundamental proof steps that can cascade across rubric criteria.Source: §4.1 · p. 4
  • Two independent annotators produced 48 human-verified candidate solutions, each with a grade and justification; non-expert validation was omitted because of the proofs’ specialized nature.Source: §4.1 · p. 4
  • The human-curated Trojan-Bench(H) achieves QWK 0.76 and Pearson correlation 0.89 between annotators, with 85% of scores within one point.The reported two-point agreement is 94%, and systematic bias is ±0.08.Source: §4.1 · pp. 4–5, Table 1 · p. 4

4.2 Synthetic dataset generation

  • TROJAN takes a problem, reference solution, marking scheme, and target score profile, then injects calibrated errors and iterates self-critique and refinement to produce a proof and grade justification.The loop ends after consecutive alignment judgments or a bounded number of rounds.Source: §4.2 · p. 5, Figure 3 · p. 5
  • Trojan-Bench(S) draws on four competitions, and its grades and justifications are treated as ground truth when evaluating the synthetic data.The reported experiments find close correlation with Trojan-Bench(H).Source: §4.2 · p. 5
  • In the synthetic-data audit, ∼83% of problems fell within one grading point of expert-assigned grades, and expert annotators agreed within one point on all graded problems.Source: Table 2 · p. 5, §4.2 · p. 6, Table 3 · p. 6

5 Our Approach

MABGrader treats grade selection as a bandit problem, using defended grade proposals and a judging oracle to guide selection. It adopts UCB to balance exploration and exploitation across the discrete grade range.

5 Our Approach

  • The method frames grade assignment as a multi-armed bandit problem over candidate grades 0–7.Even with a reference solution and marking scheme, assigning a grade outright is difficult.Source: §5 · p. 6
  • MABGrader adopts UCB instead of pairwise A/B voting because comparisons are token-intensive and spend pulls exploring clearly sub-optimal grades.UCB first plays each arm once, then selects among arms in subsequent rounds.Source: §5 · p. 6
  • For each candidate grade, an LLM provides a justification and self-reported confidence; the same model then acts as a judging oracle, selecting arms and assigning rewards.MABGrader aggregates rewards and updates arm statistics to balance exploration and exploitation toward the underlying true grade.Source: §5 · p. 6
  • The parameter c is user-controlled and can be adapted to different problems; the design is compatible with single-arm sampling bandits, while comparison with alternatives is left for future work.The oracle’s 1–5 fairness Likert rating is rescaled to [0, 1] via r = (˜r − 1)/4.Source: §5 · p. 6

6 Experiments

The experiments evaluate LLM grading against human judgments across settings, sampling methods, and synthetic data. MABGrader achieves the highest QWK across tested models, while results also show that human-curated cases are harder and synthetic-data fine-tuning improves agreement.

6.1 Experimental Setup

  • The evaluation uses seven alignment metrics, fixed sampling settings, and both Full and Blind scenarios, with 16 independent attempts for multi-sample experiments.The setup fixes topp = 0.95 and temperature t = 0.1; the default testing environment follows the MathArena template.Source: §6.1 · p. 7

6.2 Analysis of Trojan-Bench(S)

  • In the Full setting, MajorityVote@16 raises average correlation by 0.06 absolute and 24.2% relative, yet models remain below 0.70 versus expert agreement of 0.76; Blind performance reaches at most 0.53.Figure 4 reports QWK across Full and Blind settings for CoT@1, MeanCoT@16, and MajorityVote@16.Source: §6.2 · p. 7, Figure 4 · p. 8
  • Under Full inference, MajorityVote scores 5.46% higher than CoT and 2.36% higher than MeanCoT, with its primary benefit described as stabilizing grading output.The relatively low sampling temperature makes the gap between single- and multi-sampling small.Source: §6.2 · p. 8
  • On human-curated data, models show 0.07 lower absolute QWK, 0.12 higher RMSE, and 0.04 higher Bias than on synthetic data; the human-crafted set is harder, and expert-label versus synthetic-set response correlation is Pearson r = 0.89.Figure 5 reports MajorityVote@16 across QWK, RMSE, and Bias for human and synthetic USAMO 2025 subsets of N = 48.Source: §6.2 · pp. 8–9, Figure 5 · p. 8
  • Fine-tuning on synthetic data improves smaller models across the three primary metrics and raises correlation with human grading at both small and large model scales.The fine-tuning experiment uses Qwen3.5-9B and 27B models trained on synthetic data.Source: §6.2 · p. 9
  • The selected TROJAN settings, niter = 5 and nalig. = 2, achieve QWK = 0.884 and RMSE = 0.707, the best correlation and lowest error across the ablated configurations.Some alternatives yield zero bias but have substantially lower correlation and higher error.Source: §6.2 · p. 9, Table 5 · p. 9

6.3 Performance of MABGrader

  • MABGrader achieves the highest QWK across all four tested models, while RMSE and Bias improve for three models but reward models are slightly better on DeepSeek-V4-Flash for those error measures.The comparison uses the manually annotated USAMO 2025 dataset in the Full setting.Source: §6.3 · pp. 9–10, Table 6 · p. 10

7 Limitations and Future Work

The evaluation requires both a markscheme and a golden reference solution, limiting its applicability to settings where both are available. MABGrader shares this dependency and does not apply in the Blind setting.

7 Limitations and Future Work

  • The evaluation pipeline requires both a markscheme and a golden reference solution, unlike many real-world verification settings such as peer review of new theorems.Creating a high-quality markscheme without a reference solution remains an open problem the work does not address.Source: §7 · p. 10
  • MABGrader requires a markscheme aligned with a golden solution and therefore does not apply to the Blind setting.The authors identify reference-free grading, potentially using a synthesized proof outline, as future work.Source: §7 · p. 10

8 Conclusion

The study finds that current LLM verifiers fall short of expert-level agreement on Olympiad mathematics. MABGrader achieves the best overall performance, while TROJAN supports scalable adversarial proof generation.

8 Conclusion

  • MABGrader achieves the best overall performance, outperforming ProofGrader by 26.4% in QWK and reducing grading error by 14%.Current LLM verifiers still fall short of expert-level agreement.Source: §8 · p. 10
  • The study evaluates 20 frontier models on a human-curated USAMO benchmark with markscheme-aligned injected errors and expert grades.The evaluation spans prompting and inference settings.Source: §8 · p. 10
  • TROJAN provides scalable adversarial proof generation to support evaluation and supervised fine-tuning and improve grading alignment.Source: §8 · p. 10

A Datasheets

The datasheets provide additional information about the expert-annotated and synthetically generated datasets. Their accompanying information is released, with the data described as primarily intended for benchmarking.

A Datasheets

  • Tables 7 and 8 provide additional information about the expert-annotated and TROJAN-generated synthetic datasets, respectively.Source: A Datasheets · p. 18, Table 7 · p. 18, Table 8 · p. 21
  • The dataset documentation says the data is primarily for benchmarking and discourages training use, while another response says it may be used for training.Source: A Datasheets · pp. 19, 22
  • The datasheets report that others may use the released accompanying information and identify the first author as the dataset maintainer.Source: A Datasheets · p. 20
  • The dataset is released under the MIT license, and the authors plan periodic updates if mistakes are found.Source: A Datasheets · pp. 20, 23

B Distribution of injected errors in Trojan-Bench(H)

The appendix details the injected-error distribution, evaluated-model coverage, and extended evaluation protocol, then reports substantial differences in grader performance across models and settings.

B Distribution of injected errors in Trojan-Bench(H)

C Evaluated Model List

  • The 20-model evaluation covers 52 model-by-dataset-and-style configurations, with uneven provider coverage and broader evaluation of frontier thinking-enabled models.Prometheus-family models were evaluated on Trojan-Bench(H) Full only because they produced no usable rubric-free scores.Source: C Evaluated Model List · p. 24, Table 10 · p. 25

D Extended evaluation results

D.1 Trojan-Bench(H)

  • Thinking-enabled frontier models are the strongest Trojan-Bench(H) graders, while smaller graders and GPT-4o reach near-zero or negative correlation and MAE near or above 3.0.Under Full, DeepSeek-V4-Flash (Think) leads on most aggregate metrics, with mean Pearson r 0.66, mean QWK 0.63, and mean MAE 1.38 across attempts.Source: §D.1 · p. 27
  • Mean-CoT@16 and MajorityVote@16 yield small, consistent gains over single CoT, while Blind grading shifts correlations downward and can reverse bias.For DeepSeek-V3.2 (Think), bias moves from +0.27 Full to −0.88 Blind.Source: §D.1 · p. 27
  • Qwen3-8B, GPT-5 Mini, and Kimi-K2.5 achieve better QWK and lower MAE under Blind than Full, with the Full rubric anchoring small graders toward higher scores.Source: §D.1 · p. 27

D.2 Trojan-Bench(S)

On Trojan-Bench(S), Full-setting graders achieve stronger aggregate correlations than on the human benchmark, while common failure patterns and grader rankings largely carry across datasets. MABGrader’s gains over sampling baselines also persist on the synthetic benchmark, and the accompanying plots expose metric patterns across graders and sampling methods.

D.2 Trojan-Bench(S)

  • 0.81 Pearson r and 0.75 QWK are achieved by Claude-Sonnet-4.6 (Think) on Trojan-Bench(S) Full; DeepSeek-V3.2 (Think) reaches 0.81 Pearson r and 0.77 QWK with MeanCoT@16.GPT-5 reaches 0.77 Pearson r and 0.69 QWK; Mean-CoT and MajorityVote improve aggregate quality by a few points over a single CoT call.Source: §D.2 · p. 31
  • GPT-4o’s QWK is 0.12 despite Pearson correlation of 0.53 and bias of +3.37, indicating ranking alignment alongside substantial grade inflation.Lower-tier graders show positive bias of about +1.6 to +2.2; under Blind, most graders’ bias shifts to small positive or near-zero values with MajorityVote@16.Source: §D.2 · p. 31
  • Grader ordering is largely preserved across Trojan-Bench(H) and Trojan-Bench(S), with the same top three and bottom three on Full, while synthetic-set metric values shift upward in correlation and downward in error.The authors attribute the higher synthetic-set values to lower per-rubric-item ambiguity by construction.Source: §D.2 · p. 31

D.3 Additional evaluation of BoN methods

  • MABGrader leads on QWK and RMSE for the three graders evaluated on Trojan-Bench(S) Full, while MajorityVote and BoN baselines yield essentially flat gains over CoT@1.The reported comparison attributes consistent gains across graders to MABGrader’s prompt-side hypothesis enumeration.Source: §D.3 · p. 36, Table 31 · p. 36

E Extended Bar plots

  • The bar plots organize each dataset-and-style pair by metric family, with CoT@1, Mean-CoT@16, and MajorityVote@16 bars for each model.Across the plots, frontier thinking-enabled models cluster higher in correlation and lower in error; close-but-not-exact agreement is achievable for most frontier models, while exact agreement remains low.Source: E Extended Bar plots · p. 37, Figure 6 · p. 37, Figure 7 · p. 38

F Evaluation of LLM correlation with human and other LLM annotators

The heatmaps show that removing the markscheme weakens ordinal agreement and grader-to-grader consensus, while absolute error changes less and average bias on the human benchmark reverses direction. The human benchmark’s reference grades came from independent expert grading followed by joint reconciliation.

F Evaluation of LLM correlation with human and other LLM annotators

  • On Trojan-Bench(H), removing the markscheme lowers mean human-vs-LLM Pearson r from 0.50 to 0.39, Kendall τ from 0.42 to 0.30, and QWK from 0.41 to 0.33, while MAE stays essentially unchanged at 1.99 versus 2.00.On Trojan-Bench(S), Pearson r falls from 0.67 to 0.46 and Kendall τ by 0.20, while MAE improves from 1.83 to 1.74 under Blind.Source: F Evaluation of LLM correlation with… · p. 48
  • On Trojan-Bench(H), average bias shifts from −1.48 under Full to +0.51 under Blind, with 10 of 14 judges changing sign; on Trojan-Bench(S), only 1 of 8 changes sign.The authors interpret this contrast as a markscheme-versus-human-style effect rather than an artifact of model calibration.Source: F Evaluation of LLM correlation with… · p. 48
  • On Trojan-Bench(H), mean inter-LLM Pearson r falls from 0.64 to 0.44 under Blind, and pairwise standard deviation rises from 0.15 to 0.28; the synthetic set’s mean falls from 0.63 to 0.54.Under Full, frontier reasoning graders form a high-agreement block, with pairwise Pearson typically above 0.7 and pairwise QWK above 0.6.Source: F Evaluation of LLM correlation with… · p. 48

G Annotation procedure

  • Two annotators graded all 48 problems independently, then jointly inspected disagreements and committed one consensus grade per problem.The custom tool presented the problem, marking scheme, golden solution, and candidate solution, and stored scores and justifications as JSON.Source: G Annotation procedure · p. 65, Figure 34 · p. 65

H Additional details on SFT training

The appendix documents the supervised fine-tuning configurations for the two synthetic-data-trained Qwen variants, including their distinct tuning methods and shared training setup.

H Additional details on SFT training

I Hyperparameter c ablation in MABGrader

For MABGrader with DeepSeek-V4-Flash-Thinking, the selected exploration coefficient balances over- and under-exploration. Case analyses of smaller graders show that rubric-conditioned scoring can over-credit flawed proofs, consistent with their weaker compositional reasoning.

I Hyperparameter c ablation in MABGrader

  • c = 0.25 gives the best QWK (0.657), lowest RMSE (2.06), and near-best bias (−1.04); larger c values over-explore weak arms, while c = 0.10 under-explores.The authors use c = 0.25 with 16 iterations for the main-text MABGrader results.Source: I Hyperparameter c ablation in MABGrader · p. 67

J.1 Behavior of smaller models on Full and Blind settings

  • The six reported examples were selected as the largest Blind-versus-Full instance gaps within each of the three smaller models.Each case reports mean grades, per-instance MAE, an aggregate gap, and representative grader text.Source: §J.1 · p. 68
  • A small grader’s Full-template mean grade is 6.94 on one flawed proof, versus 2.23 under Blind, a 4.71-point inflation gap.The Full grader grants rubric credit based on proof-structure phrases even as its free-form response rejects the induction argument.Source: §J.1 · p. 69
  • Small graders can award credit for later rubric steps even when those steps depend on a definition they identify as wrong, while Blind grading can withhold that credit.The cases describe this as difficulty with compositional reasoning across proof steps.Source: §J.1 · pp. 69, 71
  • On one Kimi-K2.5 case, the Full template gives a mean grade of 7.00 against human grade 0, an inflation gap of 6.31 points, while Blind gives 0.69.The Full grader awards every rubric item despite the Blind grader identifying major flaws in the construction and argument.Source: §J.1 · p. 70
  • The rubric can act as a high-precision surface-form matcher: proofs using the expected theorem names and outline may receive inflated scores despite substantive errors.The authors contrast smaller graders’ pattern matching with larger models’ ability to combine local rubric judgments with global proof assessment.Source: §J.1 · pp. 71–72

J.2 Effect of MABGrader on grading procedures

On the 48-point comparison and related cases, MABGrader addresses grading errors that persist across consistent CoT samples. The section also reports SFT and generator-model experiments that extend the analysis to held-out USAMO problems and a smaller generator.

J.2 Effect of MABGrader on grading procedures

  • +0.171 QWK lift is MABGrader’s largest improvement over prompt-engineering or aggregation methods; mean signed error moves from CoT’s +1.383 to +0.340.MABGrader improves every reported aggregate metric and is closest to zero bias.Source: §J.2 · p. 72
  • 38 of 48 CoT samples agree, and 16-shot MajorityVote is no better—and slightly worse on EM—than a single attempt, leaving structural bias unresolved.The section identifies over-grading bias, rather than stochastic noise, as the dominant failure on this benchmark.Source: §J.2 · pp. 72, 74
  • On the cascading-error case, MABGrader selects grade 0 with zero instance MAE, while vanilla CoT’s mean grade is 5.25 and its MAE is 6.The vanilla failure applies rubric credit atomistically despite a foundational error; MABGrader identifies its downstream consequences.Source: §J.2 · p. 73
  • On the off-by-one case, MABGrader selects grade 5 with zero instance MAE, while vanilla CoT gives a mean grade of 7 and MAE of 2.CoT treats the algebraic error as a typo; MABGrader’s competing readings receive equal oracle reward, and UCB tie-breaking returns the human grade.Source: §J.2 · p. 73
  • MABGrader generates eight defences, one per candidate grade, then has a separate oracle score each defence; UCB ties favor the lowest grade.The oracle scores defences on a Likert scale mapped to a [0, 1] reward, while the tie-break encodes a strict-grading prior.Source: §J.2 · pp. 73–74

K Inclusion of USAMO 2025 samples in the training set

L Effect of changing the generator model in TROJAN pipeline

  • Using both generator models improves the underlying 9B model; DeepSeek V4 Flash performs better in Blind settings, while Opus is generally better in Full settings.The comparison excludes USAMO 2025 samples to reduce memorization and overfitting effects.Source: L Effect of changing the generator… · p. 74

M Benchmarking TROJAN SFT pipeline against ProofBench

This section benchmarks models fine-tuned on TROJAN synthetic data against ProofBench, reporting their grading performance and comparing UCB-based MABGrader with uniform sampling. It also documents the generation, critique, and refinement prompts, along with checklist disclosures about scope, limitations, reproducibility, grading variability, and datapoint contents.

M Benchmarking TROJAN SFT pipeline against ProofBench

  • TROJAN-fine-tuned models matched or exceeded baseline correlations with expert grades on ProofBench while generally reducing overall error and bias.The evaluation fine-tuned Qwen3.5-9B and Qwen3.5-27B on synthetic data, excluded overlap with ProofBench, and tested both Full and Blind settings; the authors interpret the independent benchmark results as evidence that synthetic errors generalize to real-world mistakes and unseen grading tasks.Source: M Benchmarking TROJAN SFT pipeline… · pp. 74–75, Table 37 · p. 75

N Effect of Multi-Armed Bandit algorithm on grading

  • MABGrader’s UCB policy outperformed uniform sampling, whose justification-and-scoring mechanism improved on direct MajorityVote grading and gained further from larger sampling budgets.Uniform sampling scores justifications for every candidate grade and pulls each arm a fixed number of times, whereas UCB adaptively allocates computation using oracle feedback.Source: Table 38 · p. 75, N Effect of Multi-Armed Bandit… · p. 76

O Prompt templates

  • The appendix provides grading templates and TROJAN’s error-injection, critique, and refinement prompts for reproducibility.The error-injection prompt targets a specified score profile; an independent grader critiques rubric misalignments, and refinement produces a minimally edited revision aligned with that profile.Source: O Prompt templates · p. 77
  • TROJAN’s generation template supplies the problem, markscheme, reference solution, and target score profile, then requests a candidate proof with notes explaining deductions.The requested notes identify each deducted criterion, awarded score, specific error, and reason for the deduction.Source: O Prompt templates · p. 83
  • The critique prompt grades each rubric criterion independently against the target and requests specific revision guidance when actual and target scores differ.It calibrates error severity and checks whether the proof reads as a coherent student attempt.Source: O Prompt templates · p. 84
  • The refinement prompt preserves already aligned proof sections and makes minimal, specific edits to bring misaligned criteria to their target scores.It also calls for believable, calibrated errors and a coherent, unified proof.Source: O Prompt templates · pp. 85–86

NeurIPS Paper Checklist

  • The checklist states that abstract and introduction claims are supported by broad model evaluation, limitations are discussed in the appendix, and experimental parameters and SFT model cards are reported for reproducibility.The reproducibility statement specifically mentions verification, grading, dataset construction, and inference parameters.Source: NeurIPS Paper Checklist · pp. 87–88
  • Mean and variance are reported for grading across 16 independent runs, with experiment error bars in the Appendix.Source: NeurIPS Paper Checklist · p. 89
  • The authors state that their work discusses fairness in mathematical verification and that they anticipate no negative societal impacts.Source: NeurIPS Paper Checklist · p. 90
  • Each dataset datapoint includes a marking scheme, candidate solutions, and corresponding justifications.Source: NeurIPS Paper Checklist · p. 92
  • The authors state that they describe LLM use in mathematical grading and provide experiment details including base models, templates, and relevant parameters.Source: NeurIPS Paper Checklist · p. 93

Related papers

Loading 2610.36767v1…