Research map / Reinforcement learning / Visual and representation RL
Automated Proof of Polynomial Inequalities via Reinforcement Learning
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes APPIRL, a DQN-based reinforcement learning method that selects Krivine basis terms to prove polynomial inequalities on the unit hypercube, with FFT-based polynomial multiplication, and applies it to maximum stable set.
Problem
Proving polynomial inequalities non-negative on a hyperrectangle with traditional algebraic (SOS/Lasserre-type) methods is limited by a fixed truncation degree D, which is either too expensive or too restrictive.
Approach
Formulates the proof as an LP over Krivine-basis terms x^alpha(1-x)^beta and trains a DQN agent to incrementally add basis terms (multiplying existing memory elements by x_i or 1-x_i) until the LP optimum becomes non-negative, avoiding a fixed degree bound; uses FFT-based multivariate polynomial multiplication to speed up action-space expansion.
Key results
- On 10 polynomial inequality benchmarks APPIRL averages 75.4 proof steps versus 445.1 for random search (about 6x fewer); on C8 it needs 3 steps vs 51 minimum for random search.
- On maximum stable set G3, APPIRL completes the proof in 37 steps versus 42 for LDPP; G1 and G2 match LDPP at 6 steps.
- On maximum stable set graphs R1-R5 and G1-G3, APPIRL finds the same stable set sizes as S2V-DQN.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use APPIRL instead of Random Search | Polynomial inequality proving · C1–C10 | proof steps: Across the 10 examples in the table, APPIRL requires an average of 75.4 steps, while Random search requires an average o | Helped |
| Use APPIRL instead of Random Search | Polynomial inequality proving · C2 | proof steps: 19 vs 13 (Smin); 19 vs 43 (Savg) | Helped |
| Use APPIRL instead of Random Search | Polynomial inequality proving · C3 | proof steps: 17 vs 7 (Smin); 17 vs 76 (Savg) | Helped |
| Use APPIRL instead of LDPP | Maximum stable set proof · G1 and G2 | proof steps: 6 vs 6 | No clear effect |
| Use APPIRL instead of LDPP | Maximum stable set proof · G3 | proof steps: 37 vs 42 | Helped |
| Use APPIRL instead of S2V-DQN | Maximum stable set · G1–G3 and R1–R5 | maximum stable set size: APPIRL and S2V-DQN report identical values for all listed graphs | No clear effect |
Limitations
- Comparison to random search is the main baseline on polynomial benchmarks; no comparison to SOS/Lasserre solvers reported
- Reward and performance depend on network architecture and hyperparameters, with variability across runs (C5 vs C6)
- Maximum stable set comparison with S2V-DQN shows equal results only, not improvement
Experimental setup
Datasets: 10 polynomial inequality examples from prior literature (C1-C10) maximum stable set benchmark graphs G1-G3 and R1-R5
Benchmarks: C1-C10 polynomial inequality examples G1-G3 maximum stable set graphs (vs LDPP) G1-G3, R1-R5 maximum stable set graphs (vs S2V-DQN)
Metrics: number of proof time steps maximum stable set size
Baselines: Random Search LDPP S2V-DQN
Builds on: DQN Positivstellensatz Sherali-Adams LDPP S2V-DQN
Closest papers by meaning
- Finding Simple Proofs for First-Order Optimization (NeurIPS 2026 · similarity 0.84)
- Learning Polynomial Problems with $SL(2, \mathbb{R})$-Equivariance (ICLR 2024 · similarity 0.83)
- Learning-enabled Polynomial Lyapunov Function Synthesis via High-Accuracy Counterexample-Guided Framework (CVPR 2025 · similarity 0.83)
- Computational Algebra with Attention: Transformer Oracles for Border Basis Algorithms (NeurIPS 2025 · similarity 0.82)
- Learning to Discover Iterative Spectral Algorithms (NeurIPS 2026 · similarity 0.82)
- Learning to compute Gröbner bases (NeurIPS 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.