Elamur Research⌕
☰
home / papers / 2024 / Proving Olympiad Algebraic Inequalities without Human Demonstrations

Proving Olympiad Algebraic Inequalities without Human Demonstrations

Paper · 2024 · Chenrui Wei, Mengzhou Sun and Wei Wang

Summary

Learning-based provers have made progress on Olympiad geometry, but algebraic inequalities remain difficult. Competition-grade training data is scarce, and the space of possible transformations is effectively unbounded. The authors present AIPS (Algebraic Inequality Proving System), which works without any human-written proofs. Its core is a symbolic deductive engine built on SymPy. The engine represents expressions as trees, tracks how each node affects the overall value, and pattern-matches classical inequalities to derive new bounds. The same engine also synthesizes fresh ternary and quaternary inequality theorems. Proof search is best-first and guided by a value network that ranks candidate subgoals. This network is fine-tuned on generated problems presented in order of rising difficulty, a scheme the authors call value curriculum learning. On a 20-problem Olympiad benchmark, AIPS proves 10, outperforming LLMs, a Lean-based prover and other search variants. The work matters because it shows that self-generated data combined with symbolic reasoning can reach competition level in a domain without curated datasets.

Key points

  • The engine's theorem library includes AM-GM (plain and weighted), Cauchy, Jensen, discrete Hölder, Schur and binary/ternary Muirhead. Matching for expensive theorems is time-limited.
  • On MO-INT-20, each problem had 90 minutes on one CPU core. AIPS solved 10 of 20, including 5 of the 10 IMO/IMO-shortlist items, which is roughly average IMO-contestant level.
  • Baseline results on the same benchmark:
    • Gemini 1.5 Pro: 1
    • GPT-4, GPT-4 Turbo, Llemma-7b and LeanCopilot (LeanDojo): 0 each
    • Deductive engine with BFS: 4
    • Deductive engine with MCTS: 5
    • Deductive engine guided by GPT-4 Turbo heuristics: 6
    • Tree-depth heuristic or a pretrained value net only: 7 each
  • The curriculum used 1,000 inequality problems. As fine-tuning progressed, the number of search steps dropped and the number of solved problems rose.
  • Three national-olympiad medalists judged several synthesized theorems comparable to IMO problems from around 2000. One was chosen for a major city's 2024 Mathematical Olympiad.

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 worksMathematics · 233 worksComputational Theory and Mathematics · 496 worksApplied Mathematics · 73 worksModeling and Simulation · 12 works

Cite

Cite as Chenrui Wei, Mengzhou Sun and Wei Wang. 2024. Proving Olympiad Algebraic Inequalities without Human Demonstrations. arXiv:2406.14219.

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

@misc{wei2024proving,
  title = {{Proving Olympiad Algebraic Inequalities without Human Demonstrations}},
  author = {Chenrui Wei, Mengzhou Sun and Wei Wang},
  year = {2024},
  doi = {10.48550/arxiv.2406.14219},
  eprint = {2406.14219},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2406.14219}
}

References

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

  1. Judea Pearl. Graphical models for probabilistic and causal reasoning. Quantified representation of uncertainty and imprecision, pages 367–389, 1998. find
  2. W-T Wu. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 21:157–179, 1978. find
  3. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3): 219–246, 2000. find
  4. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024.
  5. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems, 2021. URL https://arxiv.org/abs/2110.14168, 2021. ↗
  6. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
  7. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  8. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.
  9. Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arXiv:2007.02924, 2020.
  10. Hongming Zhang and Tianyang Yu. Alphazero. Deep Reinforcement Learning: Fundamentals, Research and Applications, pages 391–415, 2020. find
  11. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349, 2022.
  12. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  13. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
  14. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534, 2024.
  15. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Handbook of the History of Logic, volume 9, pages 135–214. Elsevier, 2014.
  16. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. find
  17. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The coq proof assistant reference manual. INRIA, version, 6(11), 1999. find
  18. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. find
  19. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C Paulson. Isarstep: a benchmark for high-level mathematical reasoning. arXiv preprint arXiv:2006.09265, 2020.
  20. Floris van Doorn, Gabriel Ebner, and Robert Y Lewis. Maintaining a library of formal mathematics. In International Conference on Intelligent Computer Mathematics, pages 251–267. Springer, 2020. find
  21. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pages 6984–6994. PMLR, 2019.
  22. Georges Gonthier et al. Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008. find
  23. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 31(2):349–354, 2022. find
  24. Kevin Buzzard and Richard Taylor. A lean proof of fermat’s last theorem. 2024. find
  25. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484–489, 2016. find
  26. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. nature, 550(7676):354–359, 2017. find
  27. Rina Dechter and Judea Pearl. Generalized best-first search strategies and the optimality of a. Journal of the ACM (JACM), 32(3):505–536, 1985. find
  28. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017.
  29. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023.
  30. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023.
  31. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. Advances in Neural Information Processing Systems, 35:3843–3857, 2022.
  32. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824–24837, 2022.
  33. Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Learning hierarchical representations of math concepts in theorem proving. arXiv preprint arXiv:2401.02949, 2024.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wei-2024-proving-olympiad-algebraic-inequalities-without/