用强化学习自动证明多项式不等式，突破传统方法的阶数限制。
Automated Proof of Polynomial Inequalities via Reinforcement Learning
- 将不等式证明转化为基于强化学习的基选择问题，寻找非负Krivine基。
- 结合快速傅里叶变换加速多项式乘法，提升动作空间搜索效率。
- 工具APPIRL成功解决最大稳定集问题，适用于数学证明与优化场景。
多项式不等式证明是多个数学领域基础性问题，在众多领域有广泛应用。现有传统代数方法依赖于在一组基上寻找多项式正定表示，但受限于截断阶数。本文提出一种基于强化学习的方法，用于寻找证明多项式不等式的{Krivine-basis}表示。具体而言，将不等式证明问题建模为线性规划（LP）问题，并通过强化学习（RL）编码为基选择问题，得到非负的{Krivine basis}。此外，采用基于快速傅里叶变换（FFT）的高效多变量多项式乘法方法，提升动作空间搜索效率。我们实现了名为{APPIRL}（Automated Proof of Polynomial Inequalities via Reinforcement Learning）的工具。在基准问题上的实验验证了该方法的可行性和有效性。此外，{APPIRL}已成功应用于求解最大稳定集问题。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。