The DOI matches its DataCite record.
Learning dynamic polynomial proofs
Open accessAbstract
Polynomial inequalities lie at the heart of many mathematical disciplines. In this paper, we consider the fundamental computational task of automatically searching for proofs of polynomial inequalities. We adopt the framework of semi-algebraic proof systems that manipulate polynomial inequalities via elementary inference rules that infer new inequalities from the premises. These proof systems are known to be very powerful, but searching for proofs remains a major difficulty. In this work, we introduce a machine learning based method to search for a dynamic proof within these proof systems. We propose a deep reinforcement learning framework that learns an embedding of the polynomials and guides the choice of inference rules, taking the inherent symmetries of the problem as an inductive bias. We compare our approach with powerful and widely-studied linear programming hierarchies based on static proof systems, and show that our method reduces the size of the linear program by several orders of magnitude while also improving performance. These results hence pave the way towards augmenting powerful and well-studied semi-algebraic proof systems with machine learning guiding strategies for enhancing the expressivity of such proof systems.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Synthetic data has long been recognized and used as an important ingredient in theorem proving.
“Synthetic data has long been recognized and used as an important ingredient in theorem proving63–66.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [65]
The Experimental results section says the prover was trained on randomly generated graphs, supporting the use of synthetic data in this theorem-proving work. The paper does not establish that synthetic data has long been recognized as an important ingredient in theorem proving more generally. (LLM, conf=0.82)
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 25
- Yoshua Bengio, Andrea Lodi, and Antoine Prouvost. Machine learning for combinatorial optimization: a methodological tour d'horizon. arXiv preprint arXiv:1811.06128, 2018. · arXiv
- Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving (ex- tended version). arXiv preprint arXiv:1904.03241, 2019. · arXiv
- Boaz Barak and David Steurer. Sum-of-squares proofs and the quest toward optimal algorithms. In Proceedings of International Congress of Mathematicians (ICM), 2014.
- Eden Chlamtac and Madhur Tulsiani. Convex relaxations and integrality gaps. In Handbook on semidefinite, conic and polynomial optimization, pages 139-169. Springer, 2012.
- Dima Grigoriev, Edward A Hirsch, and Dmitrii V Pasechnik. Complexity of semi- algebraic proofs. In Annual Symposium on Theoretical Aspects of Computer Science, pages 419-430. Springer, 2002.
- Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608, 2018. · arXiv
- Jean-Louis Krivine. Quelques propriétés des préordres dans les anneaux commutatifs unitaires. Comptes Rendus Hebdomadaires des Seances de l'Academie des Sciences, 258(13):3417, 1964.
- Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, pages 8822-8833, 2018.
- Jean B Lasserre. Global optimization with polynomials and the problem of moments. SIAM Journal on Optimization, 11(3):796-817, 2001.
- Jean B Lasserre. An introduction to polynomial and semi-algebraic optimization, volume 52. Cambridge University Press, 2015.
- Monique Laurent. A comparison of the Sherali-Adams, Lovász-Schrijver, and Lasserre relaxations for 0-1 programming. Mathematics of Operations Research, 28(3):470-496, 2003.
- Long-Ji Lin. Self-improving reactive agents based on reinforcement learning, planning and teaching. Machine learning, 8(3-4):293-321, 1992.
- László Lovász. On the Shannon capacity of a graph. IEEE Transactions on Information theory, 25(1):1-7, 1979.
- László Lovász and Alexander Schrijver. Cones of matrices and set-functions and 0-1 optimization. SIAM journal on optimization, 1(2):166-190, 1991.
- Monique Laurent and Zhao Sun. Handelman's hierarchy for the maximum stable set problem. Journal of Global Optimization, 60(3):393-423, 2014.
- Anirudha Majumdar, Amir Ali Ahmadi, and Russ Tedrake. Control design along trajectories with sums of squares programming. In 2013 IEEE International Conference on Robotics and Automation, pages 4054-4061. IEEE, 2013.
- Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, and Michaël Périn. Polyhedral approximation of multivariate polynomials using Handelman's theorem. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 166-184. Springer, 2016.
- Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin Riedmiller. Playing atari with deep reinforcement learning. arXiv preprint arXiv:1312.5602, 2013. · arXiv
- Pablo A Parrilo. Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. PhD thesis, California Institute of Technology, 2000.
- Antonis Papachristodoulou and Stephen Prajna. On the construction of Lyapunov functions using the sum of squares decomposition. In Proceedings of the 41st IEEE Conference on Decision and Control, 2002., volume 3, pages 3482-3487. IEEE, 2002.
- Pablo A Parrilo and Ronen Peretz. An inequality for circle packings proved by semidef- inite programming. Discrete & Computational Geometry, 31(3):357-367, 2004.
- Hanif D Sherali and Warren P Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM Journal on Discrete Mathematics, 3(3):411-430, 1990.
- Alexander Schrijver. Combinatorial optimization: polyhedra and efficiency, volume 24. Springer Science & Business Media, 2003.
- Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685, 2018. · arXiv
- Gilbert Stengle. A nullstellensatz and a positivstellensatz in semialgebraic geometry. Mathematische Annalen, 207(2):87-97, 1974.
Cited by
Sorted by citations
Solving olympiad geometry without human demonstrations
Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024) · Nature · doi:10.1038/s41586-023-06747-5 · Cited by 311
Metadata
- Authors
- Fawzi, A., Malinowski, M., Fawzi, H., & Fawzi, O.
- Affiliations
- Google DeepMind (United Kingdom) (GB)
- University of Cambridge (GB)
- École Normale Supérieure de Lyon (FR)
- Venue
- arXiv
- Publisher
- arXiv
- Published
- 2019
- Volume
- 32
- Pages
- 4179-4188
- ISSN
- 2331-8422 (ISSN-L)
- arXiv
- 1906.01681
- OpenAlex
- W2948465511
- Cited by
- 8
- References
- 0
- Citations by year
- 2024: 1 · 2023: 2 · 2022: 1 · 2021: 2 · 2020: 2
- Type
- posted content
- Language
- en
- Open access
- green
- arxiv.org
- Locations
- arXiv (Cornell University) (submittedVersion)
- HAL (submittedVersion, other-oa)
- arXiv (Cornell University)
- neural information processing systems
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Polynomial and algebraic computation
- Physical Sciences › Mathematics › Numerical Analysis › Advanced Optimization Algorithms Research
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Complexity and Algorithms in Graphs
- Keywords
- polynomial inequalities, proof search, deep reinforcement learning, inductive bias, automated theorem proving, proof complexity
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
