Automated Proof of Polynomial Inequalities via Reinforcement Learning

• URL: http://arxiv.org/abs/2503.06592v1
• Date: Sun, 09 Mar 2025 12:50:28 GMT
• Title: Automated Proof of Polynomial Inequalities via Reinforcement Learning
• Authors: Banglong Liu, Niuniu Qi, Xia Zeng, Lydia Dehbi, Zhengfeng Yang,
• Abstract summary: This paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving inequalities.<n>We also implement a tool called APPIRL (Automated Proof of Polynomial Inequalities via Reinforcement)
• Score: 4.246350085706678
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization [4.2518927441106]
  Main bottleneck in existing methods is a computationally expensive quantifier elimination step.<n>We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula.<n>Our method offers a range of appealing theoretical properties combined with a strong practical performance.
  arXiv  Detail & Related papers  (2024-12-18T14:37:15Z)
• A practical, fast method for solving sum-of-squares problems for very large polynomials [10.645318208507213]
  Sum of squares (SOS) optimization is a powerful technique for solving problems where the positivity of as must be enforced. Our goal is to devise an approach that can handle larger, more complex problems than is currently possible.
  arXiv  Detail & Related papers  (2024-10-21T12:47:42Z)
• Complementary polynomials in quantum signal processing [0.0]
  To implement a given $P$, one must first construct a corresponding complementary $Q$. Existing approaches to this problem employ numerical methods that are not amenable to explicit error analysis. We present a new approach to complementarys using complex analysis.
  arXiv  Detail & Related papers  (2024-06-06T16:47:11Z)
• Optimizing Solution-Samplers for Combinatorial Problems: The Landscape of Policy-Gradient Methods [52.0617030129699]
  We introduce a novel theoretical framework for analyzing the effectiveness of DeepMatching Networks and Reinforcement Learning methods. Our main contribution holds for a broad class of problems including Max-and Min-Cut, Max-$k$-Bipartite-Bi, Maximum-Weight-Bipartite-Bi, and Traveling Salesman Problem. As a byproduct of our analysis we introduce a novel regularization process over vanilla descent and provide theoretical and experimental evidence that it helps address vanishing-gradient issues and escape bad stationary points.
  arXiv  Detail & Related papers  (2023-10-08T23:39:38Z)
• A Direct Reduction from the Polynomial to the Adversary Method [92.54311953850168]
  We give a simple and direct reduction from the method (in the form of a dual) to the adversary method. This shows that any lower bound in the form of a dual is an adversary lower bound of a specific form.
  arXiv  Detail & Related papers  (2023-01-24T21:37:20Z)
• Sparse resultant based minimal solvers in computer vision and their connection with the action matrix [17.31412310131552]
  We show that for some camera geometry problems our extra-based method leads to smaller and more stable solvers than the state-of-the-art Grobner basis-based solvers. It provides a competitive alternative to popularner basis-based methods for minimal problems in computer vision.
  arXiv  Detail & Related papers  (2023-01-16T14:25:19Z)
• Blind Polynomial Regression [28.35687689204994]
  We state the (potentially partial) blind regression problem, rendering some of its theoretical properties, and propose algorithmic approaches to solve it. As a case-study, we apply our methods to a jitter-correction problem and corroborate its performance.
  arXiv  Detail & Related papers  (2022-10-21T10:54:35Z)
• SARAH-based Variance-reduced Algorithm for Stochastic Finite-sum Cocoercive Variational Inequalities [137.6408511310322]
  We consider the problem of finite-sum cocoercive variational inequalities. For strongly monotone problems it is possible to achieve linear convergence to a solution using this method.
  arXiv  Detail & Related papers  (2022-10-12T08:04:48Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  We present an end-to-end method to learn the proximal operator across non-family problems. We show that for weakly-ized objectives and under mild conditions, the method converges globally.
  arXiv  Detail & Related papers  (2022-01-28T05:53:28Z)
• A Boosting Approach to Reinforcement Learning [59.46285581748018]
  We study efficient algorithms for reinforcement learning in decision processes whose complexity is independent of the number of states. We give an efficient algorithm that is capable of improving the accuracy of such weak learning methods.
  arXiv  Detail & Related papers  (2021-08-22T16:00:45Z)
• Computational Barriers to Estimation from Low-Degree Polynomials [81.67886161671379]
  We study the power of low-degrees for the task of detecting the presence of hidden structures. For a large class of "signal plus noise" problems, we give a user-friendly lower bound for the best possible mean squared error achievable by any degree. As applications, we give a tight characterization of the low-degree minimum mean squared error for the planted submatrix and planted dense subgraph problems.
  arXiv  Detail & Related papers  (2020-08-05T17:52:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.