Automated Proof of Polynomial Inequalities via Reinforcement Learning
On the map: Deep reinforcement learning methods → RL theory and sample complexity
Abstract (arXiv)
Polynomial inequality proving is fundamental to many mathematical disciplines and finds wide applications in diverse fields. Current traditional algebraic methods are based on searching for a polynomial positive definite representation over a set of basis. However, these methods are limited by truncation degree. To address this issue, this paper proposes an approach based on reinforcement learning to find a {Krivine-basis} representation for proving polynomial inequalities. Specifically, we formulate the inequality proving problem as a linear programming (LP) problem and encode it as a basis selection problem using reinforcement learning (RL), achieving a non-negative {Krivine basis}. Moreover, a fast multivariate polynomial multiplication method based on Fast Fourier Transform (FFT) is employed to enhance the efficiency of action space search. Furthermore, we have implemented a tool called {APPIRL} (Automated Proof of Polynomial Inequalities via Reinforcement Learning). Experimental evaluation on benchmark problems demonstrates the feasibility and effectiveness of our approach. In addition, {APPIRL} has been successfully applied to solve the maximum stable set problem.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Placed in RL theory and sample complexity, one of 15 directions in Deep reinforcement learning methods. Builds on 6 of its 29 references that are in the map. First posted on arXiv 9 Mar 2025.
Builds on
6 of 29 references.
References · 6
- 2013Playing Atari with Deep Reinforcement Learningcited by 3,274
- 2021Convex optimizationcited by 2,515
- 2018Reinforcement Learning of Theorem Provingcited by 69
- 2018GamePad: A Learning Environment for Theorem Provingcited by 48
- 2019HOList: An Environment for Machine Learning of Higher-Order Theorem Provingcited by 19
- 2019Learning dynamic polynomial proofscited by 8
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2026From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
- 2026Learning Fast Monomial Orders for Gr"obner Basis Computations
- 2025Discovering Hidden Algebraic Structures via Transformers with Rank-Aware Beam GRPO
- 2026CircuitBuilder: From Polynomials to Circuits via Reinforcement Learning
- 2026Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates
- 2026FactorLibrary: From Polynomials to Circuits via Recursive Subgoals
- 2026Reinforcement Learning for Symbolic Equation Solving
- 2026Hierarchical Reinforcement Learning for Sparse-Reward Search in Commutative Algebra