Elamur Research⌕
☰
home / papers / 2025 / Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

Paper · 2025 · Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev et al.

Summary

Benchmarks such as MathArena show reasoning LLMs performing at near-elite levels on answer-based contests like AIME and HMMT. However, these tests only check a final number, not whether the argument is valid. The authors test whether current models can write rigorous natural-language proofs. They used the six problems of USAMO 2025, which were uncontaminated because evaluation began within hours of the contest's release. Eight reasoning models each attempted every problem four times. Four experienced olympiad graders scored the anonymized LaTeX solutions on the standard 7-point scale, with two graders per problem and rubrics built from verified AoPS solutions. Results were poor. Gemini-2.5-Pro averaged about 24%, and every other model stayed under 5%. Every model presented its answers as complete solutions, even when they were wrong. The study also classifies errors and documents training-induced quirks. These findings mean that LLM-generated mathematics still requires careful human verification, and that answer-only benchmarks overstate models' reasoning ability.

Key points

  • Models tested: Gemini-2.5-Pro, R1, Grok 3, Flash-Thinking, Claude 3.7, QwQ, o1-pro, o3-mini.
  • Average totals out of 42 points:
    • Gemini-2.5-Pro: 10.1 (about 24.4%), with 6 of its 24 attempts scoring 6/7 or higher.
    • R1 and Grok 3: 2.0 each.
    • o3-mini: 0.9.
    • o1-pro: 1.2, at a cost of about $203.
  • Across roughly 175 solutions from the models other than Gemini, the only full 7/7 score was a single Grok 3 attempt on Problem 1.
  • Graders labeled the first error in each solution as logic, assumption, creativity, or algebra/arithmetic. Flawed logic was the most common category. Models also often dismissed key steps as "trivial," which was especially frequent for o3-mini.
  • Observed artifacts include:
    • placing answers in boxes when no single answer was appropriate (QwQ reduced "all even k" to 2);
    • generalizing from a single example;
    • Gemini inventing citations to papers that do not exist.
  • An attempt to grade solutions automatically with an LLM judge, given the rubric and reference solution, was unsuccessful.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 3Research subjects and languages the work is about.Language models & pretraining · 4,145 worksReasoning · 1,948 worksEvaluation & benchmarks · 1,394 works

Cite

Cite as Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović and Martin Vechev. 2025. Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad. arXiv:2503.21934.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2503.21934 · arXiv 2503.21934

@misc{petrov2025proof,
  title = {{Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad}},
  author = {Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović and Martin Vechev},
  year = {2025},
  doi = {10.48550/arxiv.2503.21934},
  eprint = {2503.21934},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2503.21934}
}

References

14 references, 9 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Anthropic. Claude 3.7 sonnet system card, March 2025. URL https://assets.anthropic.com/ m/785e231869ea8b3b/original/claude-3-7-sonnet-system-card.pdf . ↗
  2. Mislav Balunovic, Jasper Dekoninck, Nikola Jovanovic, Ivo Petrov, and Martin T. Vechev. Math-construct: Challenging LLM reasoning with constructive proofs. CoRR, abs/2502.10197, 2025. doi: 10.48550/ARXIV.2502.10197. URL https://doi.org/10.48550/arXiv.2502.10197 . — [doi:10.48550/arxiv.2502.10197](https://doi.org/10.48550/arxiv.2502.10197) ↗
  3. Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. Matharena: Evaluating llms on uncontaminated math competitions, February 2025. URL https://matharena.ai/ . ↗
  4. Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. Mathematical capabilities of chatgpt. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neu…
  5. Google DeepMind. Gemini Pro, March 2025. URL https://deepmind.google/technologies/ gemini/pro/ . Accessed: 2025-04-03. ↗
  6. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  7. Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, Ally Bennett, Ananya Kumar, Andre Saraiva, An… — OpenAI o1 System Card
  8. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: A challenge formal dataset for automated theorem proving. CoRR, abs/2309.04295, 2023.
  9. OpenAI. Openai o3-mini system card, January 2025. find
  10. URL https://cdn.openai.com/o3-mini-system-card-feb10.pdf . Qwen. Qwq-32b: Embracing the power of reinforcement learning, March 2025. URL https://qwenlm.github.io/blog/qwq-32b/ . ↗
  11. Machel Reid, Nikolay Savinov, Denis Teplyashin, Dmitry Lepikhin, Timothy P. Lillicrap, Jean-Baptiste Alayrac, Radu Soricut, Angeliki Lazaridou, Orhan Firat, Julian Schrittwieser, Ioannis Antonoglou, Rohan Anil, Sebastian Borgeaud, Andrew M. Dai, Katie Millican, Ethan Dyer, Mia Glaese, Thibault Sotti… — Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context
  12. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024. doi: 10.48550/ARXIV.2402.03300. URL https://doi.org/10.48550/arXiv.2402.03300… ↗
  13. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami-tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. CoRR, abs/2407.11214, 2024. xAI. Grok 3 beta — the age of reasoning agents, Februar…
  14. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR. OpenReview.net, 2022.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/petrov-2025-proof-or-bluff-evaluating-llms/