REVIEW 18 cited by
Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad
read the original abstract
Recent math benchmarks for large language models (LLMs) such as MathArena indicate that state-of-the-art reasoning models achieve impressive performance on mathematical competitions like AIME, with the leading model, Gemini-2.5-Pro, achieving scores comparable to top human competitors. However, these benchmarks evaluate models solely based on final numerical answers, neglecting rigorous reasoning and proof generation which are essential for real-world mathematical tasks. To address this, we introduce a comprehensive evaluation of full-solution reasoning for challenging mathematical problems. Using expert human annotators, we evaluated several state-of-the-art reasoning models on the six problems from the 2025 USAMO within hours of their release. Our results reveal that all tested models struggled significantly: only Gemini-2.5-Pro achieves a non-trivial score of 25%, while all other models achieve less than 5%. Through detailed analysis of reasoning traces, we identify the most common failure modes and find several unwanted artifacts arising from the optimization strategies employed during model training. Overall, our results suggest that current LLMs are inadequate for rigorous mathematical reasoning tasks, highlighting the need for substantial improvements in reasoning and proof generation capabilities.
Forward citations
Cited by 18 Pith papers
-
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
ProofRank benchmark shows substantial differences in LLM proof quality not captured by correctness, with trade-offs between quality metrics and accuracy.
-
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
LLM proofs for hard math problems show large differences in quality metrics like conciseness and cognitive simplicity that correctness-only tests miss, along with trade-offs between quality and correctness.
-
BAS: A Decision-Theoretic Approach to Evaluating Large Language Model Confidence
BAS aggregates utility from an answer-or-abstain model across risk thresholds and is uniquely maximized by truthful confidence estimates.
-
MathArena: Evaluating LLMs on Uncontaminated Math Competitions
MathArena evaluates over 50 LLMs on 162 fresh competition problems across seven contests, detects contamination in AIME 2024, and reports top models scoring below 40 percent on IMO 2025 proof tasks.
-
You Don't Need to Run Every Eval
The benchmark score matrix of 84 models on 133 tasks is approximately rank-2; BenchPress recovers held-out scores to within 4.6 points and identifies 5-benchmark subsets that predict the full scorecard to within 3.93-...
-
Cost-Effective Automated Judging of Natural-Language Mathematical Proofs
Cheap open-weight judges match frontier models on pass/fail grading of IMO proofs at up to 100x lower cost, with the best voting rule still pending replication.
-
QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs
On QEDBench, frontier LLM judges over-score university math proofs by up to +0.36 on average relative to human experts, while some solver models fail badly on discrete-combinatorial problems.
-
From Proof to Program: Characterizing Tool-Induced Reasoning Hallucinations in Large Language Models
Tool use in LLMs improves final-answer accuracy but degrades reasoning quality through Tool-Induced Myopia, with the effect worsening as tool calls increase and shifting errors toward logic and assumption failures.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
A neurosymbolic method using two LLM prompting frameworks generates provably correct inductive arguments for 84% of a set of mid-size open-source RTL hardware designs.
-
Beyond Reasoning Gains: Mitigating General-Capability Forgetting in Large Reasoning Models
A dynamic replay and reweighting scheduler (RECAP) preserves general capabilities during RLVR while keeping reasoning performance at least as good as reasoning-only finetuning.
-
Seesaw: Accelerating Training by Balancing Learning Rate and Batch Size Scheduling
When a cosine schedule would halve the learning rate, Seesaw cuts it by √2 and doubles the batch, matching loss curves with ~36% fewer serial steps.
-
STAR-P\'olyaMath: Multi-Agent Reasoning under Persistent Meta-Strategic Supervision
STAR-PólyaMath introduces a multi-agent framework with meta-strategic supervision and state-machine orchestration that reports state-of-the-art and perfect scores on eight top math competition benchmarks.
-
Too long; didn't solve
Longer prompts and solutions in a new expert-authored math dataset correlate with higher failure rates across LLMs, with length linked to empirical difficulty after difficulty adjustment.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
LLMs, verified by a symbolic model checker, produced correct inductive strengthenings for 82 of 94 curated RTL safety properties.
-
Too long; didn't solve
Prompt length and solution length both rise with LLM failure on expert-authored adversarial math problems, linking structural length to empirical difficulty.
-
Can LLMs Generate and Solve Linguistic Olympiad Puzzles?
LLMs like o1 outperform humans on most linguistic olympiad puzzle types except writing systems and understudied languages, with insights applied to the new task of puzzle generation.
-
Phi-4-reasoning Technical Report
A 14B reasoning model trained via supervised fine-tuning on selected prompts and o3-mini traces, plus outcome RL, outperforms larger open models like DeepSeek-R1-Distill-Llama-70B on math, coding, planning and related...
-
Sustainability via LLM Right-sizing
Empirical comparison shows smaller open-weight LLMs achieve strong performance on everyday work tasks, supporting task-aware selection over always using the largest models for sustainability and cost reasons.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.