Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automated Proof of Polynomial Inequalities via Reinforcement Learning

Banglong Liu, Niuniu Qi, Xia Zeng, Lydia Dehbi, Zhengfeng Yang

TL;DR

This paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving polynomial inequalities, and formulate the inequality proving problem as a linear programming problem and encode it as a basis selection problem using reinforcement learning, achieving a non-negative Krivine basis.

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.

Automated Proof of Polynomial Inequalities via Reinforcement Learning

TL;DR

This paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving polynomial inequalities, and formulate the inequality proving problem as a linear programming problem and encode it as a basis selection problem using reinforcement learning, achieving a non-negative Krivine basis.

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.

Paper Structure

This paper contains 11 sections, 3 theorems, 20 equations, 3 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. LP Problem Transformation
  4. Dynamic Proof via Reinforcement Learning
  5. Environment Construction
  6. DQN Training
  7. Fast Multivariate Polynomial Multiplication
  8. Experiments
  9. Performance Evaluation
  10. Application: Maximum stable sets in graphs
  11. Conclusion

Key Result

Theorem 1

(Positivstellensatz krivine1964). Suppose $f$ is a polynomial that satisfies $f({\bf x}) > 0$ for all ${\bf x}\in [0,1]^n$. Then there exists an integer $l$ and non-negative scalars $\lambda_{\alpha,\beta}\geq 0$ such that:

Figures (3)

  • Figure 1: The framework of automated proof of polynomial inequalities based on RL
  • Figure 2: An undirected graph $\mathcal{G} = (\mathcal{V},\mathcal{E})$, The vertices set is $\mathcal{V}=\{x_1,\ldots,x_{10}\}$, and the edge set is $\mathcal{E} = \{x_ix_j = 0,x_i,x_j\in \mathcal{V}\}$, where $x_i$ and $x_j$ are vertices connected by an edge.
  • Figure 3: An example of proof generated by our agent

Theorems & Definitions (3)

  • Theorem 1
  • Lemma 1
  • Theorem 2