From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

# From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
Source: [https://arxiv.org/html/2605.15445](https://arxiv.org/html/2605.15445)
###### Abstract

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability\. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions\. In parallel, LLM\-guided methods have made notable progress, particularly on competition\-style inequalities with a small number of variables\. To address the remaining scalability challenges, we propose NSPI, a neuro\-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial\-inequality proving\. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum\-Of\-Squares \(SOS\) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end\-to\-end pipeline from heuristic discovery to machine\-checked proof\. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method\.

Machine Learning, ICML

## 1Introduction

Polynomial inequalities play a fundamental role in areas such as optimization, control, and combinatorics\(Kaltofen et al\.,[2012](https://arxiv.org/html/2605.15445#bib.bib18); Parrilo,[2000a](https://arxiv.org/html/2605.15445#bib.bib36); Maréchal et al\.,[2015](https://arxiv.org/html/2605.15445#bib.bib32)\)\. The automation of complex inequality proving has recently emerged as an important benchmark for evaluating the limits of AI in mathematical reasoning\(Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48); Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54); He et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib15); Li et al\.,[2025c](https://arxiv.org/html/2605.15445#bib.bib27)\)\. Recent systems such as AlphaGeometry\(Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48); Chervonyi et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib8)\)and Seed\-Prover\(Chen et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib7),[a](https://arxiv.org/html/2605.15445#bib.bib6)\)have demonstrated impressive performance on Olympiad\-level problems, highlighting the potential of large language models \(LLMs\) for theorem proving\. Nevertheless, automated inequality proving remains highly challenging due to the long reasoning chains, vast search spaces, and substantial computational complexity involved, especially for high\-dimensional and multivariate cases\.

Symbolic computation has long been a cornerstone for proving polynomial inequalities\(Yang,[1999](https://arxiv.org/html/2605.15445#bib.bib56); Lasserre,[2002](https://arxiv.org/html/2605.15445#bib.bib22); Uray,[2020](https://arxiv.org/html/2605.15445#bib.bib52); Yang et al\.,[2023](https://arxiv.org/html/2605.15445#bib.bib57)\)\. A widely used approach is based on Sum\-of\-Squares \(SOS\) decomposition\(Kaltofen et al\.,[2012](https://arxiv.org/html/2605.15445#bib.bib18)\), which transforms the nonnegativity of a polynomial into a semidefinite programming \(SDP\) problem\. Modern computer algebra systems further support such pipelines with basic algebraic operations\(Heck & Koepf,[1993](https://arxiv.org/html/2605.15445#bib.bib16); De Moura & Bjørner,[2008](https://arxiv.org/html/2605.15445#bib.bib9); Meurer et al\.,[2017](https://arxiv.org/html/2605.15445#bib.bib34)\)\. However, purely symbolic approaches often suffer from poor scalability due to combinatorial explosion and typically fail to produce structured, human\-readable proofs\. In parallel, recent LLM\-based methods have substantially advanced automated formal theorem proving\(Lample et al\.,[2022](https://arxiv.org/html/2605.15445#bib.bib20); Xin et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib55); Ren et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib44); Lin et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib28); Wang et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib53); Lin et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib29)\)integrated with proof assistants such as Lean\(De Moura et al\.,[2015](https://arxiv.org/html/2605.15445#bib.bib10)\)and Isabelle\(Paulson,[1990](https://arxiv.org/html/2605.15445#bib.bib40)\)\. Nevertheless, their performance on complex algebraic inequalities remains limited by the scarcity formalized training data\.

To address the above challenges, a promising approach is to integrate neural and symbolic methods, thereby combining the strengths of structured reasoning and symbolic precision while mitigating dependence on large\-scale formalized training data\(Heule et al\.,[2016](https://arxiv.org/html/2605.15445#bib.bib17); Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48); Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54); Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25)\)\. However, existing approaches \(e\.g\., AIPS\(Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54)\)\) remain limited in two key aspects: they mainly target low\-dimensional cases \(e\.g\., ternary or quaternary polynomials\), and typically restrict the role of LLMs to search guidance or strategy selection, since directly using LLMs to generate symbolic conjectures remains difficult to control and certify\. In this paper, we propose a new neuro\-symbolic framework for polynomial inequality proving that targets unconstrained polynomial inequality scenarios, high\-dimensional multivariate problems and elevates LLMs to primary conjecture generators\. By formulating inequality proving as SOS\-based certification and tightly coupling LLM\-driven hypothesis generation with symbolic refinement and formal verification, our approach establishes an end\-to\-end pipeline from heuristic discovery to certified proof, significantly extending the scope of neuro\-symbolic automated theorem proving\.

The main contributions can be summarized as follows:

- •We propose a neuro\-symbolic approach for automated polynomial inequality proving, which automatically generates complete formal proofs of inequalities through a pipeline of neural conjecture, symbolic correction, and Lean verification\.
- •We develop a principled reliability bridge that integrates LLM\-based heuristic conjecture generation with symbolic exact certification, transforming neural conjectures into machine\-checkable proofs and enabling automated inequality proving to scale to higher\-dimensional multivariate cases\.
- •Extensive experiments on522522challenging inequality problems demonstrate the effectiveness of the proposed method, which outperforms both symbolic computation\-based and LLM\-assisted approaches, especially on problems with up to1010variables\.

## 2Related Work

Symbolic Methods for Inequality Proving\.Polynomial inequality proving has traditionally been approached through symbolic computation\. A classical method is based on the SOS methodology\(Kaltofen et al\.,[2012](https://arxiv.org/html/2605.15445#bib.bib18); Martin\-Dorel & Roux,[2017](https://arxiv.org/html/2605.15445#bib.bib33)\), which reduces nonnegativity certification to the existence of an SOS decomposition and further to solving SDP problem\. Meanwhile, computer algebra systems such as Maple\(Heck & Koepf,[1993](https://arxiv.org/html/2605.15445#bib.bib16)\), Z3\(De Moura & Bjørner,[2008](https://arxiv.org/html/2605.15445#bib.bib9)\)and SymPy\(Meurer et al\.,[2017](https://arxiv.org/html/2605.15445#bib.bib34)\)provide fundamental symbolic capabilities, which support algebraic preprocessing and manipulation in inequality\-proving pipelines\. Nevertheless, purely symbolic approaches typically struggle to produce human\-readable reasoning steps and often suffer from combinatorial explosion as the problem dimension increases, particularly for multivariate and algebraically intensive polynomial inequalities\.

LLM\-based Formal Theorem Proving\.In recent years, LLM\-based automated theorem proving has advanced rapidly\. Various approaches integrate LLMs with interactive proof assistants such as Lean\(De Moura et al\.,[2015](https://arxiv.org/html/2605.15445#bib.bib10)\)to produce machine\-checkable formal proofs\. One line of work fine\-tunes models on large\-scale corpora of formal proofs to generate proof strategies or local proof tactics\(Polu & Sutskever,[2020](https://arxiv.org/html/2605.15445#bib.bib43); Lample et al\.,[2022](https://arxiv.org/html/2605.15445#bib.bib20); Xin et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib55)\)\. Another line explores end\-to\-end generation of complete formal proofs\(Ren et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib44); Lin et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib28); Wang et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib53); Lin et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib29)\), exemplified by Goedel\-Prover\(Lin et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib28)\),Kimina Prover\(Wang et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib53)\)and DeepSeek\-Prover\-V2\(Ren et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib44)\)\. However, LLM\-based methods are limited by the scarcity and uneven quality of formal\-proof data, and thus remain weak on high\-dimensional inequalities\.

Neuro\-Symbolic Theorem Proving\.To bridge the scalability limitations of purely symbolic methods and the data bottleneck of purely neural approaches, recent work has explored neuro\-symbolic integration for automated theorem proving\(Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48); Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54); Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25); Chervonyi et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib8)\)\. These methods typically combine neural models with symbolic solvers, using learning\-based components to guide or prioritize symbolic reasoning or derivation steps\. Representative systems such as AlphaGeometry\(Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48)\), AIPS\(Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54)\), and LIPS\(Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25)\)demonstrate the effectiveness of this paradigm in geometry and algebraic inequality proving\. In contrast, while existing approaches mainly focus on learning\-guided derivation or strategy selection, we treat LLMs as generators of symbolic conjectures and machine\-checkable formal verification\. Centered on verifiable SOS certificates, our framework establishes an end\-to\-end neuro\-symbolic pipeline for tackling more complex multivariate polynomial inequalities\.

## 3Preliminaries

![Refer to caption](https://arxiv.org/html/2605.15445v1/x1.png)Figure 1:Overview of Neuro\-Symbolic SOS\-based Polynomial Inequality Proving \(NSPI\)\. \(1\)Neural Conjecture Module: Non\-negative polynomial\-SOS representation pairs are constructed using computation\-driven and structure\-driven approaches\. A Large Language Model \(LLM\) is trained on the constructed data to function as an SOS structure conjecturer, which generates corresponding SOS representations based on the non\-negative polynomials and ranks them according to the magnitude of the errors\. \(2\)Symbolic Correction Module: An exact SOS representation is derived from the top\-ranked SOS structure conjectures through a symbolic computation process that involves Newton iteration and rational recovery\. \(3\)Formal Verification Module: Based on the exact SOS representations and predefined Lean proof templates, a complete Lean formal proof is automatically generated\.Letℝ​\[x\]:=ℝ​\[x1,…,xn\]\\mathbb\{R\}\[x\]:=\\mathbb\{R\}\[x\_\{1\},\\ldots,x\_\{n\}\]be the ring of polynomials innnvariables with coefficients in the real fieldℝ\\mathbb\{R\}\. A polynomialf​\(x\)∈ℝ​\[x\]f\(x\)\\in\\mathbb\{R\}\[x\]is said to be nonnegative or positive semidefinite \(PSD\) iff​\(x\)≥0f\(x\)\\geq 0for allx∈ℝnx\\in\\mathbb\{R\}^\{n\}\. In this work, we focus on automated proving of unconstrained polynomial nonnegativity: givenf∈ℝ​\[𝐱\]f\\in\\mathbb\{R\}\[\\mathbf\{x\}\], our goal is to formally prove

f​\(x\)≥0,∀x∈ℝn\.\\displaystyle f\(x\)\\geq 0,\\quad\\forall x\\in\\mathbb\{R\}^\{n\}\.\(1\)Beyond establishing \([1](https://arxiv.org/html/2605.15445#S3.E1)\) mathematically, automated theorem proving additionally requires certificates that are rigorous and machine\-checkable, rather than purely numerical or heuristic validations\.

A widely\-used sufficient certificate for \([1](https://arxiv.org/html/2605.15445#S3.E1)\) is a*sum\-of\-squares*\(SOS\) decomposition\. A polynomialf​\(x\)f\(x\)is said to be an SOS, if there exist polynomialsf1​\(x\),…,fm​\(x\)f\_\{1\}\(x\),\\ldots,f\_\{m\}\(x\)such that

f​\(x\)=∑i=1mfi​\(x\)2\.\\displaystyle f\(x\)=\\sum\_\{i=1\}^\{m\}f\_\{i\}\(x\)^\{2\}\.\(2\)It is immediatef​\(x\)f\(x\)being SOS implies that is nonnegative overℝn\\mathbb\{R\}^\{n\}, hence an explicit SOS decomposition provides a constructive certificate of \([1](https://arxiv.org/html/2605.15445#S3.E1)\)\. Notice that necessarilyf​\(x\)f\(x\)must be of even degree2​d2d\. Let𝐯d​\(x\)\\mathbf\{v\}\_\{d\}\(x\)be the vector

𝐯d​\(x\)=\[1,x1,x2,…,xn,x12,x1​x2,…,xnd\]𝖳,\\mathbf\{v\}\_\{d\}\(x\)=\[1,x\_\{1\},x\_\{2\},\\ldots,x\_\{n\},x\_\{1\}^\{2\},x\_\{1\}x\_\{2\},\\ldots,x\_\{n\}^\{d\}\]^\{\\mathsf\{T\}\},of all monomials inxxand whose degrees are at mostdd, which has dimensions​\(d\)=\(n\+dd\)s\(d\)=\\binom\{n\+d\}\{d\}\. Thenf​\(x\)f\(x\)is SOS if and only if there exists a symmetric positive semidefinite matrixG⪰0G\\succeq 0such that

f​\(x\)=𝐯​\(x\)𝖳​G​𝐯​\(x\)\.\\displaystyle f\(x\)=\\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}G\\mathbf\{v\}\(x\)\.\(3\)Equating coefficients in the identity \([3](https://arxiv.org/html/2605.15445#S3.E3)\) yields a system of linear equations that the entries ofGGmust satisfy\. Therefore, determining whetherf​\(x\)f\(x\)is SOS can be formulated as a semidefinite feasibility problem:

\{findG∈ℝs​\(d\)×s​\(d\)s\.t\.G⪰0,G=G𝖳,f​\(x\)=𝐯​\(x\)𝖳​G​𝐯​\(x\)\.\\displaystyle\\left\\\{\\begin\{aligned\} &\\text\{find\}&&G\\in\\mathbb\{R\}^\{s\(d\)\\times s\(d\)\}\\\\ &\\text\{s\.t\.\}&&G\\succeq 0,\\quad G=G^\{\\mathsf\{T\}\},\\\\ &&&f\(x\)=\\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}G\\mathbf\{v\}\(x\)\.\\end\{aligned\}\\right\.\(4\)However, SDP solvers typically return numerical solutions, while formal verification requires exact certificates\. This motivates our focus on constructing*exact*SOS certificates that can be directly checked in a proof assistant\.

## 4Methodology

In this section, we introduceNeuro\-Symbolic SOS\-basedPolynomialInequalityProving \(NSPI\), a neuro\-symbolic framework for automated proving of unconstrained polynomial inequalities\. NSPI is designed as a pipeline that integrates LLM\-based conjecture with symbolic computation and formal verification\. The overall architecture of NSPI is illustrated in Fig\.[1](https://arxiv.org/html/2605.15445#S3.F1), which depicts the following three main stages:

\[Neural Conjecture\]\.The LLM is employed as a*structure conjecturer*for sum\-of\-squares \(SOS\) representations\. By combining computation\-driven and structure\-driven strategies, we construct a diverse dataset of nonnegative polynomials and their corresponding SOS pair forms\. The conjecturer is trained on synthetically generated data via a progressive two\-stage training scheme, enabling the LLM to more accurately predict plausible SOS structures for given polynomials \(see more details in Section[4\.1](https://arxiv.org/html/2605.15445#S4.SS1)\)\.

\[Symbolic Correction\]\.Symbolic computation serves as a*precision bridge*in SOS\-based proving\. At this point, symbolic computation tools are employed to refine the approximate SOS decomposition produced in the previous stage\. By combining Newton\-type iterative refinement with rational recovery techniques, numerical solutions are systematically converted into exact rational representations, yielding a precise SOS certificate of the target polynomial\. \(see more details in Section[4\.2](https://arxiv.org/html/2605.15445#S4.SS2)\)\.

\[Formal Verification\]\.This module converts the precise SOS decomposition into machine\-checkable Lean proof templates, thereby ensuring that the entire proving process, from conjecture to certificate, is fully verified by a trusted formal kernel\. \(see more details in Section[4\.3](https://arxiv.org/html/2605.15445#S4.SS3)\)\.

### 4\.1Neural Conjecture: LLM\-Guided SOS Generation

Given an input polynomial, the*neural conjecture*component leverages the structural conjecturing capability of large language models to propose candidate the sum\-of\-squares decomposition\. The overall procedure is organized into two complementary parts as follows:

- i\)Constructing SOS training data: we construct large\-scale polynomial–SOS training pairs by generating SOS polynomials through Gram matrix synthesis, using both computation\-driven and structure\-driven mechanisms to obtain PSD matrices with controlled coefficient properties\. \(see Subsection[4\.1\.1](https://arxiv.org/html/2605.15445#S4.SS1.SSS1)\)
- ii\)Training the SOS structure conjecturer: we train an SOS structure conjecturer via a progressive two\-stage scheme, where supervised fine\-tuning provides a cold start on the synthetic corpus and curriculum\-based reinforcement learning further improves conjecturing performance on harder multivariate instances\. \(see Subsection[4\.1\.2](https://arxiv.org/html/2605.15445#S4.SS1.SSS2)\)

#### 4\.1\.1SOS Data Construction Method

Constructing nonnegative polynomials and and their corresponding SOS representations in a systematic and numerically well\-behaved manner is a nontrivial task\. A straightforward approach is to randomly sample polynomialsfi​\(x\)f\_\{i\}\(x\)and constructf​\(x\)=∑ifi​\(x\)2\.f\(x\)=\\sum\_\{i\}f\_\{i\}\(x\)^\{2\}\.However, this naive strategy suffers from two major limitations: \(1\) the coefficients of the generatedfi​\(x\)f\_\{i\}\(x\)are typically non\-integer, which makes the resulting polynomial inconsistent with the typical symbolic representations that require integer coefficients, and \(2\) the expansion of randomly generated squared polynomials often leads to severe coefficient swelling, producing polynomials with unreasonably large or unbalanced coefficients\.

To address these issues, we develop a novel data construction method grounded in the algebraic structure of SOS decomposition\. As reviewed in[Section3](https://arxiv.org/html/2605.15445#S3), a polynomialf​\(x\)f\(x\)is SOS if and only if there exists a positive semidefinite \(PSD\) Gram matrixG~\\widetilde\{G\}such thatf​\(x\)=𝐯​\(x\)𝖳​G~​𝐯​\(x\),f\(x\)=\\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}\\widetilde\{G\}\\mathbf\{v\}\(x\),where𝐯​\(x\)\\mathbf\{v\}\(x\)denotes the vector of monomials\. Consequently, the problem of generating suitable polynomial–SOS pairs reduces to the problem of*constructing a PSD Gram matrixG~\\widetilde\{G\}*with controlled coefficient structure\.

Based on this observation, we propose two families of SOS data construction methods, namely*computation\-driven*and*structure\-driven*approaches\. Once a Gram matrixG~\\widetilde\{G\}is obtained by either approach, the SOS polynomialf​\(x\)f\(x\)is generated by instantiating a monomial basis𝐯​\(x\)\\mathbf\{v\}\(x\)\.

\(1\) Computation\-Driven Methods\.We first consider constructing the Gram matrixG~\\widetilde\{G\}through numerical procedures\. The objective is to systematically control the magnitude and precision of the coefficients while ensuring that the resultingG~~\\widetilde\{G\}remains positive semi\-definite\. The computation\-driven methods comprise two main approaches\.

![Refer to caption](https://arxiv.org/html/2605.15445v1/x2.png)Figure 2:Two\-stage training of the SOS conjecturer: \(1\)Cold Start: supervised fine\-tuning \(SFT\) on large\-scale synthetic polynomial–SOS pairs; \(2\)Progressive reinforcement learning: curriculum\-based GRPO on challenging training data\.\[Explicit Algebraic Construction\]\.One direct way to obtain a PSD Gram matrixG~\\widetilde\{G\}is based on spectral shifting\. Specifically, we first generate a symmetric integer matrixG∈𝕊mG\\in\\mathbb\{S\}^\{m\}and compute its smallest eigenvalueλmin\\lambda\_\{\\min\}\. Setting

G~=G−k​I⪰0​, where​k=⌊λmin⌋\\displaystyle\\widetilde\{G\}=G\-kI\\succeq 0\\text\{, where \}k=\\left\\lfloor\\lambda\_\{\\min\}\\right\\rfloor\(5\)yields a matrixG~⪰0\\widetilde\{G\}\\succeq 0, since its smallest eigenvalue satisfiesλmin−k≥0\\lambda\_\{\\min\}\-k\\geq 0\.

Alternatively, a PSD Gram matrix can also be constructed in factored form\. LetL∈ℤm×kL\\in\\mathbb\{Z\}^\{m\\times k\}\(k≤mk\\leq m\) be a sparse integer matrix and letD∈ℝk×kD\\in\\mathbb\{R\}^\{k\\times k\}be a positive definite diagonal matrix, wherekkcorresponds to the number of squared terms in the SOS decomposition\. Then the matrix

G~=L𝖳​D​L\\displaystyle\\widetilde\{G\}=L^\{\\mathsf\{T\}\}DL\(6\)is symmetric positive semidefinite by construction\.

\[Optimization\-Based Approach\]\.Another computation\-driven method constructs the Gram matrixG~\\widetilde\{G\}through Linear Matrix Inequality \(LMI\) optimization\. This approach employs LMI optimization to compute an approximate SOS representation, followed by controlled adjustment to obtain an exact integer\-coefficient solution\. Supposef​\(x\)∈ℤ​\[x\]f\(x\)\\in\\mathbb\{Z\}\[x\]is a randomly selected integer\-coefficient polynomial\. We first solve the following semidefinite program:

\{max​λs\.t\.​f​\(x\)=𝐯​\(x\)𝖳​G​𝐯​\(x\)G−λ​I⪰0,G=G𝖳\.\\displaystyle\\begin\{cases\}\\text\{max\}\\ \\lambda\\\\ \\text\{s\.t\.\}\\ f\(x\)=\\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}G\{\\mathbf\{v\}\}\(x\)\\\\ \\ \\ \\ \\ \\ \\ G\-\\lambda I\\succeq 0,\\quad G=G^\{\\mathsf\{T\}\}\.\\end\{cases\}\(7\)Let\(λ,G\)\(\\lambda,G\)be an optimal solution\. SinceG−λ​I⪰0G\-\\lambda I\\succeq 0, for any integerk≥−λk\\geq\-\\lambdawe haveG\+k​I⪰0G\+kI\\succeq 0\. Choosingk:=⌈−λ⌉∈ℤk:=\\lceil\-\\lambda\\rceil\\in\\mathbb\{Z\}yieldsG\+k​I⪰0G\+kI\\succeq 0, and therefore

f~​\(x\):=f​\(x\)\+𝐯​\(x\)𝖳​\(k​I\)​𝐯​\(x\)=𝐯​\(x\)𝖳​\(G\+k​I\)​𝐯​\(x\)\\tilde\{f\}\(x\)\\ :=\\ f\(x\)\+\\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}\(kI\)\\mathbf\{v\}\(x\)\\ =\\ \\mathbf\{v\}\(x\)^\{\\mathsf\{T\}\}\(G\+kI\)\\mathbf\{v\}\(x\)is SOS polynomial with integer coefficients\. Then the Gram matrix is updated asG~=G\+k​I\\widetilde\{G\}=G\+kI\. Appendix[B\.1](https://arxiv.org/html/2605.15445#A2.SS1)provides the theoretical foundations for the aforementioned computation\-driven methods\.

\(2\) Structure\-Driven Methods\.This category constructs the Gram matrixG~\\widetilde\{G\}by exploiting algebraic matrix structures that guarantee positive semidefiniteness by design, most notably diagonally dominant \(dd\) matrices and scaled diagonally dominant \(sdd\) matrices\.

Specifically, a matrixG∈ℝm×mG\\in\\mathbb\{R\}^\{m\\times m\}is defined as diagonally dominant if it satisfies the following condition:Gi​i≥∑j≠i\|Gi​j\|,∀iG\_\{ii\}\\geq\\sum\_\{j\\neq i\}\|G\_\{ij\}\|,\\forall i\. By Gershgorin’s circle theorem\(Gerschgorin,[1931](https://arxiv.org/html/2605.15445#bib.bib13)\), any symmetricGGthat satisfies the diagonal dominance condition is guaranteed to be positive semidefinite\. In this case,G~\\widetilde\{G\}can be directly initialized as a diagonally dominant matrix\. Furthermore, we*construct*G~\\widetilde\{G\}in a structured diagonally dominant form by restricting it to a non\-negative combination ofmmrank\-one generators inspired by\(Barker & Carlson,[1975](https://arxiv.org/html/2605.15445#bib.bib4)\):

G~=∑i=1m2ηi​Ui,\\displaystyle\\widetilde\{G\}=\\sum\_\{i=1\}^\{m^\{2\}\}\\eta\_\{i\}U\_\{i\},\(8\)whereG~\\widetilde\{G\}is anm×mm\\times msymmetric matrix,ηi≥0\\eta\_\{i\}\\geq 0, andUi=𝐮i​𝐮i⊤U\_\{i\}=\\mathbf\{u\}\_\{i\}\\mathbf\{u\}\_\{i\}^\{\\top\}, with𝐮i∈ℝm\\mathbf\{u\}\_\{i\}\\in\\mathbb\{R\}^\{m\}having at most two non\-zero components, each equal to±1\\pm 1\. This representation provides a convenient structural parameterization of PSD Gram matrices, and naturally extends to the scaled diagonally dominant case to introduce greater flexibility\. Appendix[B\.2](https://arxiv.org/html/2605.15445#A2.SS2)provides the theoretical foundations and more details of structure\-driven methods\.

#### 4\.1\.2Training the SOS Structure Conjecturer

To obtain an LLM\-based SOS structure conjecturer with strong structural reasoning capability, we design a progressive two\-stage training scheme\. As illustrated in Fig\.[2](https://arxiv.org/html/2605.15445#S4.F2), the procedure consists of two phases\. \(1\)*Cold Start*:*endow*the model with the ability to conjecture SOS structures via supervised fine\-tuning \(SFT\) on the constructed polynomial\-SOS pair data\. \(2\)*Progressive Reinforcement Learning*:*further enhance*the model’s SOS\-structure conjecturing performance via curriculum\-based reinforcement learning \(RL\) on challenging data\.

Cold Start\.We perform SFT on the base model using over one million synthetic data samples\. These samples are generated via the method described in Section[4\.1\.1](https://arxiv.org/html/2605.15445#S4.SS1.SSS1), with each instance formulated as a pair\(f​\(x\),S\)\(f\(x\),S\), wheref​\(x\)f\(x\)denotes a non\-negative polynomial andSSrepresents its corresponding SOS decomposition\. This stage endows the base model with the foundational capability for SOS structural reasoning, serving as a critical precursor to the subsequent reinforcement learning phase\. Further details regarding the synthetic dataset are provided in Appendix[D\.2](https://arxiv.org/html/2605.15445#A4.SS2)\.

Progressive Reinforcement Learning\.We further optimize the model’s SOS structural reasoning through progressive reinforcement learning on challenging tasks\. Specifically, we curate the training instances that remain unsolved by the cold\-started model into an easy\-to\-hard curriculum and conduct curriculum\-based Group Relative Policy Optimization \(GRPO\)\(Shao et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib46)\)\. The reward function is designed with three critical components:

\[Accuracy Reward\]\.The accuracy reward encourages SOS structure conjectures with smaller errors compared to the original polynomial\. It measures the numerical fidelity of the conjecture and is computed as

RAccuracy=11\+α​‖𝐟​\(x\)−𝐟^​\(x\)‖2,\\displaystyle R\_\{\\text\{Accuracy\}\}=\\frac\{1\}\{1\+\\alpha\\\|\\mathbf\{f\}\(x\)\-\\hat\{\\mathbf\{f\}\}\{\(x\)\}\\\|\_\{2\}\},\(9\)where𝐟​\(𝐱\)\\mathbf\{f\(x\)\}represents the original polynomial,𝐟^​\(𝐱\)\\hat\{\\mathbf\{f\}\}\(\\bf x\)denotes the SOS structure conjecture generated by the model, andα\\alphais a scaling factor\.

\[Format Reward\]\.A binary indicator ensuring the output strictly adheres to the predefined SOS structural template and delimiters \(e\.g\.,<SOS Expression\>\)\.

\[Algebraic Structure Penalty\]\.The algebraic structure consistency penalty is designed to ensure that the set of nonzero monomials in the SOS strucure conjecture closely matches that of the original polynomial, which comprises asoft penaltyand ahard penalty\. Appendix[D\.3](https://arxiv.org/html/2605.15445#A4.SS3)details the specific computation procedure and provides further details on the progressive reinforcement learning procedure\.

### 4\.2Symbolic Correction: Exact Rational Recovery

In this part, thesymbolic correctionmodule serves as a precision bridge between model\-generated SOS structure conjecture and the exact representation required for formal verification, which encompasses two stages: Gauss–Newton refinement and rational recovery\.

Gauss–Newton Refinement\.After obtaining the SOS structural conjecturef^​\(x\)\\hat\{f\}\{\(x\)\}from theneural conjecturemodule, we perform Gauss–Newton refinement to enhance the numerical precision of the SOS representation\.

First, the corresponding monomial basis𝐯​\(x\)\{\\mathbf\{v\}\}\(x\)is extracted, and an initial floating\-point Gram matrix𝐆\\mathbf\{G\}is constructed such thatf^​\(x\)≈𝐯​\(x\)𝖳​𝐆𝐯​\(x\)\\hat\{f\}\{\(x\)\}\\approx\{\\mathbf\{v\}\}\(x\)^\{\\mathsf\{T\}\}\\mathbf\{G\}\{\\mathbf\{v\}\}\(x\)\. To refine𝐆\\mathbf\{G\}using the Gauss–Newton iteration, we compute the Cholesky decomposition of𝐆\\mathbf\{G\}:

f^​\(𝐱\)≈𝐯​\(𝐱\)𝖳​L​L𝖳​𝐯​\(𝐱\)=∑i=1k\(∑αci,α​𝐱α\)2,\\displaystyle\\hat\{f\}\(\\mathbf\{x\}\)\\approx\\mathbf\{v\}\(\\mathbf\{x\}\)^\{\\mathsf\{T\}\}LL^\{\\mathsf\{T\}\}\\mathbf\{v\}\(\\mathbf\{x\}\)=\\sum\_\{i=1\}^\{k\}\\left\(\\sum\_\{\\alpha\}c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}\\right\)^\{2\},\(10\)wherekkis the rank of the matrix𝐆\\mathbf\{G\}, andL​L𝖳LL^\{\\mathsf\{T\}\}denotes the Cholesky factorization of the Gram matrix𝐆\\mathbf\{G\}\.

The Gauss–Newton iteration is applied to compute the coefficient correction termΔ​ci,α​𝐱α\\Delta c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}such that

f^​\(𝐱\)=∑i=1k\(∑αci,α​𝐱α\+Δ​ci,α​𝐱α\)2,\\displaystyle\\hat\{f\}\(\\mathbf\{x\}\)=\\sum\_\{i=1\}^\{k\}\\left\(\\sum\_\{\\alpha\}c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}\+\\Delta c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}\\right\)^\{2\},\(11\)
whereΔ​ci,α​𝐱α\\Delta c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}represents the perturbation to the polynomial coefficients, and the Gram matrix is updated as𝐆\+Δ​𝐆\\mathbf\{G\}\+\\Delta\\mathbf\{G\}\. The optimization objective is to minimize the backward error:

θ=‖f^​\(𝐱\)−𝐯​\(x\)T​𝐆𝐯​\(x\)‖\.\\displaystyle\\theta=\|\|\\hat\{f\}\(\\mathbf\{x\}\)\-\{\\mathbf\{v\}\}\(x\)^\{T\}\\mathbf\{G\}\{\\mathbf\{v\}\}\(x\)\|\|\.\(12\)Gauss–Newton iteration terminates whenθ\\thetafalls below a predefined tolerance thresholdτ\\tau\. This process is crucial for the subsequent rational recovery process, ensuring that the obtained SOS representation achieves high precision\. Appendix[C\.1](https://arxiv.org/html/2605.15445#A3.SS1)provides further details of the procedure\.

Rational Recovery\.The numerical Gram matrixGNG\_\{N\}obtained from Gauss–Newton refinement contains inherent floating\-point errors\. Our objective is to transform the matrix into an exact rational PSD matrix that rigorously satisfies the polynomial identity without numerical uncertainty, thereby yielding an exact SOS representation\.

According to a classical result on rational recovery\(Peyrl & Parrilo,[2008a](https://arxiv.org/html/2605.15445#bib.bib41)\),111If a polynomial admits a Gram matrix lying strictly in the interior of the PSD cone, then there exists a thresholdδ\>0\\delta\>0such that any numerical Gram matrix withinδ\\deltaof the exact solution can be converted into an exact rational PSD matrix by combining rational approximation with orthogonal projectionwe distinguish two recovery regimes depending on the numerical rank of the refined solution\. \(1\)Interior\-point case: when the refined Gram matrix lies strictly in the interior of the PSD cone, we project it orthogonally onto the affine subspace defined by the SOS constraints and then rationalize the resulting matrix\. \(2\)Boundary case: when the matrix is numerically rank\-deficient, direct matrix rationalization is avoided\. Instead, we perform a truncatedL​D​L⊤LDL^\{\\top\}factorization followed by simultaneous Diophantine approximation to recover rational vectors while preserving the rank structure\. Appendix[C](https://arxiv.org/html/2605.15445#A3)provides further details of Symbolic Correction module\.

### 4\.3Formal Verification: Lean Proof Generation

After obtaining the exact SOS certificates, theformal verificationmodule generates a complete Lean proof\. By integrating pre\-defined proof templates with theneural conjectureandsymbolic correctionmodules, we implement a callable Lean tactic,llm\_ineq\. Given a target polynomial and its exact SOS certificate,llm\_ineqautomatically constructs a complete Lean proof by discharging two obligations:

Equality between polynomial and SOS certificate\.Lean expands the polynomial and the SOS expression into canonical forms and checks their equality via thelinear\_combinationtactic\. For example, the code below shows how Lean verifies the equality:

haveh\_eq:p=\(terms\.map\(fun\(q,k\)=\>k\*q^2\)\)\.sum:=by

linear\_combination

Nonnegativity of the SOS expansion\.Lean provides several built\-in strategies for proving nonnegativity\. The nonnegativity of the SOS expression is proved byLean’spositivitytactic, which recursively applies standard rules \(e\.g\.,sq\_nonneg,mul\_nonneg,add\_nonneg\)\.

haveh\_nn:0<=\(terms\.map\(fun\(q,k\)=\>k\*q^2\)\)\.sum:=by

positivity

Further details on the proof templates and illustrative examples are provided in Appendix[E](https://arxiv.org/html/2605.15445#A5)\.

## 5Experiments

Table 1:Comparative Performance on PolyIneqBench \(n=3 to 10\)\.Pass: success rate within 1 hour;t\(s\): mean execution time of solved instances\.DS\-Prover\-v2denotes DeepSeek\-Prover\-v2\. Best and second\-best results are inboldandunderlined, respectively\.Method Namen=3n=4n=5n=6n=7n=8n=9n=10Passt\(s\)Passt\(s\)Passt\(s\)Passt\(s\)Passt\(s\)Passt\(s\)Passt\(s\)Passt\(s\)Symbol\-based MethodMaple97\.6%24\.639\.0%107\.426\.7%451\.28\.2%54\.96\.7%821\.56\.67%456\.33\.3%3176\.61\.7%1525\.6Z397\.6%0\.632\.5%21\.823\.3%101\.919\.7%196\.41\.7%65\.01\.7%1598\.60\.0%NA0\.0%NALLM\-based ProverDS\-Prover\-v242\.9%19\.82\.6%17\.90\.0%NA0\.0%NA0\.0%NA0\.0%NA0\.0%NA0\.0%NAGoedel\-Prover\-v220\.2%189\.65\.2%136\.40\.0%NA0\.0%NA0\.0%NA0\.0%NA0\.0%NA0\.0%NAKimina\-Prover36\.9%117\.05\.2%111\.70%NA0\.0%NA1\.7%120\.60\.0%NA1\.7%115\.80\.0%NAGeneral\-purpose LLMGPT\-5\.226\.2%56\.810\.4%86\.71\.7%51\.84\.9%154\.43\.3%75\.33\.3%55\.93\.3%68\.31\.7%49\.2Gemini\-3\-Pro22\.6%91\.224\.7%102\.436\.7%109\.821\.3%138\.915\.0%140\.715\.0%126\.713\.3%143\.56\.7%116\.7DeepSeek\-V3\.214\.3%368\.46\.5%420\.91\.7%526\.81\.6%495\.85\.0%393\.85\.0%561\.51\.7%358\.03\.3%678\.9Hybrid systemLIPS71\.4%82\.527\.3%131\.013\.3%141\.611\.5%195\.78\.3%150\.28\.3%153\.11\.7%148\.70\.0%NANSPI \(ours\)44\.1%16\.340\.3%14\.436\.7%20\.029\.5%21\.426\.7%29\.621\.7%63\.915\.0%20\.811\.7%58\.3![Refer to caption](https://arxiv.org/html/2605.15445v1/x3.png)Figure 3:Distribution of sample counts across data source categories in PolyIneq\-Real\.![Refer to caption](https://arxiv.org/html/2605.15445v1/x4.png)Figure 4:Performance of different methods on PolyIneqBench \(PolyIneq\-Real and PolyIneq\-Synth\)\.![Refer to caption](https://arxiv.org/html/2605.15445v1/x5.png)Figure 5:Performance on PolyIneqBench across different training stages\.Left:Success rate heatmap showing capability boundary migration\.Middle:Overall performance gains from base model through RL stages\.Right:Scalability trends across curriculum groups\.### 5\.1A Challenging Benchmark for Multivariate Polynomial Inequalities

Existing mathematical benchmarks for theorem provingdo notencompass proofs ofhigh\-dimensional multivariatepolynomial inequalities\. To fill this gap, we constructPolyIneqBench, a challenging benchmark for unconstrained polynomial inequality proving\. It contains522complex inequality problems with3 to 10variables, all transformed into the form of \([1](https://arxiv.org/html/2605.15445#S3.E1)\) and formalized in Lean\. Among them, 102 problems are collected from international mathematics competitions and other authoritative sources\(Chen,[2014](https://arxiv.org/html/2605.15445#bib.bib5); Tung,[2012](https://arxiv.org/html/2605.15445#bib.bib50); Riasat,[2008](https://arxiv.org/html/2605.15445#bib.bib45); Manfrino et al\.,[2010](https://arxiv.org/html/2605.15445#bib.bib31); Mildorf,[2005](https://arxiv.org/html/2605.15445#bib.bib35); Parvardi,[2011](https://arxiv.org/html/2605.15445#bib.bib39); Tung & Zhe,[2014](https://arxiv.org/html/2605.15445#bib.bib51); Lee,[2005](https://arxiv.org/html/2605.15445#bib.bib24); Andreescu,[2019](https://arxiv.org/html/2605.15445#bib.bib2)\), formingPolyIneq\-Real\. Fig\.[3](https://arxiv.org/html/2605.15445#S5.F3)shows the distribution of data sources for PolyIneq\-Real\. Notably, existing competition problems are largely concentrated in the 3 or 4\-variable setting\. To extend the benchmark to more challenging high\-dimensional cases, we synthesize problems with 4 to 10 variables to buildPolyIneq\-Synth\. Appendix[G\.3](https://arxiv.org/html/2605.15445#A7.SS3)provides further details on PolyIneqBench\.

### 5\.2Experimental Setup

We compare our method NSPI with several state\-of\-the\-art inequality\-proving approaches\. Symbolic computation–based baselines include Maple\(Heck & Koepf,[1993](https://arxiv.org/html/2605.15445#bib.bib16)\)and Z3\(De Moura & Bjørner,[2008](https://arxiv.org/html/2605.15445#bib.bib9)\)\. State\-of\-the\-art LLM\-based provers include DeepSeek\-Prover\-V2\(Ren et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib44)\), Goedel\-Prover\-V2\(Lin et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib28)\), and Kimina Prover\(Wang et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib53)\)\. We also consider recent general\-purpose LLMs, including GPT\-5\.2, Gemini\-3\-Pro, and DeepSeek\-V3\.2\(DeepSeek\-AI,[2025](https://arxiv.org/html/2605.15445#bib.bib11)\), as well as the hybrid system LIPS\(Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25)\)\. We evaluate all methods on PolyIneqBench using proof success rate and the average runtime of successful proofs, and further examine performance trends as the polynomial degree increases to assess scalability\. Appendix[G](https://arxiv.org/html/2605.15445#A7)provides additional implementation details and experimental configurations\.

### 5\.3Main Results

##### Best performance under multivariate scenarios\.

[Table1](https://arxiv.org/html/2605.15445#S5.T1)presents the comparative performance of various baseline methods on the PolyIneqBench across different numbers of variablesnn\. As illustrated, a general downward trend in pass rates is observed for all methods as the problem dimensionality increases\. Overall, the proposed NSPI framework outperforms symbol\-based methods, pure LLM\-based approaches, and other hybrid systems, achieving best performance\. Notably, while baseline methods struggle as the variable count scales ton=10n=10, NSPI maintains a consistent pass rate of 11\.7%\. Our analysis further reveals several key insights: \(1\) symbolic methods, though proficient in low\-dimensional settings, suffer from exponential computational complexity as dimensionality increases and lack the ability to generate human\-readable formal proofs; \(2\) state\-of\-the\-art \(SOTA\) LLM\-based provers encounter significant performance bottlenecks when tackling competition\-level polynomial inequalities exceeding 5 variables; and \(3\) although general\-purpose LLMs like Gemini\-3\-Pro exhibit commendable scalability in certain cases, their overall performance remains inferior to NSPI\.

##### Challenging synthetic data \(PolyIneq\-Real vs\. PolyIneq\-Synth\)\.

We compare the performance of various LLM\-assisted methods on PolyIneq\-Real and PolyIneq\-Synth\. Fig\.[4](https://arxiv.org/html/2605.15445#S5.F4)shows a marked decrease in both pass rates and computational efficiency \(running time\) observed across all methods when tested on synthetic data, validating that the synthesized high\-dimensional instances represent more challenging reasoning scenarios\. Under the more rigorous PolyIneq\-Synth benchmark, NSPI achieves a25\.95%pass rate while maintaining the minimum average execution time, thereby underscoring its superior efficacy and robustness\. Notably, NSPI delivers a2\.87\-foldimprovement in pass rate over the hybrid LIPS system\. In terms of computational throughput, NSPI consistently outperforms its counterparts by maintaining the lowest latency across both benchmarks, yielding a remarkable speedup exceeding10xcompared to several state\-of\-the\-art LLM\-based provers\.

##### Effectiveness of the progressive training process\.

Fig\.[5](https://arxiv.org/html/2605.15445#S5.F5)illustrates the performance of the SOS Structure Conjecturer across successive training stages on PolyIneqBench\. As illustrated by the color transitions in the left panel of Fig\.[5](https://arxiv.org/html/2605.15445#S5.F5), progressive reinforcement learning \(RL\) facilitates the migration of the model’scapability boundariestoward higher\-dimensional polynomials\. Furthermore, the right panel of Fig\.[5](https://arxiv.org/html/2605.15445#S5.F5)highlights “jump\-like” performance improvements at the curriculum boundary points for different data groups\. Moreover, training on specific curriculum groups yields cross\-group generalization, partially enhancing performance on out\-of\-distribution instances\. Overall, large\-scale supervised fine\-tuning \(SFT\) in the cold\-start phase establishes a strong performance foundation \(middle panel\), upon which progressive RL provides additional gains by extending generalization to more challenging, higher\-dimensional instances\.

### 5\.4Ablation Studies

To validate the effectiveness of the individual components of NSPI, we conduct ablation studies on PolyIneqBench under three settings: \(1\) removing the synthetic SOS cold start and applying RL directly to the base model; \(2\) removing progressive RL; and \(3\) disabling curriculum\-based data partitioning during RL\. The results in[Table2](https://arxiv.org/html/2605.15445#S5.T2)show that the cold\-start stage trained on large\-scale synthetic data is crucial for SOS conjecturing performance, and that curriculum\-based GRPO further improves the overall results\.

Table 2:Ablation study of NSPI components\. PI\-Real and PI\-Synth denote PolyIneq\-Real and PolyIneq\-Synth, respectively\.

## 6Conclusion

In this paper, we presented NSPI, a neuro\-symbolic framework for automated polynomial\-inequality proving that combines the complementary strengths of large language models and symbolic computation to provide an end\-to\-end pipeline from conjecture to certified proof\. NSPI leverages an LLM to propose approximate Sum\-Of\-Squares \(SOS\) decompositions, and refines them via symbolic computation into exact SOS representations that directly prove the target inequalities; we then machine\-check these proofs in Lean\. Extensive experiments on challenging benchmarks with polynomials of up to 10 variables show that NSPI consistently improves the success rate and efficiency over competitive baseline methods, substantially broadening the practical scope of automated polynomial\-inequality proving\.

## Acknowledgements

This work was supported in part by the National Key Research and Development Program of China under Grant 2023YFA1009402, the Strategic Priority Research Program of Chinese Academy of Sciences under Grant XDA0480501, and the Natural Science Foundation of Hunan Province under Grant 2026JJ70102\.

## Impact Statement

This paper presents work whose goal is to the field of Machine Learning\. The development of our approach holds potential for significant impact within the domains of formal verification and automated polynomial inequality proving\. While there are various potential societal consequences of this work, none which we feel must be specifically highlighted here\.

## References

- Ahmadi & Majumdar \(2019\)Ahmadi, A\. A\. and Majumdar, A\.Dsos and sdsos optimization: more tractable alternatives to sum of squares and semidefinite optimization\.*SIAM Journal on Applied Algebra and Geometry*, 3\(2\):193–230, 2019\.
- Andreescu \(2019\)Andreescu, T\.*118 Inequalities for Mathematics Competitions*\.XYZ Press, Plano, TX, 2019\.
- Azerbayev et al\. \(2023\)Azerbayev, Z\., Piotrowski, B\., Schoelkopf, H\., Ayers, E\. W\., Radev, D\., and Avigad, J\.Proofnet: Autoformalizing and formally proving undergraduate\-level mathematics, 2023\.
- Barker & Carlson \(1975\)Barker, G\. and Carlson, D\.Cones of diagonally dominant matrices\.*Pacific Journal of Mathematics*, 57\(1\):15–32, 1975\.
- Chen \(2014\)Chen, E\.A brief introduction to olympiad inequalities\.*URL: https://web\.evanchen\.cc/handouts/Ineq/en\.pdf \(accessed 20\.03\.2021\)*, 2014\.
- Chen et al\. \(2025a\)Chen, J\., Chen, W\., Du, J\., Hu, J\., Jiang, Z\., Jie, A\., Jin, X\., Jin, X\., Li, C\., Shi, W\., Wang, Z\., Wang, M\., Wei, C\., Wei, S\., Xin, H\., Yang, F\., Gao, W\., Yuan, Z\., Zhan, T\., Zheng, Z\., Zhou, T\., and Zhu, T\. H\.Seed\-prover 1\.5: Mastering undergraduate\-level theorem proving via learning from experience, 2025a\.URL[https://arxiv\.org/abs/2512\.17260](https://arxiv.org/abs/2512.17260)\.
- Chen et al\. \(2025b\)Chen, L\., Gu, J\., Huang, L\., Huang, W\., Jiang, Z\., Jie, A\., Jin, X\., Jin, X\., Li, C\., Ma, K\., Ren, C\., Shen, J\., Shi, W\., Sun, T\., Sun, H\., Wang, J\., Wang, S\., Wang, Z\., Wei, C\., Wei, S\., Wu, Y\., Wu, Y\., Xia, Y\., Xin, H\., Yang, F\., Ying, H\., Yuan, H\., Yuan, Z\., Zhan, T\., Zhang, C\., Zhang, Y\., Zhang, G\., Zhao, T\., Zhao, J\., Zhou, Y\., and Zhu, T\. H\.Seed\-prover: Deep and broad reasoning for automated theorem proving, 2025b\.URL[https://arxiv\.org/abs/2507\.23726](https://arxiv.org/abs/2507.23726)\.
- Chervonyi et al\. \(2025\)Chervonyi, Y\., Trinh, T\. H\., Olšák, M\., Yang, X\., Nguyen, H\. H\., Menegali, M\., Jung, J\., Kim, J\., Verma, V\., Le, Q\. V\., et al\.Gold\-medalist performance in solving olympiad geometry with alphageometry2\.*Journal of Machine Learning Research*, 26\(241\):1–39, 2025\.
- De Moura & Bjørner \(2008\)De Moura, L\. and Bjørner, N\.Z3: An efficient smt solver\.In*International conference on Tools and Algorithms for the Construction and Analysis of Systems*, pp\. 337–340\. Springer, 2008\.
- De Moura et al\. \(2015\)De Moura, L\., Kong, S\., Avigad, J\., Van Doorn, F\., and von Raumer, J\.The lean theorem prover \(system description\)\.In*International Conference on Automated Deduction*, pp\. 378–388\. Springer, 2015\.
- DeepSeek\-AI \(2025\)DeepSeek\-AI\.Deepseek\-v3\.2: Pushing the frontier of open large language models, 2025\.
- El Din \(2008\)El Din, M\. S\.Computing the global optimum of a multivariate polynomial over the reals\.In*Proceedings of the twenty\-first international symposium on Symbolic and algebraic computation*, pp\. 71–78, 2008\.
- Gerschgorin \(1931\)Gerschgorin, S\.Uber die abgrenzung der eigenwerte einer matrix\.*Izvestija Akademii Nauk SSSR, Serija Matematika*, 7\(3\):749–754, 1931\.
- Golub & Van Loan \(2013\)Golub, G\. H\. and Van Loan, C\. F\.*Matrix computations*\.JHU press, 2013\.
- He et al\. \(2024\)He, C\., Luo, R\., Bai, Y\., Hu, S\., Thai, Z\., Shen, J\., Hu, J\., Han, X\., Huang, Y\., Zhang, Y\., Liu, J\., Qi, L\., Liu, Z\., and Sun, M\.OlympiadBench: A challenging benchmark for promoting AGI with olympiad\-level bilingual multimodal scientific problems\.In Ku, L\.\-W\., Martins, A\., and Srikumar, V\. \(eds\.\),*Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\)*, pp\. 3828–3850, Bangkok, Thailand, August 2024\. Association for Computational Linguistics\.doi:10\.18653/v1/2024\.acl\-long\.211\.URL[https://aclanthology\.org/2024\.acl\-long\.211/](https://aclanthology.org/2024.acl-long.211/)\.
- Heck & Koepf \(1993\)Heck, A\. and Koepf, W\.*Introduction to MAPLE*, volume 1993\.Springer, 1993\.
- Heule et al\. \(2016\)Heule, M\. J\. H\., Kullmann, O\., and Marek, V\. W\.Solving and verifying the boolean pythagorean triples problem via cube\-and\-conquer\.In Creignou, N\. and Le Berre, D\. \(eds\.\),*Theory and Applications of Satisfiability Testing – SAT 2016*, pp\. 228–245, Cham, 2016\. Springer International Publishing\.ISBN 978\-3\-319\-40970\-2\.
- Kaltofen et al\. \(2012\)Kaltofen, E\. L\., Li, B\., Yang, Z\., and Zhi, L\.Exact certification in global polynomial optimization via sums\-of\-squares of rational functions with rational coefficients\.*Journal of Symbolic Computation*, 47\(1\):1–15, 2012\.ISSN 0747\-7171\.doi:https://doi\.org/10\.1016/j\.jsc\.2011\.08\.002\.URL[https://www\.sciencedirect\.com/science/article/pii/S0747717111001143](https://www.sciencedirect.com/science/article/pii/S0747717111001143)\.
- Lagarias \(1985\)Lagarias, J\. C\.The computational complexity of simultaneous diophantine approximation problems\.*SIAM Journal on Computing*, 14\(1\):196–209, 1985\.
- Lample et al\. \(2022\)Lample, G\., Lacroix, T\., Lachaux, M\.\-A\., Rodriguez, A\., Hayat, A\., Lavril, T\., Ebner, G\., and Martinet, X\.Hypertree proof search for neural theorem proving\.*Advances in neural information processing systems*, 35:26337–26349, 2022\.
- Langley \(2000\)Langley, P\.Crafting papers on machine learning\.In Langley, P\. \(ed\.\),*Proceedings of the 17th International Conference on Machine Learning \(ICML 2000\)*, pp\. 1207–1216, Stanford, CA, 2000\. Morgan Kaufmann\.
- Lasserre \(2002\)Lasserre, J\. B\.Semidefinite programming vs\. lp relaxations for polynomial programming\.*Mathematics of operations research*, 27\(2\):347–360, 2002\.
- Le & Van Barel \(2014\)Le, H\. and Van Barel, M\.An algorithm for decomposing a non\-negative polynomial as a sum of squares of rational functions\.*Numerical Algorithms*, 69, 06 2014\.doi:10\.1007/s11075\-014\-9903\-3\.
- Lee \(2005\)Lee, H\.Topics in inequalities\.*Halen gelismekte olan kitabı bulmak için internetten arayınız*, 2005\.
- Li et al\. \(2025a\)Li, Z\., Li, Z\., Tang, W\., Zhang, X\., Yao, Y\., Si, X\., Yang, F\., Yang, K\., and Ma, X\.Proving olympiad inequalities by synergizing LLMs and symbolic reasoning\.In*International Conference on Learning Representations \(ICLR\)*, 2025a\.
- Li et al\. \(2025b\)Li, Z\., Liao, B\., and Ye, Q\.Ineqsearch: Hybrid reasoning for olympiad inequality proofs\.In*The Thirty\-ninth Annual Conference on Neural Information Processing Systems*, 2025b\.
- Li et al\. \(2025c\)Li, Z\., Liao, B\., and Ye, Q\.Ineqsearch: Hybrid reasoning for olympiad inequality proofs\.In*The Thirty\-ninth Annual Conference on Neural Information Processing Systems*, 2025c\.
- Lin et al\. \(2025a\)Lin, Y\., Tang, S\., Lyu, B\., Wu, J\., Lin, H\., Yang, K\., Li, J\., Xia, M\., Chen, D\., Arora, S\., et al\.Goedel\-prover: A frontier model for open\-source automated theorem proving\.*arXiv preprint arXiv:2502\.07640*, 2025a\.
- Lin et al\. \(2025b\)Lin, Y\., Tang, S\., Lyu, B\., Yang, Z\., Chung, J\.\-H\., Zhao, H\., Jiang, L\., Geng, Y\., Ge, J\., Sun, J\., et al\.Goedel\-prover\-v2: Scaling formal theorem proving with scaffolded data synthesis and self\-correction\.*arXiv preprint arXiv:2508\.03613*, 2025b\.
- Magron et al\. \(2023\)Magron, V\., Din, M\. S\. E\., and Vu, T\.\-H\.Sum of squares decompositions of polynomials over their gradient ideals with rational coefficients\.*SIAM Journal on Optimization*, 33\(1\):63–88, 2023\.
- Manfrino et al\. \(2010\)Manfrino, R\. B\., Ortega, J\. A\. G\., and Delgado, R\. V\.*Inequalities: a mathematical olympiad approach*\.Springer Science & Business Media, 2010\.
- Maréchal et al\. \(2015\)Maréchal, A\., Fouilhé, A\., King, T\., Monniaux, D\., and Périn, M\.Polyhedral approximation of multivariate polynomials using handelman’s theorem\.In*International Conference on Verification, Model Checking, and Abstract Interpretation*, pp\. 166–184\. Springer, 2015\.
- Martin\-Dorel & Roux \(2017\)Martin\-Dorel, É\. and Roux, P\.A reflexive tactic for polynomial positivity using numerical solvers and floating\-point computations\.In*Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs*, pp\. 90–99, 2017\.
- Meurer et al\. \(2017\)Meurer, A\., Smith, C\. P\., Paprocki, M\., Čertík, O\., Kirpichev, S\. B\., Rocklin, M\., Kumar, A\., Ivanov, S\., Moore, J\. K\., Singh, S\., et al\.Sympy: symbolic computing in python\.*PeerJ Computer Science*, 3:e103, 2017\.
- Mildorf \(2005\)Mildorf, T\. J\.Olympiad inequalities\.*Preprint, https://artofproblemsolving\. com/articles/files/MildorfInequalities\. pdf*, 2005\.
- Parrilo \(2000a\)Parrilo, P\.Structured semidenite programs and semialgebraic geometry methods in robustness and optimization\.*PhD thesis*, 08 2000a\.
- Parrilo \(2000b\)Parrilo, P\. A\.*Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization*\.California Institute of Technology, 2000b\.
- Parrilo \(2003\)Parrilo, P\. A\.Semidefinite programming relaxations for semialgebraic problems\.*Mathematical programming*, 96\(2\):293–320, 2003\.
- Parvardi \(2011\)Parvardi, A\. H\.Problems proposed by vasc and arqady, 2011\.
- Paulson \(1990\)Paulson, L\. C\.Isabelle: The next 700 theorem provers\.In*Logic and computer science*, volume 31, pp\. 361–386, 1990\.
- Peyrl & Parrilo \(2008a\)Peyrl, H\. and Parrilo, P\. A\.Computing sum of squares decompositions with rational coefficients\.*Theoretical Computer Science*, 409\(2\):269–281, 2008a\.ISSN 0304\-3975\.doi:https://doi\.org/10\.1016/j\.tcs\.2008\.09\.025\.URL[https://www\.sciencedirect\.com/science/article/pii/S0304397508006452](https://www.sciencedirect.com/science/article/pii/S0304397508006452)\.Symbolic\-Numerical Computations\.
- Peyrl & Parrilo \(2008b\)Peyrl, H\. and Parrilo, P\. A\.Computing sum of squares decompositions with rational coefficients\.*Theor\. Comput\. Sci\.*, 409:269–281, 2008b\.URL[https://api\.semanticscholar\.org/CorpusID:2370460](https://api.semanticscholar.org/CorpusID:2370460)\.
- Polu & Sutskever \(2020\)Polu, S\. and Sutskever, I\.Generative language modeling for automated theorem proving\.*arXiv preprint arXiv:2009\.03393*, 2020\.
- Ren et al\. \(2025\)Ren, Z\., Shao, Z\., Song, J\., Xin, H\., Wang, H\., Zhao, W\., Zhang, L\., Fu, Z\., Zhu, Q\., Yang, D\., et al\.Deepseek\-prover\-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.*arXiv preprint arXiv:2504\.21801*, 2025\.
- Riasat \(2008\)Riasat, S\.Basics of olympiad inequalities\.*Preprint*, 20:80–90, 2008\.
- Shao et al\. \(2024\)Shao, Z\., Wang, P\., Zhu, Q\., Xu, R\., Song, J\., Bi, X\., Zhang, H\., Zhang, M\., Li, Y\., Wu, Y\., et al\.Deepseekmath: Pushing the limits of mathematical reasoning in open language models\.*arXiv preprint arXiv:2402\.03300*, 2024\.
- Team \(2025\)Team, Q\.Qwen3 technical report, 2025\.URL[https://arxiv\.org/abs/2505\.09388](https://arxiv.org/abs/2505.09388)\.
- Trinh et al\. \(2024\)Trinh, T\. H\., Wu, Y\., Le, Q\. V\., He, H\., and Luong, T\.Solving olympiad geometry without human demonstrations\.*Nature*, 625\(7995\):476–482, 2024\.
- Tsoukalas et al\. \(2024\)Tsoukalas, G\., Lee, J\., Jennings, J\., Xin, J\., Ding, M\., Jennings, M\., Thakur, A\., and Chaudhuri, S\.Putnambench: evaluating neural theorem\-provers on the putnam mathematical competition\.In*Proceedings of the 38th International Conference on Neural Information Processing Systems*, NIPS ’24, Red Hook, NY, USA, 2024\. Curran Associates Inc\.ISBN 9798331314385\.
- Tung \(2012\)Tung, N\. D\.567 nice and hard inequality\.[https://phamtuankhai\.wordpress\.com/wp\-content/uploads/2012/04/567\-bat\-dang\-thuc\-hay\.pdf](https://phamtuankhai.wordpress.com/wp-content/uploads/2012/04/567-bat-dang-thuc-hay.pdf), 2012\.
- Tung & Zhe \(2014\)Tung, N\. D\. and Zhe, Z\. Y\.The interesting around technical analysis: Three variable inequalities, 2014\.
- Uray \(2020\)Uray, M\.On proving inequalities by cylindrical algebraic decomposition\.*Annales Universitatis Scientiarum Budapestinensis de Rolando Eötvös Nominatae\. Sectio computatorica*, pp\. 231–252, 01 2020\.doi:10\.71352/ac\.51\.231\.
- Wang et al\. \(2025\)Wang, H\., Unsal, M\., Lin, X\., Baksys, M\., Liu, J\., Santos, M\. D\., Sung, F\., Vinyes, M\., Ying, Z\., Zhu, Z\., et al\.Kimina\-prover preview: Towards large formal reasoning models with reinforcement learning\.*arXiv preprint arXiv:2504\.11354*, 2025\.
- Wei et al\. \(2024\)Wei, C\., Sun, M\., and Wang, W\.Proving olympiad algebraic inequalities without human demonstrations\.*Advances in Neural Information Processing Systems*, 37:82811–82822, 2024\.
- Xin et al\. \(2025\)Xin, R\., Xi, C\., Yang, J\., Chen, F\., Wu, H\., Xiao, X\., Sun, Y\., Zheng, S\., and Ding, M\.Bfs\-prover: Scalable best\-first tree search for llm\-based automatic theorem proving\.In*Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\)*, pp\. 32588–32599, 2025\.
- Yang \(1999\)Yang, L\.Recent advances in automated theorem proving on inequalities\.*J\. Comput\. Sci\. Technol\.*, 14\(5\):434–446, September 1999\.ISSN 1000\-9000\.doi:10\.1007/BF02948785\.URL[https://doi\.org/10\.1007/BF02948785](https://doi.org/10.1007/BF02948785)\.
- Yang et al\. \(2023\)Yang, Z\., Zhao, H\., and Zhi, L\.Verifyrealroots: A matlab package for computing verified real solutions of polynomials systems of equations and inequalities\.*Journal of Systems Science and Complexity*, 02 2023\.doi:10\.1007/s11424\-023\-1406\-7\.
- Zheng et al\. \(2021\)Zheng, K\., Han, J\. M\., and Polu, S\.Minif2f: a cross\-system benchmark for formal olympiad\-level mathematics\.*arXiv preprint arXiv:2109\.00110*, 2021\.

## Appendix ASum of Squares and Semidefinite Programming

We introduce the relationship between sum\-of\-squares \(SOS\) polynomials and semidefinite programming \(SDP\), which provides the theoretical foundation for the methods employed in this study\.

A polynomialf​\(𝐱\)∈ℝ​\[𝐱\]f\(\\mathbf\{x\}\)\\in\\mathbb\{R\}\[\\mathbf\{x\}\]is called a sum\-of\-squares \(SOS\) polynomial if it can be expressed as

f​\(𝐱\)=∑ifi​\(𝐱\)2,where​fi​\(𝐱\)∈ℝ​\[𝐱\]\.\\displaystyle f\(\\mathbf\{x\}\)=\\sum\_\{i\}f\_\{i\}\(\\mathbf\{x\}\)^\{2\},\\quad\\text\{where \}f\_\{i\}\(\\mathbf\{x\}\)\\in\\mathbb\{R\}\[\\mathbf\{x\}\]\.\(13\)
###### Example 1\.

Consider the polynomialf​\(𝐱\)=2​x14\+2​x13​x2−x12​x22\+5​x24,𝐱=\(x1,x2\)∈ℝ2f\(\\mathbf\{x\}\)=2x\_\{1\}^\{4\}\+2x\_\{1\}^\{3\}x\_\{2\}\-x\_\{1\}^\{2\}x\_\{2\}^\{2\}\+5x\_\{2\}^\{4\},\\quad\\mathbf\{x\}=\(x\_\{1\},x\_\{2\}\)\\in\\mathbb\{R\}^\{2\}\. Definef1​\(𝐱\)=12​\(2​x12−3​x22\+x1​x2\),f2​\(𝐱\)=12​\(x22\+3​x1​x2\)f\_\{1\}\(\\mathbf\{x\}\)=\\frac\{1\}\{\\sqrt\{2\}\}\\left\(2x\_\{1\}^\{2\}\-3x\_\{2\}^\{2\}\+x\_\{1\}x\_\{2\}\\right\),f\_\{2\}\(\\mathbf\{x\}\)=\\frac\{1\}\{\\sqrt\{2\}\}\\left\(x\_\{2\}^\{2\}\+3x\_\{1\}x\_\{2\}\\right\)\. Thenf​\(𝐱\)f\(\\mathbf\{x\}\)admits the SOS decompositionf​\(𝐱\)=f1​\(𝐱\)2\+f2​\(𝐱\)2f\(\\mathbf\{x\}\)=f\_\{1\}\(\\mathbf\{x\}\)^\{2\}\+f\_\{2\}\(\\mathbf\{x\}\)^\{2\}, which implies thatf​\(𝐱\)≥0f\(\\mathbf\{x\}\)\\geq 0for all𝐱∈ℝ2\\mathbf\{x\}\\in\\mathbb\{R\}^\{2\}\.

Semidefinite programming \(SDP\) is a class of convex optimization problems, whose standard form can be expressed as

minimize⟨C,G⟩subject to⟨Ai,G⟩=bi,i=1,…,m,G⪰0,\\displaystyle\\begin\{aligned\} \\text\{minimize\}\\quad&\\langle C,G\\rangle\\\\ \\text\{subject to\}\\quad&\\langle A\_\{i\},G\\rangle=b\_\{i\},\\quad i=1,\\dots,m,\\\\ &G\\succeq 0,\\end\{aligned\}\(14\)whereGGis a symmetric matrix variable andG⪰0G\\succeq 0denotes thatGGis positive semidefinite\.⟨A,G⟩=tr​\(A⊤​G\)\\langle A,G\\rangle=\\mathrm\{tr\}\(A^\{\\top\}G\)denotes the matrix inner product\.

###### Theorem A\.1\.

\(Parrilo,[2000b](https://arxiv.org/html/2605.15445#bib.bib37)\)A multivariate polynomialf​\(x\)f\(x\)innnvariables and of degree2​d2dis a sum of squares \(SOS\) if and only if there exists a symmetric positive semidefinite \(PSD\) matrixG~\\widetilde\{G\}such that

f​\(x\)=𝐯​\(x\)⊤​G~​𝐯​\(x\),f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}\\widetilde\{G\}\{\\mathbf\{v\}\}\(x\),\(15\)where𝐯​\(x\)=\[1,x1,x2,…,xn,x12,x1​x2,…,xnd\]\{\\mathbf\{v\}\}\(x\)=\[1,x\_\{1\},x\_\{2\},\.\.\.,x\_\{n\},x\_\{1\}^\{2\},x\_\{1\}x\_\{2\},\.\.\.,x\_\{n\}^\{d\}\]is the vector of monomials up to degreedd\.

The matrixG~\\widetilde\{G\}is referred to as aGram matrixoff​\(x\)f\(x\)with respect to the monomial basis𝐯​\(x\)\{\\mathbf\{v\}\}\(x\)\.

According to[TheoremA\.1](https://arxiv.org/html/2605.15445#A1.Thmtheorem1), expanding the right\-hand side of equation[Equation15](https://arxiv.org/html/2605.15445#A1.E15)and matching the coefficients with those off​\(x\)f\(x\)yields a system of linear equality constraints on the entries of the Gram matrixGG\. Consequently, the problem of finding an SOS decomposition of the polynomial can be equivalently reformulated as the SDP problem given in[Equation4](https://arxiv.org/html/2605.15445#S3.E4)of[Section3](https://arxiv.org/html/2605.15445#S3)\.

###### Example 2\.

\(Parrilo,[2003](https://arxiv.org/html/2605.15445#bib.bib38)\)Consider the bivariate quartic polynomialf​\(𝐱\)=2​x14\+2​x13​x2−x12​x22\+5​x24,𝐱=\(x1,x2\)∈ℝ2f\(\\mathbf\{x\}\)=2x\_\{1\}^\{4\}\+2x\_\{1\}^\{3\}x\_\{2\}\-x\_\{1\}^\{2\}x\_\{2\}^\{2\}\+5x\_\{2\}^\{4\},\\quad\\mathbf\{x\}=\(x\_\{1\},x\_\{2\}\)\\in\\mathbb\{R\}^\{2\}\. Let the monomial basis vector be𝐯​\(𝐱\)=\[x12,x22,x1​x2\]⊤\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)=\[x\_\{1\}^\{2\},\\ x\_\{2\}^\{2\},\\ x\_\{1\}x\_\{2\}\]^\{\\top\}\. Thenf​\(𝐱\)f\(\\mathbf\{x\}\)can be written in Gram form as

f​\(𝐱\)\\displaystyle f\(\\mathbf\{x\}\)=𝐯​\(𝐱\)⊤​G​𝐯​\(𝐱\)\\displaystyle=\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)^\{\\top\}G\\,\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)=\[x12x22x1​x2\]⊤​\[q11q12q13q12q22q23q13q23q33\]​\[x12x22x1​x2\]\\displaystyle=\\begin\{bmatrix\}x\_\{1\}^\{2\}\\\\ x\_\{2\}^\{2\}\\\\ x\_\{1\}x\_\{2\}\\end\{bmatrix\}^\{\\\!\\top\}\\begin\{bmatrix\}q\_\{11\}&q\_\{12\}&q\_\{13\}\\\\ q\_\{12\}&q\_\{22\}&q\_\{23\}\\\\ q\_\{13\}&q\_\{23\}&q\_\{33\}\\end\{bmatrix\}\\begin\{bmatrix\}x\_\{1\}^\{2\}\\\\ x\_\{2\}^\{2\}\\\\ x\_\{1\}x\_\{2\}\\end\{bmatrix\}=q11​x14\+q22​x24\+\(q33\+2​q12\)​x12​x22\+2​q13​x13​x2\+2​q23​x1​x23\.\\displaystyle=q\_\{11\}x\_\{1\}^\{4\}\+q\_\{22\}x\_\{2\}^\{4\}\+\(q\_\{33\}\+2q\_\{12\}\)x\_\{1\}^\{2\}x\_\{2\}^\{2\}\+2q\_\{13\}x\_\{1\}^\{3\}x\_\{2\}\+2q\_\{23\}x\_\{1\}x\_\{2\}^\{3\}\.\(16\)Matching coefficients with the target polynomialf​\(𝐱\)f\(\\mathbf\{x\}\)yields the following linear equalities:

q11=2,q22=5,q33\+2​q12=−1,2​q13=2,2​q23=0\.q\_\{11\}=2,\\qquad q\_\{22\}=5,\\qquad q\_\{33\}\+2q\_\{12\}=\-1,\\qquad 2q\_\{13\}=2,\\qquad 2q\_\{23\}=0\.\(17\)A positive semidefinite matrixG⪰0G\\succeq 0satisfying \([17](https://arxiv.org/html/2605.15445#A1.E17)\) can be obtained, e\.g\., via semidefinite programming\. One feasible choice is

G=\[2−31−350105\]=L⊤​L,L=12​\[2−31013\]\.G=\\begin\{bmatrix\}2&\-3&1\\\\ \-3&5&0\\\\ 1&0&5\\end\{bmatrix\}=L^\{\\top\}L,\\qquad L=\\frac\{1\}\{\\sqrt\{2\}\}\\begin\{bmatrix\}2&\-3&1\\\\ 0&1&3\\end\{bmatrix\}\.Consequently,f​\(𝐱\)f\(\\mathbf\{x\}\)admits the explicit SOS decompositionf​\(𝐱\)=12​\(2​x12−3​x22\+x1​x2\)2\+12​\(x22\+3​x1​x2\)2f\(\\mathbf\{x\}\)=\\frac\{1\}\{2\}\\left\(2x\_\{1\}^\{2\}\-3x\_\{2\}^\{2\}\+x\_\{1\}x\_\{2\}\\right\)^\{2\}\+\\frac\{1\}\{2\}\\left\(x\_\{2\}^\{2\}\+3x\_\{1\}x\_\{2\}\\right\)^\{2\}\.

## Appendix BTheoretical Foundations of SOS Data Construction

This part provides the formal theoretical guarantees for the data construction methods described in Section[4\.1\.1](https://arxiv.org/html/2605.15445#S4.SS1.SSS1)\. We focus on the spectral properties and decomposition theorems that ensure the generated Gram matricesG~\\widetilde\{G\}are positive semidefinite\.

![Refer to caption](https://arxiv.org/html/2605.15445v1/x6.png)Figure 6:Framework of SOS data construction methods in[Section4\.1\.1](https://arxiv.org/html/2605.15445#S4.SS1.SSS1)\. The generation of polynomial\-SOS pairs is based on the quadratic formf​\(x\)=𝐯​\(x\)𝖳​G~​𝐯​\(x\)f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\mathsf\{T\}\}\\widetilde\{G\}\{\\mathbf\{v\}\}\(x\), where the Gram matrixG~\\widetilde\{G\}is synthesized through either computation\-driven or structure\-driven approaches\.### B\.1Spectral Foundations for Computation\-Driven Methods

The computation\-driven methods rely on the relationship between eigenvalues and the PSD property\.

###### Lemma B\.1\(Eigenvalue Shift\)\.

LetG∈𝕊mG\\in\\mathbb\{S\}^\{m\}be a symmetric matrix with real entries\. For anyk∈ℝk\\in\\mathbb\{R\}, the eigenvalues ofG~=G−k​I\\widetilde\{G\}=G\-kIare given byλi​\(G~\)=λi​\(G\)−k\\lambda\_\{i\}\(\\widetilde\{G\}\)=\\lambda\_\{i\}\(G\)\-k\. Consequently, selectingk≤λmin​\(G\)k\\leq\\lambda\_\{\\min\}\(G\)is a sufficient condition to ensureG~⪰0\\widetilde\{G\}\\succeq 0\.

To generate Gram matrices with controlled sparsity and coefficient types, we employ a constructive approach based on quadratic forms\.

###### Lemma B\.2\.

LetL∈ℤk×mL\\in\\mathbb\{Z\}^\{k\\times m\}be an arbitrary matrix \(representing the coefficients ofkkbasis polynomials\) andD=diag​\(d1,…,dk\)D=\\text\{diag\}\(d\_\{1\},\\dots,d\_\{k\}\)be a diagonal matrix withdi\>0d\_\{i\}\>0\. The resulting matrix

G~=L⊤​D​L\\widetilde\{G\}=L^\{\\top\}DL\(18\)is guaranteed to be positive semi\-definite \(G~⪰0\\widetilde\{G\}\\succeq 0\)\.

### B\.2Diagonally Dominant \(dd\) and Scaled Diagonally Dominant \(sdd\) Cones

Structure\-driven methods restrict the search space to specific sub\-cones of the PSD cone to simplify formal verification\.

###### Definition B\.3\.

\(Ahmadi & Majumdar,[2019](https://arxiv.org/html/2605.15445#bib.bib1)\)A matrixG∈ℝm×mG\\in\\mathbb\{R\}^\{m\\times m\}is defined as diagonally dominant \(dd\) if it satisfies the following condition:

Gi​i≥∑j≠i\|Gi​j\|,∀i\.\\displaystyle G\_\{ii\}\\geq\\sum\_\{j\\neq i\}\|G\_\{ij\}\|,\\quad\\forall i\.\(19\)A symmetric matrixGGis called scaled diagonally dominant \(sdd\) if there exists a diagonal matrixDDwith strictly positive diagonal elements such that the matrixD​G​DDGDis diagonally dominant\.

According to Gershgorin’s circle theorem\(Gerschgorin,[1931](https://arxiv.org/html/2605.15445#bib.bib13)\), any symmetric diagonally dominant matrix with non\-negative diagonal entries is positive semi\-definite\.

The following lemma provides the theoretical justification for the extreme ray decomposition used in our framework:

###### Lemma B\.4\.

\(Barker & Carlson,[1975](https://arxiv.org/html/2605.15445#bib.bib4)\)The cone ofm×mm\\times msymmetric dd matrices is the set of all matrices that can be represented as:

G~=∑i=1m2ηi​Ui,ηi≥0\\widetilde\{G\}=\\sum\_\{i=1\}^\{m^\{2\}\}\\eta\_\{i\}U\_\{i\},\\quad\\eta\_\{i\}\\geq 0\(20\)where eachUi=𝐮i​𝐮i⊤U\_\{i\}=\\mathbf\{u\}\_\{i\}\\mathbf\{u\}\_\{i\}^\{\\top\}is a rank\-one matrix and𝐮i∈ℝm\\mathbf\{u\}\_\{i\}\\in\\mathbb\{R\}^\{m\}is a vector with at most two non\-zero components, each belonging to\{±1\}\\\{\\pm 1\\\}, that is,𝐮i∈\{±ek:k∈\[m\]\}∪\{±ek±eℓ:1≤k<ℓ≤m\}\\mathbf\{u\}\_\{i\}\\in\\\{\\pm e\_\{k\}:k\\in\[m\]\\\}\\,\\cup\\,\\\{\\pm e\_\{k\}\\pm e\_\{\\ell\}:1\\leq k<\\ell\\leq m\\\}\.

For the construction of scaled diagonally dominant \(sdd\) matrices, we utilize the properties of diagonal congruence transformation:

###### Lemma B\.5\.

A matrixGGis sdd if there exists a positive definite diagonal matrixD≻0D\\succ 0such thatD​G​DDGDis dd\. By Sylvester’s Law of Inertia, diagonal congruence transformations preserve the inertia of a matrix and, in particular, the signs of its eigenvalues\. SinceD​G​DDGDis dd, it follows thatD​G​D⪰0DGD\\succeq 0\. Consequently,G=D−1​\(D​G​D\)​D−1⪰0G=D^\{\-1\}\(DGD\)D^\{\-1\}\\succeq 0\.

SinceGGis dd, it admits the decomposition∑i=1m2ηi​Ui\\sum\_\{i=1\}^\{m^\{2\}\}\\eta\_\{i\}U\_\{i\}\. Applying the diagonal congruence transformationG~=D−1​G​D−1\\widetilde\{G\}=D^\{\-1\}GD^\{\-1\}yields the sdd matrixG~\\widetilde\{G\}as a non\-negative linear combination of scaled rank\-one matrices:

G~=∑i=1m2ηi​U^i,\\displaystyle\\widetilde\{G\}=\\sum\_\{i=1\}^\{m^\{2\}\}\\eta\_\{i\}\\widehat\{U\}\_\{i\},\(21\)whereU^i:=D−1​Ui​D−1=𝐰i​𝐰i⊤\\widehat\{U\}\_\{i\}:=D^\{\-1\}U\_\{i\}D^\{\-1\}=\\mathbf\{w\}\_\{i\}\\mathbf\{w\}\_\{i\}^\{\\top\}and𝐰i:=D−1​𝐮i\\mathbf\{w\}\_\{i\}:=D^\{\-1\}\\mathbf\{u\}\_\{i\}\. Each vector𝐰i\\mathbf\{w\}\_\{i\}still has at most two nonzero components, whose magnitudes are determined by the diagonal entries ofD−1D^\{\-1\}\.

## Appendix CFurther Details of Symbolic Correction Module

This section presents the theoretical foundations of the symbolic correction module described in Section[4\.2](https://arxiv.org/html/2605.15445#S4.SS2)\. The purpose of this module is to convert the SOS structural conjecture obtained from the SOS conjecture stage into an exact rational sum\-of\-squares certificate, ensuring suitability for formal verification\.

### C\.1Gauss\-Newton Refinement for SOS

Suppose a polynomialf​\(x\)∈ℝ​\[x\]f\(x\)\\in\\mathbb\{R\}\[x\]of degree2​d2dis conjectured to admit a sum\-of\-squares \(SOS\) decomposition\. Let𝐯​\(x\)\{\\mathbf\{v\}\}\(x\)denote the monomial basis consisting of all monomials of degree at mostdd\. The SOS condition is equivalently expressed in Gram matrix form asf​\(x\)=𝐯​\(x\)⊤​G​𝐯​\(x\)f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}G\{\\mathbf\{v\}\}\(x\), whereG⪰0G\\succeq 0is a symmetric positive semidefinite Gram matrix\. In practice, numerical solvers only provide an approximate Gram matrixGG, such thatf​\(x\)≈𝐯​\(x\)⊤​G​𝐯​\(x\)f\(x\)\\approx\{\\mathbf\{v\}\}\(x\)^\{\\top\}G\{\\mathbf\{v\}\}\(x\)\.

To reduce numerical errors and improve stability prior to exact rational recovery, we apply a structure\-preserving Gauss–Newton refinement\.

#### C\.1\.1Numerical Newton Refinement of an Approximate Gram Matrix

##### Factorization\-based parameterization\.

AssumeG⪰0G\\succeq 0numerically and compute a factorization

G≈L​L⊤,G\\approx LL^\{\\top\},\(22\)whereL∈ℝm×kL\\in\\mathbb\{R\}^\{m\\times k\}andk=rank​\(G\)k=\\mathrm\{rank\}\(G\)\. Then

𝐯​\(𝐱\)⊤​G​𝐯​\(𝐱\)≈∑i=1kℓi​\(𝐱\)2,ℓi​\(𝐱\):=∑αci,α​𝐱α\.\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)^\{\\top\}G\\,\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)\\approx\\sum\_\{i=1\}^\{k\}\\ell\_\{i\}\(\\mathbf\{x\}\)^\{2\},\\quad\\ell\_\{i\}\(\\mathbf\{x\}\):=\\sum\_\{\\alpha\}c\_\{i,\\alpha\}\\mathbf\{x\}^\{\\alpha\}\.\(23\)
We refine the coefficient vectorsL:,iL\_\{:,i\}via a Gauss–Newton update so that the induced polynomial∑iℓi​\(𝐱\)2\\sum\_\{i\}\\ell\_\{i\}\(\\mathbf\{x\}\)^\{2\}matchesf​\(𝐱\)f\(\\mathbf\{x\}\)as accurately as possible\.

###### Proposition C\.1\.

By applying a Cholesky factorizationG=L​L⊤G=LL^\{\\top\}or anL​D​L⊤LDL^\{\\top\}decomposition to the Gram matrixGG, and treating the coefficients of the SOS factors as optimization variables, the Gauss–Newton iteration exhibits rapid convergence when applied to SOS problems\. Provided that sufficient numerical precision is employed, the backward errorθ\\thetacan be reduced to arbitrarily small values\.

This yields a high\-accuracy numerical approximation, which serves as a reliable foundation for the subsequent rational recovery procedure\.

##### Residual and stopping criterion\.

Letcoeff​\(⋅\)\\mathrm\{coeff\}\(\\cdot\)denote the coefficient vector of a polynomial in the chosen monomial basis\. Define the residual

r​\(L\):=coeff​\(∑i=1kℓi​\(𝐱\)2−f​\(𝐱\)\),θ:=‖r​\(L\)‖2\.r\(L\):=\\mathrm\{coeff\}\\\!\\left\(\\sum\_\{i=1\}^\{k\}\\ell\_\{i\}\(\\mathbf\{x\}\)^\{2\}\-f\(\\mathbf\{x\}\)\\right\),\\qquad\\theta:=\\\|r\(L\)\\\|\_\{2\}\.\(24\)
Here,θ\\thetadenotes the backward error of the numerical Gram matrixGG\. We apply the Gauss–Newton iteration to compute the coefficient correction termsΔ​ci,α\\Delta c\_\{i,\\alpha\}so as to minimizeθ\\theta, as described in[Equation11](https://arxiv.org/html/2605.15445#S4.E11)of[Section4\.2](https://arxiv.org/html/2605.15445#S4.SS2)\.

Simultaneously, the Gram matrix is updated according toG←G\+Δ​GG\\leftarrow G\+\\Delta G, where the correction termΔ​G\\Delta Gcan be expressed as

∑i=1k\(∑αΔ​ci,α​xα\)2=𝐯​\(x\)⊤​Δ​G​𝐯​\(x\)\.\\sum\_\{i=1\}^\{k\}\\left\(\\sum\_\{\\alpha\}\\Delta c\_\{i,\\alpha\}x^\{\\alpha\}\\right\)^\{2\}=\{\\mathbf\{v\}\}\(x\)^\{\\top\}\\Delta G\\,\{\\mathbf\{v\}\}\(x\)\.
The iteration terminates onceθ<τ\\theta<\\taufor a prescribed toleranceτ\>0\\tau\>0\.

### C\.2Detailed Formulation of Exact Rational Recovery

The following proposition establishes the fundamental equivalence between the existence of a rational sum\-of\-squares \(SOS\) decomposition and the existence of a Gram matrix with rational entries\.

###### Proposition C\.2\.

\(Peyrl & Parrilo,[2008a](https://arxiv.org/html/2605.15445#bib.bib41)\)Letf​\(𝐱\)∈ℚ​\[𝐱\]f\(\\mathbf\{x\}\)\\in\\mathbb\{Q\}\[\\mathbf\{x\}\]be a polynomial, and let𝐯​\(𝐱\)\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)denote a fixed vector of monomials\. Then the following statements are equivalent:

1. 1\.The polynomialf​\(𝐱\)f\(\\mathbf\{x\}\)admits a rational SOS decomposition, that is, there exist polynomialsfi​\(𝐱\)∈ℚ​\[𝐱\]f\_\{i\}\(\\mathbf\{x\}\)\\in\\mathbb\{Q\}\[\\mathbf\{x\}\]such that f​\(𝐱\)=∑i=1rfi​\(𝐱\)2\.f\(\\mathbf\{x\}\)=\\sum\_\{i=1\}^\{r\}f\_\{i\}\(\\mathbf\{x\}\)^\{2\}\.
2. 2\.There exists a symmetric positive semidefinite Gram matrixG∈𝕊m∩ℚm×mG\\in\\mathbb\{S\}^\{m\}\\cap\\mathbb\{Q\}^\{m\\times m\}such that f​\(𝐱\)=𝐯​\(𝐱\)⊤​G​𝐯​\(𝐱\),G⪰0\.f\(\\mathbf\{x\}\)=\{\\mathbf\{v\}\}\(\\mathbf\{x\}\)^\{\\top\}G\\,\{\\mathbf\{v\}\}\(\\mathbf\{x\}\),\\qquad G\\succeq 0\.

For the numerical solutionGNG\_\{N\}obtained after the Gauss–Newton refinement, when the backward errorθ\\thetais sufficiently small, one can recover fromGNG\_\{N\}an exact rational PSD matrixG~\\widetilde\{G\}, which satisfies the polynomial identity exactly, thereby yielding a certified rational SOS certificate\. Which satisfies the following identity:

f​\(x\)−𝐯​\(x\)⊤​G~​𝐯​\(x\)=0,G~⪰0\.f\(x\)\-\{\\mathbf\{v\}\}\(x\)^\{\\top\}\\widetilde\{G\}\{\\mathbf\{v\}\}\(x\)=0,\\qquad\\widetilde\{G\}\\succeq 0\.\(25\)
The matrixGGis projected onto the following affine hyperplane:

𝒳=\{G\|G⊤=G,f​\(x\)−𝐯​\(x\)⊤​G​𝐯​\(x\)=0\}\.\\mathcal\{X\}=\\left\\\{G\\;\\middle\|\\;G^\{\\top\}=G,f\(x\)\-\{\\mathbf\{v\}\}\(x\)^\{\\top\}G\\,\{\\mathbf\{v\}\}\(x\)=0\\;\\right\\\}\.\(26\)Suppose that the affine hyperplane defined by[Equation26](https://arxiv.org/html/2605.15445#A3.E26)can be represented by a linear systemA​y=bAy=b, whereyyconsist of the entries ofGG\. If the matrixAAhas full row rank, then such a hyperplane is guaranteed to exist\.

The recovery strategy depends on whether the refined Gram matrix lies in the interior of the PSD cone\.

An exact solution satisfying[Equation25](https://arxiv.org/html/2605.15445#A3.E25)can be obtained via the following two approaches:

- •Case 1: If the matrixGNG\_\{N\}is of full rank, the solution is recovered by applying an orthogonal projection method\.
- •Case 2: Otherwise, a rational vector recovery method is employed\.

##### Case 1: Interior Point Solution \(GNG\_\{N\}is full rank\)\.

The solution of[Equation25](https://arxiv.org/html/2605.15445#A3.E25)lies in the intersection of the affine hyperplane𝒳\\mathcal\{X\}and the positive semidefinite cone\. To computeG~\\widetilde\{G\}, the corresponding orthogonal projection can be obtained by solving the following least\-squares problem\.

minG⪰0∥GN−G∥F2s\.t\.f\(x\)=𝐯\(x\)⊤G𝐯\(x\)\.\\min\_\{G\\succeq 0\}\\;\\;\\lVert G\_\{N\}\-G\\rVert\_\{F\}^\{2\}\\quad\\text\{s\.t\. \}f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}G\\,\{\\mathbf\{v\}\}\(x\)\.\(27\)
Next, to verify whether the recovered rational solutionG~\\widetilde\{G\}is a symmetric positive semidefinite matrix, we compute the exactL​D​L⊤LDL^\{\\top\}decomposition ofG~\\widetilde\{G\}\.

f​\(x\)=𝐯​\(x\)⊤​G~​𝐯​\(x\)=𝐯​\(x\)⊤​L​D​L⊤​𝐯​\(x\)f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}\\widetilde\{G\}\{\\mathbf\{v\}\}\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}LDL^\{\\top\}\{\\mathbf\{v\}\}\(x\)\(28\)
###### Theorem C\.3\.

LetGNG\_\{N\}be the refined numerical solution whose backward error satisfiesθ<τ\\theta<\\tau, and letA​y=bAy=bbe the linear system associated with the affine hyperplane defined by[Equation26](https://arxiv.org/html/2605.15445#A3.E26)\. Suppose thatG~\\widetilde\{G\}is the optimal rational solution of the least\-squares[Equation27](https://arxiv.org/html/2605.15445#A3.E27), and that the matrixAAhas full row rank\. If the minimal eigenvalueλ\\lambdaofG~\\widetilde\{G\}satisfies

λ\>∥GN∥F2​κ22​\(A\)​τ2,\\lambda\>\\lVert G\_\{N\}\\rVert\_\{F\}^\{2\}\\kappa\_\{2\}^\{2\}\(A\)\\tau^\{2\},\(29\)
thenG~\\widetilde\{G\}is an exact solution of[Equation25](https://arxiv.org/html/2605.15445#A3.E25)\.

Proof\.SinceG~\\widetilde\{G\}is a solution of Problem \([27](https://arxiv.org/html/2605.15445#A3.E27)\), it clearly satisfies the polynomial identityf​\(x\)=𝐯​\(x\)⊤​G~​𝐯​\(x\)f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}\\widetilde\{G\}\{\\mathbf\{v\}\}\(x\)\. LetyNy\_\{N\}andy~\\widetilde\{y\}denote the vectors consisting of the entries ofGNG\_\{N\}andG~\\widetilde\{G\}, respectively\. From \([26](https://arxiv.org/html/2605.15445#A3.E26)\), and under the assumption that the matrixAAhas full row rank, we have

∥A​yN−b∥22=θ<τ,A​y~=b\.\\lVert Ay\_\{N\}\-b\\rVert\_\{2\}^\{2\}=\\theta<\\tau,\\qquad A\\widetilde\{y\}=b\.\(30\)According to the perturbation result\(Golub & Van Loan,[2013](https://arxiv.org/html/2605.15445#bib.bib14)\)for full\-row\-rank underdetermined linear systems, the following estimate holds:

∥yN−y~∥2≤\(κ2​\(A\)​τ\)​∥yN∥2\+O​\(τ2\)\.\\lVert y\_\{N\}\-\\widetilde\{y\}\\rVert\_\{2\}\\leq\(\\kappa\_\{2\}\(A\)\\tau\)\\lVert y\_\{N\}\\rVert\_\{2\}\+O\(\\tau^\{2\}\)\.\(31\)Under the assumption thatλ\>∥GN∥F2​κ22​\(A\)​τ2,\\lambda\>\\lVert G\_\{N\}\\rVert\_\{F\}^\{2\}\\kappa\_\{2\}^\{2\}\(A\)\\tau^\{2\},it follows that

∥GN−G~∥F2≤∥yN−y~∥22<λ\\lVert G\_\{N\}\-\\widetilde\{G\}\\rVert\_\{F\}^\{2\}\\leq\\lVert y\_\{N\}\-\\widetilde\{y\}\\rVert\_\{2\}^\{2\}<\\lambda\(32\)where the inequality∥yN−y~∥22<λ\\lVert y\_\{N\}\-\\widetilde\{y\}\\rVert\_\{2\}^\{2\}<\\lambdaholds because the higher\-order termO​\(τ2\)O\(\\tau^\{2\}\)is negligible whenτ\\tauis sufficiently small\. Letλ~\\widetilde\{\\lambda\}denote an eigenvalue ofG~\\widetilde\{G\}\. By the Wielandt–Hoffman theorem\(Golub & Van Loan,[2013](https://arxiv.org/html/2605.15445#bib.bib14)\), we obtain

\|λ~−λ\|≤∥GN−G~∥F2≤λ,\|\\widetilde\{\\lambda\}\-\\lambda\|\\leq\\lVert G\_\{N\}\-\\widetilde\{G\}\\rVert\_\{F\}^\{2\}\\leq\\lambda,\(33\)which implies that all eigenvalues ofG~\\widetilde\{G\}are nonnegative\. Therefore, we conclude thatG~⪰0\\widetilde\{G\}\\succeq 0\.

##### Case 2: Boundary Solution \(GNG\_\{N\}is rank\-deficient\)\.

When the numerical Gram matrixGNG\_\{N\}obtained via Gauss–Newton refinement is rank\-deficient or ill\-conditioned \(near\-singular\), the affine hyperplane𝒳\\mathcal\{X\}defined by the linear constraints is typically tangent to the boundary of the positive semidefinite \(PSD\) cone\. In such instances,GNG\_\{N\}does not reside within the interior of the PSD cone; consequently, direct orthogonal projection may yield a rational matrixG~\\widetilde\{G\}that violates the semi\-definiteness requirement\. We provides a rigorous discussion on the structural origins of such cases and presents a theoretical framework for exact recovery based on rational vector reconstruction\.

- •Redundant Monomials: In the construction of the SOS decomposition, a monomial basis that is not strictly necessary may be used\. This situation can be avoided by exploring the sparse structure of the polynomial or by removing entire rows and columns of the Gram matrixGNG\_\{N\}that correspond to numerically small entries, i\.e\., eliminating the monomials that should not appear in the polynomial’s SOS representation\.
- •Intrinsic Singularity: If the polynomialf​\(x\)f\(x\)attains its global minimum at a nonzero real point\(ξ1,…,ξn\)\(\\xi\_\{1\},\\dots,\\xi\_\{n\}\), then the monomial vector𝐯\(ξ\{\\mathbf\{v\}\}\(\\xi\) at this point is a zero vector in the Gram matrixGNG\_\{N\}, implying thatGNG\_\{N\}is singular\. When the global minimum is attained only at finitely many nonzero points, and the backward errorθ\\thetais sufficiently small, the Gram matrix can be rendered full rank by performing Gauss–Newton refinement, after which an orthogonal projection can be applied\. In contrast, when the global minimum is attained on some manifolds, we apply the Gauss–Newton iteration to a truncated triangular decomposition ofGNG\_\{N\}\. Once the residual is sufficiently small, a rational recovery ofGNG\_\{N\}is carried out via a simultaneous Diophantine approximation algorithm\(Lagarias,[1985](https://arxiv.org/html/2605.15445#bib.bib19)\)\.

## Appendix DNeural Conjectur Midule Configuration

### D\.1Prompt Template

Here we present the prompt template employed by the SOS structure conjecture module in theneural conjecturemodule\. For a given nonnegative polynomial, the SOS structure conjecturer generates a candidate SOS structural conjecture based on an expanded\-form representation, with the objective that the proposed SOS structure matches the target polynomial as closely as possible\.

Prompt Template for SOS Structure ConjecturerTask:You are given a polynomial that is the expanded form of a sum\-of\-squares \(SOS\) expression\. Your task is to reconstruct a plausible SOS representation whose expanded form matches the given polynomial as closely as possible\.Instructions:1\. Analyze the input polynomial carefully, focusing on the coefficients and the combinations of variables involved\.2\. Infer possible linear or polynomial terms inside each square in the sum\-of\-squares expression\.3\. Construct a sum of square terms without expanding the squares\. Keep the output compact and well\-structured\.4\. Aim for the expanded form of your SOS expression to closely approximate the coefficients in the original polynomial\. Minor numerical deviations are acceptable\.5\. If multiple valid SOS decompositions exist, prefer one that is simple, symmetric, and easy to interpret\.6\. Include variables and constants inside parentheses when appropriate to match constant terms in the input polynomial\.Output format:Please provide your response in the following structure:<SOS Expression\>: <sum\_of\_squares\_expression\>Where<sum\_of\_squares\_expression\>is a sum\-of\-squares term, expressed compactly\.For example:\(x1 \+ 1\)^2 \+ \(2\*x1 \+ 3\*x2\)^2Key considerations:1\. Do not simply rewrite the input polynomial or output expanded terms\. The output must be a sum\-of\-squares expression\.2\. Constants inside square terms can be fractional or decimal, as needed, to best approximate the original polynomial\.3\. Avoid expanding the squares in the output; always keep terms inside parentheses squared\.4\. Aim for clear and interpretable variable groupings\. Symmetry and simplicity are preferred if multiple answers fit\.5\. Your SOS expression should fully explain the input polynomial’s structure and coefficients to the best achievable extent\.Example:Input polynomial:x1^2 \+ 2\*x1 \+ 1Output: \(SOS Expression\): \(x1 \+ 1\)^2Explanation: The polynomial is a perfect square trinomial; the SOS reconstruction is exact\.Input polynomial: 5\*x1^2 \+ 12\*x1\*x2 \+ 6\*x1 \+ 9\*x2^2 \+ 9Output: \(SOS Expression\): \(x1 \+ 2\.99\)^2 \+ \(2\*x1 \+ 3\*x2\)^2Now, please provide the SOS reconstruction for the following polynomial: Original polynomial: \{polynomial\}

As illustrated by the prompt template above, it consists of a task description, multiple explicit instructions specifying the required output format and content constraints for the large language model, and several illustrative examples provided to guide the generation process\.

### D\.2Synthetic Dataset Statistics

During the data construction stage of theneural conjecturemodule, we generate more than 100w synthetic data instances using the four data generation strategies proposed in Section[4\.1\.1](https://arxiv.org/html/2605.15445#S4.SS1.SSS1), including bothcomputation\-drivenandstructure\-drivenapproaches\. These synthetic datasets, covering problems with varying numbers of variables ranging from 3 to 10, are used as the training corpus for the neural conjecturer\.

Notably, we performed amanual quality inspectionof the synthesized polynomial–SOS pair data via random sampling\. For each variable setting from 3 to 10, we randomly sampled 50 instances for review\. The inspection results indicate that the synthesized data contain no formatting errors andencompass polynomial SOS decomposition cases of varying difficulty, including a substantial proportion ofhighly non\-trivial instancesthat pose significant challenges to conventional symbolic solvers\. Additionally, we computed the degree and number of SOS terms of the synthesized data\. The statistical results are reported in Fig\.[7](https://arxiv.org/html/2605.15445#A4.F7)and Fig\.[8](https://arxiv.org/html/2605.15445#A4.F8)\.

![Refer to caption](https://arxiv.org/html/2605.15445v1/x7.png)Figure 7:Statistical distribution of degrees for synthetic polynomial data\.![Refer to caption](https://arxiv.org/html/2605.15445v1/x8.png)Figure 8:Statistical distribution of SOS term counts in synthetic polynomials\.As illustrated in Fig\.[7](https://arxiv.org/html/2605.15445#A4.F7)and Fig\.[8](https://arxiv.org/html/2605.15445#A4.F8), the synthetic dataset exhibits significant diversity in both algebraic complexity and representation structure\. Specifically, the degrees of the synthesized polynomials span a wide range from 2 to 22, ensuring the model is exposed to problems of varying algebraic depths; this reflects that the synthetic data encompasses both relatively simple low\-degree polynomials and structurally sophisticated high\-degree instances\. Furthermore, the distribution of SOS term counts covers a spectrum ranging from basic single\-term squares to complex decomposition instances involving up to 15 terms\. Such structural diversity indicates that our construction strategies effectively cover a broad difficulty spectrum, preventing the model from over\-fitting to specific sparse or low\-degree patterns\.

### D\.3Additional Details of Progressive Reinforcement Learning Process

For the progressive two\-stage training procedure of the SOS\-structure conjecturer described in Section[4\.1\.2](https://arxiv.org/html/2605.15445#S4.SS1.SSS2), in the second stage we employ acurriculum\-style GRPOreinforcement learning process\. Here, we provide the theoretical foundations and several implementation details\.

##### Group Relative Policy Optimization \(GRPO\)\.

Group Relative Policy Optimization \(GRPO\)\(Shao et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib46)\)is a reinforcement learning algorithm used for fine\-tuning large language models \(LLMs\)\. Unlike the popular Proximal Policy Optimization \(PPO\), GRPO enhances efficiency by eliminating the need for a separate value function\. It estimates the advantage by normalizing the rewards of a set of responses to the same prompt\. Specifically, for each questionqqin a given setQQ, a set of responses\{o1,…,oG\}\\\{o\_\{1\},\\dots,o\_\{G\}\\\}is sampled from the old policyπold\\pi\_\{\\text\{old\}\}\. The reward model then evaluates these responses, generating rewards\{r1,…,rG\}\\\{r\_\{1\},\\dots,r\_\{G\}\\\}, and the advantage is computed as follows:

A^​i=ri−mean​\(r1,…,rG\)std​\(r1,…,rG\)\\displaystyle\\hat\{A\}i=\\frac\{r\_\{i\}\-\\text\{mean\}\(\{r\_\{1\},\\dots,r\_\{G\}\}\)\}\{\\text\{std\}\(\{r\_\{1\},\\dots,r\_\{G\}\}\)\}\(34\)The policy modelπθ\\pi\_\{\\theta\}is then optimized by maximizing the following objective:

JGRPO\(θ\)=𝔼q∼Q,\{oi\}​i=1G∼πold​\(O\|q\)1G∑i=1G1\|oi\|∑t=1\|oi\|\{min\[γi,t\(θ\)A^i,t,clip\(γi,t\(θ\),1−ϵ,1\+ϵ\)A^i,t\]−βDKL\(πθ\|\|πref\)\}J\_\{\\text\{GRPO\}\}\(\\theta\)=\\mathbb\{E\}\_\{q\\sim Q,\\\{o\_\{i\}\\\}\{i=1\}^\{G\}\\sim\\pi\_\{\\text\{old\}\}\(O\|q\)\}\\frac\{1\}\{G\}\\sum\_\{i=1\}^\{G\}\\frac\{1\}\{\|o\_\{i\}\|\}\\sum\_\{t=1\}^\{\|o\_\{i\}\|\}\\\{\\min\\left\[\\gamma\_\{i,t\}\(\\theta\)\\hat\{A\}\_\{i,t\},\\text\{clip\}\\left\(\\gamma\_\{i,t\}\(\\theta\),1\-\\epsilon,1\+\\epsilon\\right\)\\hat\{A\}\_\{i,t\}\\right\]\-\\beta D\_\{\\text\{KL\}\}\(\\pi\_\{\\theta\}\|\|\\pi\_\{\\text\{ref\}\}\)\\\}\(35\)
whereγi,t​\(θ\)=πθ​\(oi,t\|q,oi,<t\)πold​\(oi,t\|q,oi,<t\)\\gamma\_\{i,t\}\(\\theta\)=\\frac\{\\pi\_\{\\theta\}\(o\_\{i,t\}\|q,o\_\{i,<t\}\)\}\{\\pi\_\{\\text\{old\}\}\(o\_\{i,t\}\|q,o\_\{i,<t\}\)\}is the importance sampling ratio,πref\\pi\_\{\\text\{ref\}\}represents the reference model,πold\\pi\_\{\\text\{old\}\}is the policy used to sample the responses, andDKL\(πθ\|\|πref\)D\_\{\\text\{KL\}\}\(\\pi\_\{\\theta\}\|\|\\pi\_\{\\text\{ref\}\}\)introduces a KL divergence constraint to limit the deviation of the model from the reference model\.

##### Difficulty\-Based Curriculum Data Partitioning\.

As discussed in[Section4\.1\.2](https://arxiv.org/html/2605.15445#S4.SS1.SSS2), we partition the training data based on the difficulty of polynomial SOS decomposition in the dataset, obtaining multiple groups of training data with varying difficulty levels\. Each group is then trained using a Graduated Reinforcement Policy Optimization \(GRPO\) approach, progressing from easier to more challenging data\. Specifically, we categorize the data into three tiers based on the ascending number of polynomial variables: Polynomial\-SOS pairs data with 3 to 5 variables are used in the first stage, data with 6 to 8 variables in the second stage, and the more challenging data with 9 to 10 variables in the third stage\. GRPO training is conducted sequentially across these three stages\.

##### Reward Functions Design\.

As illstrated in[Section4\.1\.2](https://arxiv.org/html/2605.15445#S4.SS1.SSS2), the reward function design includes three key components:

- •\[accuracy reward\]encourages SOS structure conjectures with smaller errors compared to the original polynomial\.
- •\[format reward\]ensures that the model\-generated conjectures adhere to the required SOS structure\.
- •\[algebraic structure penalty\]penalizes the SOS structure hypothesis based on the degree of term matching with the original polynomial\.

The total reward is defined as:

R=wacc​Racc\+wfmt​Rfmt−Pstruct,\\displaystyle R=w\_\{\\text\{acc\}\}R\_\{\\text\{acc\}\}\+w\_\{\\text\{fmt\}\}R\_\{\\text\{fmt\}\}\-P\_\{\\text\{struct\}\},\(36\)wherewacc\+wfmt=1w\_\{\\text\{acc\}\}\+w\_\{\\text\{fmt\}\}=1,Racc∈\[0,1\]R\_\{\\text\{acc\}\}\\in\[0,1\]denotes the accuracy reward based on the approximation error,Rfmt∈\[0,1\]R\_\{\\text\{fmt\}\}\\in\[0,1\]denotes the format consistency reward,PstructP\_\{\\text\{struct\}\}denotes the algebraic structure penalty\.

##### Computation of Algebraic Structure Penalty\.

The algebraic structure penalty consists of two components: a soft penalty and a hard penalty\. To accurately assess the algebraic structure, we express the original polynomialffand the model\-generated SOS conjecturef^\\hat\{f\}in terms of a common monomial basis\. A coefficient thresholdτ\\tau\(e\.g\.,10−510^\{\-5\}\) is set, such that a monomial is considered present in the polynomial \(i\.e\., a nonzero term\) only if the absolute value of its coefficient exceedsτ\\tau\.

We define Structural Deviation Rate \(SDR\) to quantify the discrepancy between the algebraic structure of the SOS representation and that of the original polynomial:

S​D​R=Nmiss\+NspurNreq,\\displaystyle SDR=\\frac\{N\_\{\\text\{miss\}\}\+N\_\{\\text\{spur\}\}\}\{N\_\{\\text\{req\}\}\},\(37\)whereNreqN\_\{\\text\{req\}\}denotes the number of nonzero monomials in the original polynomial,NmissN\_\{\\text\{miss\}\}is the number of monomials that appear in the original polynomial but are absent inf^\\hat\{f\}, andNspurN\_\{\\text\{spur\}\}is the number ofextraneous termspresent inf^\\hat\{f\}but not belonging to the monomial set𝒱f\\mathcal\{V\}\_\{f\}\.

The soft penalty is defined as

Pstruct\-soft=λ⋅min⁡\(SDR,ρmax\),\\displaystyle P\_\{\\text\{struct\-soft\}\}=\\lambda\\cdot\\min\(\\text\{SDR\},\\rho\_\{\\max\}\),\(38\)whereλ\\lambdacontrols the strength of the penalty andρmax\\rho\_\{\\max\}caps the maximum penalty\.

If the generated SOS structure exhibits severe algebraic inconsistencies \(e\.g\., exceeding the degree of the original polynomial or introducing variables not present in it\), a hard penalty is imposed:

Pstruct\-hard=\{Chard,if a structural violation occurs0,otherwise\\displaystyle P\_\{\\text\{struct\-hard\}\}=\\begin\{cases\}C\_\{\\text\{hard\}\},&\\text\{if a structural violation occurs\}\\\\ 0,&\\text\{otherwise\}\\end\{cases\}\(39\)
The overall algebraic structure penalty is the sum of the soft and hard penalties:

Pstruct=Pstruct\-hard\+Pstruct\-soft\.\\displaystyle P\_\{\\text\{struct\}\}=P\_\{\\text\{struct\-hard\}\}\+P\_\{\\text\{struct\-soft\}\}\.\(40\)

## Appendix EFurther Details of Lean Verification Module

![Refer to caption](https://arxiv.org/html/2605.15445v1/x9.png)Figure 9:Automated Lean Proof Generation Example\.left:The pre\-defined Lean Proof Template\.right:An Example of automated proof generation within Lean4, where the formal verification is completed using the integrated tactic“LLM\_Ineq”\.### E\.1Lean Template of Proof

Here presents the Lean4 proof template referenced in section[Section4\.3](https://arxiv.org/html/2605.15445#S4.SS3), which yields a verifiable formal proof based on the exact sum\-of\-squares \(SOS\) representation of a non\-negative polynomial\.

Lean Proof Template[⬇](data:text/plain;base64,Ly0tCkdlbmVyYWwgdGVtcGxhdGUgZm9yIFNPUy1iYXNlZCBpbmVxdWFsaXR5IHByb29mcy4KYDxUaGVvcmVtX05hbWU+YCA6IGN1c3RvbWl6ZWQgdGhlb3JlbSBuYW1lLgpgPFBvbHlub21pYWw+YCA6IHRhcmdldCBwb2x5bm9taWFsIGV4cHJlc3Npb24uCmA8RXhhY3QgU09TIEV4cHJlc3Npb24+YCA6IGxpc3Qgb2Ygd2VpZ2h0ZWQgc3F1YXJlIHRlcm1zIHJlcHJlc2VudGluZyB0aGUgU09TIGRlY29tcG9zaXRpb24uCi0vCnRoZW9yZW0gPFRoZW9yZW1fTmFtZT4gKHgxIHgyIC4uLiB4biA6IFJlYWwpCiAgKGgxIDogSSA9IDxQb2x5bm9taWFsPikgOgogIEkgPj0gMCA6PSBieQogIC0tIFN0ZXAgMTogQ29uc3RydWN0IFNPUyB0ZXJtIGxpc3QKICBsZXQgdGVybXMgOiBMaXN0IChSZWFsICRcdGltZXMkIFJlYWwpIDo9CiAgICBbIDxFeGFjdCBTT1MgRXhwcmVzc2lvbj4gXQogIC0tIFN0ZXAgMjogUHJvdmUgZXF1YWxpdHkgYmV0d2VlbiBwb2x5bm9taWFsIGFuZCBpdHMgU09TIGV4cGFuc2lvbgogIGhhdmUgOiBJID0gKHRlcm1zLm1hcCAoZnVuIChwLCBrKSA9PiBwICoga14yKSkuc3VtIDo9IGJ5CiAgICB1bmZvbGQgdGVybXMKICAgIHNpbXAgb25seSBbTGlzdC5tYXBfY29ucywgTGlzdC5tYXBfbmlsLCBMaXN0LnN1bV9jb25zLCBMaXN0LnN1bV9uaWwsCiAgICAgIG9uZV9tdWwsIG11bF9vbmUsIHplcm9fbXVsLCBhZGRfemVybywgemVyb19hZGQsIG5lZ19tdWxdCiAgICBsaW5lYXJfY29tYmluYXRpb24gaDEKICAtLSBTdGVwIDM6IFN1YnN0aXR1dGUgYW5kIHNpbXBsaWZ5CiAgcncgW3RoaXNdCiAgdW5mb2xkIHRlcm1zCiAgc2ltcCBvbmx5IFtMaXN0Lm1hcF9jb25zLCBMaXN0Lm1hcF9uaWwsIExpc3Quc3VtX2NvbnMsIExpc3Quc3VtX25pbCwKICAgIG9uZV9tdWwsIG11bF9vbmUsIHplcm9fbXVsLCBhZGRfemVybywgemVyb19hZGQsIGdlX2lmZl9sZV0KICAtLSBTdGVwIDQ6IEFwcGx5IHBvc2l0aXZpdHkgdGFjdGljIHRvIGNvbmNsdWRlCiAgcG9zaXRpdml0eQ==)GeneraltemplateforSOS\-basedinequalityproofs\.‘<Theorem\_Name\>‘:customizedtheoremname\.‘<Polynomial\>‘:targetpolynomialexpression\.‘<ExactSOSExpression\>‘:listofweightedsquaretermsrepresentingtheSOSdecomposition\.\-/theorem<Theorem\_Name\>\(x1x2\.\.\.xn:Real\)\(h1:I=<Polynomial\>\):I\>=0:=byletterms:List\(Real×\\timesReal\):=\[<ExactSOSExpression\>\]have:I=\(terms\.map\(fun\(p,k\)=\>p\*k^2\)\)\.sum:=byunfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil,one\_mul,mul\_one,zero\_mul,add\_zero,zero\_add,neg\_mul\]linear\_combinationh1rw\[this\]unfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil,one\_mul,mul\_one,zero\_mul,add\_zero,zero\_add,ge\_iff\_le\]positivityFigure 10:Lean template for inequality proof based on SOS representation\.The template uses the following placeholders:

- •<Theorem\_Name\>: the customized theorem name;
- •<Polynomial\>: the target polynomial expression \(often an expanded or normalized form equivalent to the original\);
- •<Exact SOS Expression\>: a list of exact square terms constituting the SOS certificate, encoded as a Lean list of pairs \(e\.g\.,\(p,k\)\(p,k\)\) representing a squared polynomialpptogether with its coefficientkk, according to the chosen encoding\.

The proof proceeds in four structured steps:

- •Step 1: Construct the SOS term list\.The SOS representation is introduced as terms :List​\(ℝ×ℝ\)=\[…\]\\text\{List\}\(\\mathbb\{R\}\\times\\mathbb\{R\}\)=\[\.\.\.\]containing all exact squared terms required for the proof\.
- •Step 2: Prove the polynomial identity\.A key lemma establishes that the target polynomial equals the sum of the expanded SOS terms\. This step typically relies on simp to unfold list combinatorsList\.map\_cons, List\.sum\_cons, etc\.and onlinear\_combinationto derive the exact identity from the provided equality hypothesis \(e\.g\.,h1 : I = <Polynomial\>\) together with auxiliary algebraic equalities\.
- •Step 3: Substitute and normalize the goal\.By rewriting with the established identity \(rw \[this\]\), the original goal is transformed into nonnegativity of a sum\-of\-squares, followed by additional simplifications to reach a form amenable to automation\.
- •Step 4: Conclude via positivity automation\.Finally, the positivity tactic is invoked to prove that a sum\-of\-squares is nonnegative, completing the formal verification ofI​\(𝐱\)≥0I\(\\mathbf\{x\}\)\\geq 0\.

### E\.2An Example of Automated Lean Proof Generation

Fig\.[9](https://arxiv.org/html/2605.15445#A5.F9)illustrates the structure of the proof template and an example of automated proof generation\.

## Appendix FAlgorithm

Here provides the overall pseudocode for the proposed NSPI method \([Algorithm1](https://arxiv.org/html/2605.15445#alg1)\), along with the detailed pseudocodes for the progressive two\-stage training process of the neural conjecture module \([Algorithm2](https://arxiv.org/html/2605.15445#alg2)\), the Newton iteration \([Algorithm3](https://arxiv.org/html/2605.15445#alg3)\), and the rational recovery process \([Algorithm4](https://arxiv.org/html/2605.15445#alg4)\) within the symbolic correction module\.

Algorithm 1Overall Proof Generation Process of NSPI0:Target polynomial

f​\(x\)f\(x\); SOS structure conjecturer

MM; candidate budget

KK\.

0:A verified Lean proof script

𝒫f​o​r​m​a​l\\mathcal\{P\}\_\{formal\}, orFailure\.

1:Stage 1: Neural Conjecture

2:

𝒮a​p​p​r​o​x←M​\(f​\(x\),K\)\\mathcal\{S\}\_\{approx\}\\leftarrow M\(f\(x\),K\)⊳\\trianglerightGenerateKKSOS\-structure conjectures

3:Rank

𝒮a​p​p​r​o​x\\mathcal\{S\}\_\{approx\}by

θ​\(s\)=‖f^s​\(x\)−f​\(x\)‖2\\theta\(s\)=\\\|\\hat\{f\}\_\{s\}\(x\)\-f\(x\)\\\|\_\{2\}
4:Stage 2: Symbolic Correction

5:foreach structure

ssin

𝒮a​p​p​r​o​x\\mathcal\{S\}\_\{approx\}do

6:

GN←NewtonIteration​\(f​\(x\),s\)G\_\{N\}\\leftarrow\\text\{NewtonIteration\}\(f\(x\),s\)⊳\\trianglerightGauss–Newton refinement to obtainGNG\_\{N\}with small backward error

7:

Sr​a​t←RationalRecovery​\(GN\)S\_\{rat\}\\leftarrow\\text\{RationalRecovery\}\(G\_\{N\}\)⊳\\trianglerightInterior/boundary rational recovery

8:if

IsExactSOS​\(f​\(x\),Sr​a​t\)\\textsc\{IsExactSOS\}\(f\(x\),S\_\{rat\}\)then

9:break⊳\\trianglerightAn exact rational SOS certificate is found

10:endif

11:endfor

12:Stage 3: Formal Verification

13:if

Sr​a​tS\_\{rat\}is foundthen

14:

𝒫f​o​r​m​a​l←TemplateFill​\(f​\(x\),Sr​a​t\)\\mathcal\{P\}\_\{formal\}\\leftarrow\\textsc\{TemplateFill\}\(f\(x\),S\_\{rat\}\)⊳\\trianglerightGenerate Lean script from templates

15:if

LeanCheck​\(𝒫f​o​r​m​a​l\)\\textsc\{LeanCheck\}\(\\mathcal\{P\}\_\{formal\}\)then

16:return

𝒫f​o​r​m​a​l\\mathcal\{P\}\_\{formal\}
17:endif

18:endif

19:returnFailure\.

Algorithm 2Progressive Two\-Stage Training of the SOS Structure Conjecturer0:Base language model

M0M\_\{0\}; data construction methods

𝒟=\{𝒟1,…,𝒟4\}\\mathcal\{D\}=\\\{\\mathcal\{D\}\_\{1\},\\dots,\\mathcal\{D\}\_\{4\}\\\}; curriculum schedule

𝒞\\mathcal\{C\}; GRPO hyperparameters\.

0:Trained SOS structure conjecturer

MM\.

1:Stage 1: Data Construction and Supervised Fine\-Tuning

2:Construct synthetic polynomial–SOS pairs

𝒮←⋃j=14𝒟j\\mathcal\{S\}\\leftarrow\\bigcup\_\{j=1\}^\{4\}\\mathcal\{D\}\_\{j\}⊳\\trianglerightFour construction methods

3:Train

M0M\_\{0\}on

𝒮\\mathcal\{S\}via teacher forcing to obtain

MSFTM\_\{\\mathrm\{SFT\}\}⊳\\trianglerightSupervised fine\-tuning

4:Stage 2: Curriculum Reinforcement Learning

5:Evaluate

MSFTM\_\{\\mathrm\{SFT\}\}on

𝒮\\mathcal\{S\}and collect unsolved samples

𝒰\\mathcal\{U\}
6:Partition

𝒰\\mathcal\{U\}into curriculum buckets

\{𝒰1,…,𝒰L\}\\\{\\mathcal\{U\}\_\{1\},\\dots,\\mathcal\{U\}\_\{L\}\\\}by

𝒞\\mathcal\{C\}⊳\\trianglerightIncreasing difficulty

7:for

ℓ=1\\ell=1to

LLdo

8:foreach mini\-batch

ℬ⊂𝒰ℓ\\mathcal\{B\}\\subset\\mathcal\{U\}\_\{\\ell\}do

9:Sample SOS conjectures

\{Si\}\\\{S\_\{i\}\\\}from

MMfor each

\(f,S⋆\)∈ℬ\(f,S^\{\\star\}\)\\in\\mathcal\{B\}⊳\\trianglerightPolicy rollout

10:Compute reward

R​\(Si\)←Racc​\(Si\)\+Rfmt​\(Si\)−Palg​\(Si\)R\(S\_\{i\}\)\\leftarrow R\_\{\\text\{acc\}\}\(S\_\{i\}\)\+R\_\{\\text\{fmt\}\}\(S\_\{i\}\)\-P\_\{\\text\{alg\}\}\(S\_\{i\}\)⊳\\trianglerightAccuracy, format, and algebraic penalty

11:Update

MMvia GRPO to maximize

𝔼​\[R\]\\mathbb\{E\}\[R\]⊳\\trianglerightReinforcement learning

12:endfor

13:endfor

14:return

MM⊳\\trianglerightTrained SOS structure conjecturer

Algorithm 3NewtonIteration: Gauss–Newton Refinement for SOS Certificates0:Polynomial

f​\(x\)f\(x\); SOS structure

ss; tolerance

τ\\tau; max steps

TNT\_\{N\}\.

0:Refined numerical Gram matrix

GNG\_\{N\}\(or

∅\\emptyset\)\.

1:Build monomial basis

𝐯​\(x\)\{\\mathbf\{v\}\}\(x\)implied by

ssand initialize floating Gram matrix

G\(0\)G^\{\(0\)\}\.

2:for

t=0t=0to

TN−1T\_\{N\}\-1do

3:Compute backward error

θ\(t\)=‖f​\(x\)−𝐯​\(x\)⊤​G\(t\)​𝐯​\(x\)‖2\\theta^\{\(t\)\}=\\\|f\(x\)\-\{\\mathbf\{v\}\}\(x\)^\{\\top\}G^\{\(t\)\}\{\\mathbf\{v\}\}\(x\)\\\|\_\{2\}\.

4:if

θ\(t\)≤τ\\theta^\{\(t\)\}\\leq\\tauthen

5:return

GN←G\(t\)G\_\{N\}\\leftarrow G^\{\(t\)\}
6:endif

7:Update

G\(t\)G^\{\(t\)\}by one Gauss–Newton step \(via Cholesky parameterization\)\.

8:endfor

9:return

∅\\emptyset\.

Algorithm 4RationalRecovery: Exact Rational SOS Certificate Recovery0:Polynomial

f​\(x\)f\(x\); SOS structure

ss; refined Gram matrix

GNG\_\{N\}; rank threshold

ϵ\\epsilon; precision

ρ\\rho\.

0:Exact rational SOS certificate

Sr​a​tS\_\{rat\}\(or

∅\\emptyset\)\.

1:Form affine constraints from coefficient matching:

f​\(x\)=𝐯​\(x\)⊤​G​𝐯​\(x\)f\(x\)=\{\\mathbf\{v\}\}\(x\)^\{\\top\}G\{\\mathbf\{v\}\}\(x\)\.

2:if

NumRank​\(GN,ϵ\)\\textsc\{NumRank\}\(G\_\{N\},\\epsilon\)is fullthen

3:Project

GNG\_\{N\}onto the affine constraint and rationalize entries with precision

ρ\\rho\.

4:else

5:Perform truncated

L​D​L⊤LDL^\{\\top\}and LLL\-based rational vector recovery to preserve rank\.

6:endif

7:Construct

Sr​a​tS\_\{rat\}from the recovered rational Gram matrix andreturn

Sr​a​tS\_\{rat\}\.

## Appendix GExperimental Details

### G\.1Implementation Details

During the data construction phase of the neural conjecture module, over one million training instances were generated based on the proposed construction methods\. Qwen3\-8B\(Team,[2025](https://arxiv.org/html/2605.15445#bib.bib47)\)was employed as the base model for SOS structure conjecturing\. In the reinforcement learning phase, progressive multi\-round training was conducted using curriculum data organized by the increasing number of variables: Stage 1 \(3–5 variables\), Stage 2 \(6–8 variables\), and Stage 3 \(9–10 variables\)\. The reward function parameters were configured withα=0\.5\\alpha=0\.5,λ=0\.5\\lambda=0\.5, andCh​a​r​d=0\.5C\_\{hard\}=0\.5, with the accuracy weightwa​c​cw\_\{acc\}set to0\.90\.9\. Within the symbolic correction module, the tolerance thresholdτ\\taufor Newton iteration was predefined as1e\-15\. During the inference phase, the computational budgetkkis set to 32, with a maximum time limit of 1 hour\.

### G\.2Baseline Setups

To ensure a fair comparison, we evaluate our method against several categories of approaches, including symbol\-based methods, LLM\-based provers, general\-purpose LLMs, and hybrid systems\. Detailed configurations and specifications for each category are provided below\.

- •Symbol\-based Method\.We evaluate the symbolic computation tools Maple\(Heck & Koepf,[1993](https://arxiv.org/html/2605.15445#bib.bib16)\)and Z3\(De Moura & Bjørner,[2008](https://arxiv.org/html/2605.15445#bib.bib9)\)\. For Maple, we perform symbolic decomposition and sampling of the semi\-algebraic set viaSamplePointsto check for the absence of negative values\. For Z3, we employ itsSMTsolver to formulate the problem as a satisfiability task under real arithmetic\.
- •LLM\-based Prover\.We consider state\-of\-the\-art \(SOTA\) LLM\-driven Lean automated theorem provers, including DeepSeek\-Prover\-V2\-7B\(Ren et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib44)\), Goedel\-Prover\-V2\-8B\(Lin et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib29)\), and Kimina Prover\(Wang et al\.,[2025](https://arxiv.org/html/2605.15445#bib.bib53)\)\. Each prover is tested using its respective default prompt templates\. In our main experiments, we compare their performance under a computational budget of pass@32\.
- •General\-purpose LLM\.This group encompasses the latest closed\-source foundation models, including GPT\-5\.2, Gemini\-3\-Pro\-Preview, and DeepSeek\-V3\.2\(DeepSeek\-AI,[2025](https://arxiv.org/html/2605.15445#bib.bib11)\)\. We assess their ability to generate Lean proofs directly from Lean theorem statements\.
- •Hybrid system\.We compare against the recent hybrid inequality\-proving system LIPS\(Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25)\), using its default experimental configuration\. It is worth noting that a comparison with several hybrid systems\(Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54); Li et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib26)\)was not feasible, as their source code is not publicly available for replication\. Furthermore, these methods primarily focus on addressing problems with 3 or 4 variables, as evidenced by the datasets described in their respective papers\.

### G\.3Details of Benchmark

Here we provide additional details onPolyIneqBench, the challenging inequality proving benchmark constructed in this work\.

Specifically, PolyIneqBench consists of a total of522inequality problems, which primarily categorized into two subsets based on their origin and complexity:

- •PolyIneq\-Real: This subset contains 102 inequality problems sourced from real\-world domains\. It comprises two main components: - –Classical benchmark inequalities, including the Schur inequality, Robinson polynomial, Delzell polynomial, Peyri–Parrilo polynomial, Lax polynomial, Nesbitt inequality, and Voronoi polynomial\. - –Problems derived from national and international mathematics competitions, as well as standard competition textbooks\. Representative examples of PolyIneq\-Real are presented in Table[4](https://arxiv.org/html/2605.15445#A7.T4)\.
- •PolyIneq\-Synth: To extend the benchmark to higher\-dimensional settings, we constructed this synthetic subset containing 420 inequalities spanning four to ten variables \(with 60 problems per variable count\)\. Each generated problem was validated by domain experts through manual quality assessment on randomly sampled instances \(see[SectionD\.2](https://arxiv.org/html/2605.15445#A4.SS2)\), ensuring non\-triviality and challenge\. Representative examples are provided in Table[5](https://arxiv.org/html/2605.15445#A7.T5)\.

Expanding to High\-Dimensional Settings:As shown in Table[4](https://arxiv.org/html/2605.15445#A7.T4), most problems in PolyIneq\-Real involve onlythreeorfourvariables\. PolyIneq\-Synth was specifically designed to address this limitation by introducing systematically constructed problems in higher\-dimensional settings\.

[Table3](https://arxiv.org/html/2605.15445#A7.T3)presents the distribution of polynomial inequalities within the PolyIneqBench, categorized by the number of variables \(nn\) and their respective sample sizes\.

Table 3:Distribution of Polynomial Inequalities by Variable Count in PolyIneqBench\.Variable Count \(n\)Sample Size3844775606617608609601060Table 4:Part of PolyIneq\-Real BenchmarkTable 5:Part of PolyIneq\-Synth Benchmark![Refer to caption](https://arxiv.org/html/2605.15445v1/x10.png)Figure 11:Detailed workflow of the NSPI method applied to the Peyrl\-Parrilo polynomial from PolyIneq\-Real \(Case 1\)\.This example illustrates the complete pipeline from initial conjecture to formal certification\.![Refer to caption](https://arxiv.org/html/2605.15445v1/x11.png)Figure 12:Case study of a challenging synthetic polynomial from PolyIneq\-Synth\.This 10\-variable instance represents a significant challenge in high\-dimensional formal reasoning; notably,NSPI is the sole method among all evaluated baselines \(Case 2\)capable of successfully generating a verified formal proof\.

## Appendix HCase Study

Here we provide detailed case studies illustrating the complete proof process of NSPI on two representative examples drawn from PolyIneqBench\.

Case 1 is a classical inequality from the PolyIneq\-Real subset, whereas Case 2 is a challenging competition\-level synthetic inequality from the PolyIneq\-Synth subset, corresponding to a higher\-dimensional and more difficult setting\. Notably, for Case 2, NSPI is theonly methodamong all baselines that successfully completes the proof\.

### H\.1Case 1: Peyrl\-Parrilo polynomial\.

Case 1 features a classic non\-negative polynomial drawn from\(Peyrl & Parrilo,[2008b](https://arxiv.org/html/2605.15445#bib.bib42); Le & Van Barel,[2014](https://arxiv.org/html/2605.15445#bib.bib23)\)\. Fig\.[11](https://arxiv.org/html/2605.15445#A7.F11)presents an example of generating a complete proof using the NSPI method\.

### H\.2Case 2: A challenging synthetic polynomial\.

We present a challenging 10\-variable synthetic polynomial instance from the PolyIneq\-Synth dataset\. Notably, for this specific case, NSPI is the only method among all considered baselines that successfully generates a complete formal proof\.

## Appendix IMore Experimental Results

### I\.1Results under Different Computational Budgets

Here, we report the performance of various LLM\-based provers and our NSPI method under different computational budgets\. The results on PolyIneqBench are summarized in[Table6](https://arxiv.org/html/2605.15445#A9.T6)\.

Table 6:Comparative results of multiple methods on PolyIneqBench under different computational budgets
### I\.2Detailed Comparative Study on Benchmark Difficulty Metrics

![Refer to caption](https://arxiv.org/html/2605.15445v1/x12.png)\(a\)Average Number of Terms in Polynomials Solved by Different Methods\.
![Refer to caption](https://arxiv.org/html/2605.15445v1/x13.png)\(b\)Average Total Degree of Terms in Polynomials Solved by Different Methods\.

Figure 13:Comparative analysis of different polynomial solving methods: \(a\) average number of terms; \(b\) average total degree\.![Refer to caption](https://arxiv.org/html/2605.15445v1/x14.png)Figure 14:Average number of variables in polynomial inequalities successfully verified by each method\.This metric illustrates the scalability of various provers, where NSPI \(ours\) demonstrates a superior capability in handling higher\-dimensional problems compared to both symbolic baselines and LLM\-based provers\.Fig\.[13](https://arxiv.org/html/2605.15445#A9.F13)and Fig\.[14](https://arxiv.org/html/2605.15445#A9.F14)present a comparative analysis of different polynomial inequality solving methods in terms of average number of terms \(Fig\.[13](https://arxiv.org/html/2605.15445#A9.F13)\(a\)\), average total degree \(Fig\.[13](https://arxiv.org/html/2605.15445#A9.F13)\(b\)\), and average number of variables \(Fig\.[14](https://arxiv.org/html/2605.15445#A9.F14)\) in successfully solved instances\.

Fig\.[13](https://arxiv.org/html/2605.15445#A9.F13)shows that our NSPI outperforms other methods in terms of the average number of terms and total degree in the polynomials it solves, suggesting its ability to handle more complex polynomials\.

Fig\.[14](https://arxiv.org/html/2605.15445#A9.F14)highlights that NSPI also excels in handling higher\-dimensional problems, as it successfully solves polynomials with the largest average number of variables, outperforming symbolic and LLM\-based provers\. These metrics together demonstrate NSPI’s superior scalability in solving complex and high\-dimensional polynomial inequalities compared to both symbolic and LLM\-based approaches\.

## Appendix JExtended Discussion

Neuro\-symbolic reasoning systems represent a highly valuable and promising research direction\. It is worth noting that the neuro\-symbolic approach to inequality proving proposed in this work differs fundamentally from existing neuro\-symbolic practices\. In particular, we innovatively explore the feasibility of employing large language models \(LLMs\) as*core symbolic conjecture engines*that directly provide end\-to\-end symbolic priors, thereby opening a promising new direction in which LLMs function as the central component for symbolic conjecturing\. Moreover, we extend formalized theorem proving for polynomial inequalities to challenging high\-dimensional cases with up to 10 variables, therebyextending the boundary of automated proof generation for polynomial inequalities\. To further contextualize the contributions of this work, we provide a comparative discussion with existing neuro\-symbolic reasoning approaches\.

### J\.1A New Paradigm: LLMs as Core Symbolic Conjecture Engines

In recent years, several neuro\-symbolic hybrid reasoning approaches have demonstrated encouraging progress in automated theorem proving\. However, in most existing systems, neural modules primarily serve*auxiliary*roles that guide or accelerate symbolic derivation processes by reducing the search space\.

For example, AlphaGeometry\(Trinh et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib48)\)uses an LLM to predict auxiliary constructions, while the proof is completed by a symbolic solver that enumerates derivation rules\. AIPS\(Wei et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib54)\)employs a learned value network to evaluate intermediate subgoals during symbolic proof search\. LIPS\(Li et al\.,[2025a](https://arxiv.org/html/2605.15445#bib.bib25)\)leverages an LLM to generate candidate goal\-rewriting steps and selects promising subgoals to prune the strategy space\. Similarly, IneqSearch\(Li et al\.,[2025b](https://arxiv.org/html/2605.15445#bib.bib26)\)leverages LLMs to perform inequality transformations or to select appropriate transformation rules, integrating an iterative learning mechanism\. In these systems, neural components assist decision\-making within a symbolic engine, whereas the ability of neural models to directly provide symbolic reasoning content remains relatively underexplored\.

In contrast, our work treats the LLM as a*core symbolic conjecturing engine*\. The LLM directly produces the symbolic priors required to complete a proof, in the form of SOS structure conjectures\. These conjectures are subsequently refined through Newton\-style numerical refinement and rational recovery \(Section[4\.2](https://arxiv.org/html/2605.15445#S4.SS2)\), and finally transformed into complete formal Lean proofs \(Section[4\.3](https://arxiv.org/html/2605.15445#S4.SS3)\)\. This end\-to\-end pipeline demonstrates the feasibility of a new neuro\-symbolic paradigm in which LLMs provide high\-level symbolic structure, while symbolic computation and formal verification ensure correctness\.

### J\.2Extending the Frontier of Formal Polynomial Inequality Proving

Automated formal proving of polynomial inequalities remains a challenging problem\. Although automated theorem\-proving techniques have advanced rapidly, competition\-level polynomial inequalities continue to pose significant difficulties, especially in settings involving many variables or high\-dimensional structures\.

Learning\-based approaches to formal inequality proving often face a bottleneck in the availability of high\-quality formal data\. Widely used theorem\-proving benchmarks, such as miniF2F\(Zheng et al\.,[2021](https://arxiv.org/html/2605.15445#bib.bib58)\), ProofNet\(Azerbayev et al\.,[2023](https://arxiv.org/html/2605.15445#bib.bib3)\)and Putnum\(Tsoukalas et al\.,[2024](https://arxiv.org/html/2605.15445#bib.bib49)\)contain very few polynomial inequality problems; this scarcity is particularly pronounced for high\-dimensional multivariate polynomials\. Existing neuro\-symbolic inequality proving methods also tend to focus on low\-dimensional cases with a small number of variables, and struggle to scale to more complex settings\.

The neuro\-symbolic approach proposed in this work extends Lean\-based formal polynomial inequality proving to settings involving up to ten variables, and further introduces a competition\-level benchmark covering inequalities with three to ten variables\. As demonstrated by the results in Section[5](https://arxiv.org/html/2605.15445#S5), our method consistently outperforms all LLM\-based and symbolic baselines on this challenging benchmark, with particularly strong performance in cases involving a larger number of variables\. These results indicate that the proposed approach significantly expands the frontier of formal polynomial inequality theorem proving\.

## Appendix KMore Examples

Here we provide additional examples that were successfully solved exclusively by our proposed NSPI method among all baseline approaches\.

NSPI Achieves Solution While Baseline Methods Fail\(1\)Polynomial:
8​x16​x22​x32​x42\+6​x14​x52​x6​x2​x3​x4\+8​x13​x76​x2​x3​x4\+8​x13​x6​x23​x32​x4\+6​x13​x2​x3​x43​x82​x92\+9​x12​x54​x62−6​x1​x76​x52​x6−4​x1​x52​x62​x22​x3\+10​x1​x52​x6​x42​x82​x92\+9​x712\+2​x76​x6​x22​x3\+4​x76​x42​x82​x92\+9​x62​x24​x32−8​x6​x22​x3​x42​x82​x92\+6​x44​x84​x948x\_\{1\}^\{6\}x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{4\}^\{2\}\+6x\_\{1\}^\{4\}x\_\{5\}^\{2\}x\_\{6\}x\_\{2\}x\_\{3\}x\_\{4\}\+8x\_\{1\}^\{3\}x\_\{7\}^\{6\}x\_\{2\}x\_\{3\}x\_\{4\}\+8x\_\{1\}^\{3\}x\_\{6\}x\_\{2\}^\{3\}x\_\{3\}^\{2\}x\_\{4\}\+6x\_\{1\}^\{3\}x\_\{2\}x\_\{3\}x\_\{4\}^\{3\}x\_\{8\}^\{2\}x\_\{9\}^\{2\}\+9x\_\{1\}^\{2\}x\_\{5\}^\{4\}x\_\{6\}^\{2\}\-6x\_\{1\}x\_\{7\}^\{6\}x\_\{5\}^\{2\}x\_\{6\}\-4x\_\{1\}x\_\{5\}^\{2\}x\_\{6\}^\{2\}x\_\{2\}^\{2\}x\_\{3\}\+10x\_\{1\}x\_\{5\}^\{2\}x\_\{6\}x\_\{4\}^\{2\}x\_\{8\}^\{2\}x\_\{9\}^\{2\}\+9x\_\{7\}^\{12\}\+2x\_\{7\}^\{6\}x\_\{6\}x\_\{2\}^\{2\}x\_\{3\}\+4x\_\{7\}^\{6\}x\_\{4\}^\{2\}x\_\{8\}^\{2\}x\_\{9\}^\{2\}\+9x\_\{6\}^\{2\}x\_\{2\}^\{4\}x\_\{3\}^\{2\}\-8x\_\{6\}x\_\{2\}^\{2\}x\_\{3\}x\_\{4\}^\{2\}x\_\{8\}^\{2\}x\_\{9\}^\{2\}\+6x\_\{4\}^\{4\}x\_\{8\}^\{4\}x\_\{9\}^\{4\}Lean Proof:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKdGhlb3JlbSBmMSAoeDEgeDIgeDMgeDQgeDUgeDYgeDcgeDggeDkgSSA6IFJlYWwpIChoMSA6SSA9IDgqeDFeNip4Ml4yKngzXjIqeDReMiArIDYqeDFeNCp4Mip4Myp4NCp4NV4yKng2ICsgOCp4MV4zKngyXjMqeDNeMip4NCp4NiArIDYqeDFeMyp4Mip4Myp4NF4zKng4XjIqeDleMiArIDgqeDFeMyp4Mip4Myp4NCp4N142ICsgOSp4MV4yKng1XjQqeDZeMiAtIDQqeDEqeDJeMip4Myp4NV4yKng2XjIgKyAxMCp4MSp4NF4yKng1XjIqeDYqeDheMip4OV4yIC0gNip4MSp4NV4yKng2Kng3XjYgKyA5KngyXjQqeDNeMip4Nl4yIC0gOCp4Ml4yKngzKng0XjIqeDYqeDheMip4OV4yICsgMip4Ml4yKngzKng2Kng3XjYgKyA2Kng0XjQqeDheNCp4OV40ICsgNCp4NF4yKng3XjYqeDheMip4OV4yICsgOSp4N14xMikgOiBJID49IDAgOj0gYnkKICBsZXQgdGVybXMgOiBMaXN0IChSZWFsICRcdGltZXMkIFJlYWwpIDo9IFsgKDAsIDEpLCAoMCwgeDJeMip4MyksICg5LCB4MV4zKngyKngzKng0LzMgKyB4MSp4NV4yKng2IC0gMip4Ml4yKngzKng2LzkgKyA1Kng0XjIqeDheMip4OV4yLzkgLSB4N142LzMpLCAoNzcvOSwgNip4MV4zKngyKngzKng0LzExICsgeDJeMip4Myp4NiAtIDI2Kng0XjIqeDheMip4OV4yLzc3ICsgMyp4N142Lzc3KSwgKDE3My83NywgMjI0KngxXjMqeDIqeDMqeDQvMTczICsgeDReMip4OF4yKng5XjIgKyAyOTEqeDdeNi8xNzMpLCAoMjgyLzE3MywgLTEzKngxXjMqeDIqeDMqeDQvMjgyICsgeDdeNiksICgwLCB4M14yKng0XjQpLCAoMTkzLzI4MiwgeDFeMyp4Mip4Myp4NCksICgwLCB4NF4yKng2Kng4XjIqeDleMiksICgwLCB4Nip4N142KSBdCiAgaGF2ZSA6IEkgPSAodGVybXMubWFwIChmdW4gKHAsIGspID0+IHAgKiBrXjIpKS5zdW0gOj0gYnkKICAgIHVuZm9sZCB0ZXJtcwogICAgc2ltcCBvbmx5IFtMaXN0Lm1hcF9jb25zLCBMaXN0Lm1hcF9uaWwsIExpc3Quc3VtX2NvbnMsIExpc3Quc3VtX25pbF0KICAgIGxpbmVhcl9jb21iaW5hdGlvbiBoMQogIHJ3IFt0aGlzXQogIHVuZm9sZCB0ZXJtcwogIHNpbXAgb25seSBbTGlzdC5tYXBfY29ucywgTGlzdC5tYXBfbmlsLCBMaXN0LnN1bV9jb25zLCBMaXN0LnN1bV9uaWxdCiAgcG9zaXRpdml0eQ==)importMathlibtheoremf1\(x1x2x3x4x5x6x7x8x9I:Real\)\(h1:I=8\*x1^6\*x2^2\*x3^2\*x4^2\+6\*x1^4\*x2\*x3\*x4\*x5^2\*x6\+8\*x1^3\*x2^3\*x3^2\*x4\*x6\+6\*x1^3\*x2\*x3\*x4^3\*x8^2\*x9^2\+8\*x1^3\*x2\*x3\*x4\*x7^6\+9\*x1^2\*x5^4\*x6^2\-4\*x1\*x2^2\*x3\*x5^2\*x6^2\+10\*x1\*x4^2\*x5^2\*x6\*x8^2\*x9^2\-6\*x1\*x5^2\*x6\*x7^6\+9\*x2^4\*x3^2\*x6^2\-8\*x2^2\*x3\*x4^2\*x6\*x8^2\*x9^2\+2\*x2^2\*x3\*x6\*x7^6\+6\*x4^4\*x8^4\*x9^4\+4\*x4^2\*x7^6\*x8^2\*x9^2\+9\*x7^12\):I\>=0:=byletterms:List\(Real×\\timesReal\):=\[\(0,1\),\(0,x2^2\*x3\),\(9,x1^3\*x2\*x3\*x4/3\+x1\*x5^2\*x6\-2\*x2^2\*x3\*x6/9\+5\*x4^2\*x8^2\*x9^2/9\-x7^6/3\),\(77/9,6\*x1^3\*x2\*x3\*x4/11\+x2^2\*x3\*x6\-26\*x4^2\*x8^2\*x9^2/77\+3\*x7^6/77\),\(173/77,224\*x1^3\*x2\*x3\*x4/173\+x4^2\*x8^2\*x9^2\+291\*x7^6/173\),\(282/173,\-13\*x1^3\*x2\*x3\*x4/282\+x7^6\),\(0,x3^2\*x4^4\),\(193/282,x1^3\*x2\*x3\*x4\),\(0,x4^2\*x6\*x8^2\*x9^2\),\(0,x6\*x7^6\)\]have:I=\(terms\.map\(fun\(p,k\)=\>p\*k^2\)\)\.sum:=byunfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]linear\_combinationh1rw\[this\]unfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]positivityNSPI Achieves Solution While Baseline Methods Fail\(2\)Polynomial:
7​x12​x22​x32​x42−2​x1​x52​x2​x3​x4​x6​x7​x8−4​x1​x5​x2​x3​x4​x6​x94−6​x1​x2​x3​x4​x65​x8−10​x1​x2​x3​x4​x6​x73​x82\+8​x54​x62​x72​x82−4​x52​x62​x74​x83\+8​x52​x62​x98−4​x5​x66​x8​x94−2​x5​x62​x73​x82​x94\+5​x610​x82\+6​x66​x73​x83\+6​x62​x76​x847x\_\{1\}^\{2\}x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{4\}^\{2\}\-2x\_\{1\}x\_\{5\}^\{2\}x\_\{2\}x\_\{3\}x\_\{4\}x\_\{6\}x\_\{7\}x\_\{8\}\-4x\_\{1\}x\_\{5\}x\_\{2\}x\_\{3\}x\_\{4\}x\_\{6\}x\_\{9\}^\{4\}\-6x\_\{1\}x\_\{2\}x\_\{3\}x\_\{4\}x\_\{6\}^\{5\}x\_\{8\}\-10x\_\{1\}x\_\{2\}x\_\{3\}x\_\{4\}x\_\{6\}x\_\{7\}^\{3\}x\_\{8\}^\{2\}\+8x\_\{5\}^\{4\}x\_\{6\}^\{2\}x\_\{7\}^\{2\}x\_\{8\}^\{2\}\-4x\_\{5\}^\{2\}x\_\{6\}^\{2\}x\_\{7\}^\{4\}x\_\{8\}^\{3\}\+8x\_\{5\}^\{2\}x\_\{6\}^\{2\}x\_\{9\}^\{8\}\-4x\_\{5\}x\_\{6\}^\{6\}x\_\{8\}x\_\{9\}^\{4\}\-2x\_\{5\}x\_\{6\}^\{2\}x\_\{7\}^\{3\}x\_\{8\}^\{2\}x\_\{9\}^\{4\}\+5x\_\{6\}^\{10\}x\_\{8\}^\{2\}\+6x\_\{6\}^\{6\}x\_\{7\}^\{3\}x\_\{8\}^\{3\}\+6x\_\{6\}^\{2\}x\_\{7\}^\{6\}x\_\{8\}^\{4\}Lean Proof:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKdGhlb3JlbSBmMSAoeDEgeDIgeDMgeDQgeDUgeDYgeDcgeDggeDkgSSA6IFJlYWwpIChoMSA6SSA9IDcqeDFeMip4Ml4yKngzXjIqeDReMiAtIDIqeDEqeDIqeDMqeDQqeDVeMip4Nip4Nyp4OCAtIDQqeDEqeDIqeDMqeDQqeDUqeDYqeDleNCAtIDYqeDEqeDIqeDMqeDQqeDZeNSp4OCAtIDEwKngxKngyKngzKng0Kng2Kng3XjMqeDheMiArIDgqeDVeNCp4Nl4yKng3XjIqeDheMiAtIDQqeDVeMip4Nl4yKng3XjQqeDheMyArIDgqeDVeMip4Nl4yKng5XjggLSA0Kng1Kng2XjYqeDgqeDleNCAtIDIqeDUqeDZeMip4N14zKng4XjIqeDleNCArIDUqeDZeMTAqeDheMiArIDYqeDZeNip4N14zKng4XjMgKyA2Kng2XjIqeDdeNip4OF40KSA6IEkgPj0gMCA6PSBieQogIGxldCB0ZXJtcyA6IExpc3QgKFJlYWwgJFx0aW1lcyQgUmVhbCkgOj0gWyAoMCwgMSksICgwLCB4Myp4NF4yKSwgKDAsIHg0XjMqeDYpLCAoNywgeDEqeDIqeDMqeDQgLSB4NV4yKng2Kng3Kng4LzcgLSAyKng1Kng2Kng5XjQvNyAtIDMqeDZeNSp4OC83IC0gNSp4Nip4N14zKng4XjIvNyksICg1NS83LCB4NV4yKng2Kng3Kng4IC0gMip4NSp4Nip4OV40LzU1IC0gMyp4Nl41Kng4LzU1IC0gMTkqeDYqeDdeMyp4OF4yLzU1KSwgKDAsIHgzXjIqeDQqeDYqeDcpLCAoNDA4LzU1LCB4NSp4Nip4OV40IC0gNzkqeDZeNSp4OC8yMDQgLSAxMzkqeDYqeDdeMyp4OF4yLzQwOCksICgyNTcvNDA4LCAtMTEwKng2XjUqeDgvMjU3ICsgeDYqeDdeMyp4OF4yKSwgKDYzMy8yNTcsIHg2XjUqeDgpLCAoMCwgeDQqeDZeNSksICgwLCB4M140Kng1Kng2KSwgKDAsIHg1XjIqeDZeMip4N140Kng4XjMpLCAoMCwgeDZeNip4N14zKng4XjMpIF0KICBoYXZlIDogSSA9ICh0ZXJtcy5tYXAgKGZ1biAocCwgaykgPT4gcCAqIGteMikpLnN1bSA6PSBieQogICAgdW5mb2xkIHRlcm1zCiAgICBzaW1wIG9ubHkgW0xpc3QubWFwX2NvbnMsIExpc3QubWFwX25pbCwgTGlzdC5zdW1fY29ucywgTGlzdC5zdW1fbmlsXQogICAgbGluZWFyX2NvbWJpbmF0aW9uIGgxCiAgcncgW3RoaXNdCiAgdW5mb2xkIHRlcm1zCiAgc2ltcCBvbmx5IFtMaXN0Lm1hcF9jb25zLCBMaXN0Lm1hcF9uaWwsIExpc3Quc3VtX2NvbnMsIExpc3Quc3VtX25pbF0KICBwb3NpdGl2aXR5)importMathlibtheoremf1\(x1x2x3x4x5x6x7x8x9I:Real\)\(h1:I=7\*x1^2\*x2^2\*x3^2\*x4^2\-2\*x1\*x2\*x3\*x4\*x5^2\*x6\*x7\*x8\-4\*x1\*x2\*x3\*x4\*x5\*x6\*x9^4\-6\*x1\*x2\*x3\*x4\*x6^5\*x8\-10\*x1\*x2\*x3\*x4\*x6\*x7^3\*x8^2\+8\*x5^4\*x6^2\*x7^2\*x8^2\-4\*x5^2\*x6^2\*x7^4\*x8^3\+8\*x5^2\*x6^2\*x9^8\-4\*x5\*x6^6\*x8\*x9^4\-2\*x5\*x6^2\*x7^3\*x8^2\*x9^4\+5\*x6^10\*x8^2\+6\*x6^6\*x7^3\*x8^3\+6\*x6^2\*x7^6\*x8^4\):I\>=0:=byletterms:List\(Real×\\timesReal\):=\[\(0,1\),\(0,x3\*x4^2\),\(0,x4^3\*x6\),\(7,x1\*x2\*x3\*x4\-x5^2\*x6\*x7\*x8/7\-2\*x5\*x6\*x9^4/7\-3\*x6^5\*x8/7\-5\*x6\*x7^3\*x8^2/7\),\(55/7,x5^2\*x6\*x7\*x8\-2\*x5\*x6\*x9^4/55\-3\*x6^5\*x8/55\-19\*x6\*x7^3\*x8^2/55\),\(0,x3^2\*x4\*x6\*x7\),\(408/55,x5\*x6\*x9^4\-79\*x6^5\*x8/204\-139\*x6\*x7^3\*x8^2/408\),\(257/408,\-110\*x6^5\*x8/257\+x6\*x7^3\*x8^2\),\(633/257,x6^5\*x8\),\(0,x4\*x6^5\),\(0,x3^4\*x5\*x6\),\(0,x5^2\*x6^2\*x7^4\*x8^3\),\(0,x6^6\*x7^3\*x8^3\)\]have:I=\(terms\.map\(fun\(p,k\)=\>p\*k^2\)\)\.sum:=byunfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]linear\_combinationh1rw\[this\]unfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]positivityNSPI Achieves Solution While Baseline Methods Fail\(3\)Polynomial:
11​x14​x24​x32−4​x13​x23​x3−12​x13​x22​x33​x5​x6−6​x13​x22​x32​x55​x7\+2​x12​x23​x33​x5−2​x12​x23​x3​x4−8​x12​x23​x3​x5​x7−2​x12​x22​x3​x74\+10​x12​x22\+4​x12​x2​x32​x5​x6\+4​x12​x2​x3​x55​x7\+12​x12​x34​x52​x62\+2​x12​x33​x56​x6​x7\+12​x12​x32​x510​x72−12​x1​x22​x32​x5−4​x1​x22​x4−2​x1​x22​x5​x7−6​x1​x2​x34​x52​x6\+2​x1​x2​x33​x56​x7\+8​x1​x2​x32​x4​x5​x6\+2​x1​x2​x32​x52​x6​x7\+4​x1​x2​x3​x4​x55​x7−6​x1​x2​x3​x56​x72−14​x1​x2​x74\+10​x1​x32​x5​x6​x74\+2​x1​x3​x55​x75\+13​x22​x34​x52\+4​x22​x32​x4​x5−12​x22​x32​x52​x7\+10​x22​x42\+14​x22​x52​x72\+8​x2​x32​x5​x74\+2​x2​x4​x74\+4​x2​x5​x75\+12​x7811x\_\{1\}^\{4\}x\_\{2\}^\{4\}x\_\{3\}^\{2\}\-4x\_\{1\}^\{3\}x\_\{2\}^\{3\}x\_\{3\}\-12x\_\{1\}^\{3\}x\_\{2\}^\{2\}x\_\{3\}^\{3\}x\_\{5\}x\_\{6\}\-6x\_\{1\}^\{3\}x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{5\}^\{5\}x\_\{7\}\+2x\_\{1\}^\{2\}x\_\{2\}^\{3\}x\_\{3\}^\{3\}x\_\{5\}\-2x\_\{1\}^\{2\}x\_\{2\}^\{3\}x\_\{3\}x\_\{4\}\-8x\_\{1\}^\{2\}x\_\{2\}^\{3\}x\_\{3\}x\_\{5\}x\_\{7\}\-2x\_\{1\}^\{2\}x\_\{2\}^\{2\}x\_\{3\}x\_\{7\}^\{4\}\+10x\_\{1\}^\{2\}x\_\{2\}^\{2\}\+4x\_\{1\}^\{2\}x\_\{2\}x\_\{3\}^\{2\}x\_\{5\}x\_\{6\}\+4x\_\{1\}^\{2\}x\_\{2\}x\_\{3\}x\_\{5\}^\{5\}x\_\{7\}\+12x\_\{1\}^\{2\}x\_\{3\}^\{4\}x\_\{5\}^\{2\}x\_\{6\}^\{2\}\+2x\_\{1\}^\{2\}x\_\{3\}^\{3\}x\_\{5\}^\{6\}x\_\{6\}x\_\{7\}\+12x\_\{1\}^\{2\}x\_\{3\}^\{2\}x\_\{5\}^\{10\}x\_\{7\}^\{2\}\-12x\_\{1\}x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{5\}\-4x\_\{1\}x\_\{2\}^\{2\}x\_\{4\}\-2x\_\{1\}x\_\{2\}^\{2\}x\_\{5\}x\_\{7\}\-6x\_\{1\}x\_\{2\}x\_\{3\}^\{4\}x\_\{5\}^\{2\}x\_\{6\}\+2x\_\{1\}x\_\{2\}x\_\{3\}^\{3\}x\_\{5\}^\{6\}x\_\{7\}\+8x\_\{1\}x\_\{2\}x\_\{3\}^\{2\}x\_\{4\}x\_\{5\}x\_\{6\}\+2x\_\{1\}x\_\{2\}x\_\{3\}^\{2\}x\_\{5\}^\{2\}x\_\{6\}x\_\{7\}\+4x\_\{1\}x\_\{2\}x\_\{3\}x\_\{4\}x\_\{5\}^\{5\}x\_\{7\}\-6x\_\{1\}x\_\{2\}x\_\{3\}x\_\{5\}^\{6\}x\_\{7\}^\{2\}\-14x\_\{1\}x\_\{2\}x\_\{7\}^\{4\}\+10x\_\{1\}x\_\{3\}^\{2\}x\_\{5\}x\_\{6\}x\_\{7\}^\{4\}\+2x\_\{1\}x\_\{3\}x\_\{5\}^\{5\}x\_\{7\}^\{5\}\+13x\_\{2\}^\{2\}x\_\{3\}^\{4\}x\_\{5\}^\{2\}\+4x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{4\}x\_\{5\}\-12x\_\{2\}^\{2\}x\_\{3\}^\{2\}x\_\{5\}^\{2\}x\_\{7\}\+10x\_\{2\}^\{2\}x\_\{4\}^\{2\}\+14x\_\{2\}^\{2\}x\_\{5\}^\{2\}x\_\{7\}^\{2\}\+8x\_\{2\}x\_\{3\}^\{2\}x\_\{5\}x\_\{7\}^\{4\}\+2x\_\{2\}x\_\{4\}x\_\{7\}^\{4\}\+4x\_\{2\}x\_\{5\}x\_\{7\}^\{5\}\+12x\_\{7\}^\{8\}Lean Proof:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKdGhlb3JlbSBmMSAoeDEgeDIgeDMgeDQgeDUgeDYgeDcgSSA6IFJlYWwpIChoMSA6SSA9IDExKngxXjQqeDJeNCp4M14yIC0gNCp4MV4zKngyXjMqeDMgLSAxMip4MV4zKngyXjIqeDNeMyp4NSp4NiAtIDYqeDFeMyp4Ml4yKngzXjIqeDVeNSp4NyArIDIqeDFeMip4Ml4zKngzXjMqeDUgLSAyKngxXjIqeDJeMyp4Myp4NCAtIDgqeDFeMip4Ml4zKngzKng1Kng3IC0gMip4MV4yKngyXjIqeDMqeDdeNCArIDEwKngxXjIqeDJeMiArIDQqeDFeMip4Mip4M14yKng1Kng2ICsgNCp4MV4yKngyKngzKng1XjUqeDcgKyAxMip4MV4yKngzXjQqeDVeMip4Nl4yICsgMip4MV4yKngzXjMqeDVeNip4Nip4NyArIDEyKngxXjIqeDNeMip4NV4xMCp4N14yIC0gMTIqeDEqeDJeMip4M14yKng1IC0gNCp4MSp4Ml4yKng0IC0gMip4MSp4Ml4yKng1Kng3IC0gNip4MSp4Mip4M140Kng1XjIqeDYgKyAyKngxKngyKngzXjMqeDVeNip4NyArIDgqeDEqeDIqeDNeMip4NCp4NSp4NiArIDIqeDEqeDIqeDNeMip4NV4yKng2Kng3ICsgNCp4MSp4Mip4Myp4NCp4NV41Kng3IC0gNip4MSp4Mip4Myp4NV42Kng3XjIgLSAxNCp4MSp4Mip4N140ICsgMTAqeDEqeDNeMip4NSp4Nip4N140ICsgMip4MSp4Myp4NV41Kng3XjUgKyAxMyp4Ml4yKngzXjQqeDVeMiArIDQqeDJeMip4M14yKng0Kng1IC0gMTIqeDJeMip4M14yKng1XjIqeDcgKyAxMCp4Ml4yKng0XjIgKyAxNCp4Ml4yKng1XjIqeDdeMiArIDgqeDIqeDNeMip4NSp4N140ICsgMip4Mip4NCp4N140ICsgNCp4Mip4NSp4N141ICsgMTIqeDdeOCkgOiBJID49IDAgOj0gYnkKICBsZXQgdGVybXMgOiBMaXN0IChSZWFsICRcdGltZXMkIFJlYWwpIDo9IFsgKDAsIDEpLCAoMTAsIC14MV4yKngyXjIqeDMvMTAgLSB4MSp4Mi81ICsgMip4MSp4M14yKng1Kng2LzUgKyB4MSp4Myp4NV41Kng3LzUgKyB4Mip4M14yKng1LzUgKyB4Mip4NCArIHg3XjQvMTApLCAoNDgvNSwgLTExKngxXjIqeDJeMip4My80OCArIHgxKngyICsgNyp4MSp4M14yKng1Kng2LzI0ICsgeDEqeDMqeDVeNSp4Ny80IC0gNyp4Mip4M14yKng1LzEyIC0gNSp4Mip4NSp4Ny80OCAtIDE3Kng3XjQvMjQpLCAoNjY3LzQ4LCAtNyp4MV4yKngyXjIqeDMvMjMgKyA2Mip4MSp4M14yKng1Kng2LzY2NyAtIDEzMip4MSp4Myp4NV41Kng3LzY2NyAtIDMxNip4Mip4M14yKng1LzY2NyArIHgyKng1Kng3ICsgNjIqeDdeNC82NjcpLCAoMCwgeDIqeDMqeDUpLCAoOTI4OS8xMzM0LCAtMjc1NSp4MV4yKngyXjIqeDMvOTI4OSArIDg2MjIqeDEqeDNeMip4NSp4Ni85Mjg5ICsgMzY3Nip4MSp4Myp4NV41Kng3LzkyODkgKyA1OTQqeDIqeDNeMip4NS85Mjg5ICsgeDdeNCksICg1NzQ2MS85Mjg5LCAtMTgxNTkqeDFeMip4Ml4yKngzLzU3NDYxIC0gMTgyODEqeDEqeDNeMip4NSp4Ni81NzQ2MSArIDQ4MzkqeDEqeDMqeDVeNSp4Ny81NzQ2MSArIHgyKngzXjIqeDUpLCAoMCwgeDNeNCksICgxNjMwNzMvNTc0NjEsIC0xODc5MTEqeDFeMip4Ml4yKngzLzE2MzA3MyArIHgxKngzXjIqeDUqeDYgLSAxNTE0OTAqeDEqeDMqeDVeNSp4Ny8xNjMwNzMpLCAoNjcwMjM5LzE2MzA3MywgeDFeMip4Ml4yKngzIC0gODM4Njg0KngxKngzKng1XjUqeDcvNjcwMjM5KSwgKDAsIHgxKngzKng1XjUpLCAoMjkyNzExLzY3MDIzOSwgeDEqeDMqeDVeNSp4NykgXQogIGhhdmUgOiBJID0gKHRlcm1zLm1hcCAoZnVuIChwLCBrKSA9PiBwICoga14yKSkuc3VtIDo9IGJ5CiAgICB1bmZvbGQgdGVybXMKICAgIHNpbXAgb25seSBbTGlzdC5tYXBfY29ucywgTGlzdC5tYXBfbmlsLCBMaXN0LnN1bV9jb25zLCBMaXN0LnN1bV9uaWxdCiAgICBsaW5lYXJfY29tYmluYXRpb24gaDEKICBydyBbdGhpc10KICB1bmZvbGQgdGVybXMKICBzaW1wIG9ubHkgW0xpc3QubWFwX2NvbnMsIExpc3QubWFwX25pbCwgTGlzdC5zdW1fY29ucywgTGlzdC5zdW1fbmlsXQogIHBvc2l0aXZpdHk=)importMathlibtheoremf1\(x1x2x3x4x5x6x7I:Real\)\(h1:I=11\*x1^4\*x2^4\*x3^2\-4\*x1^3\*x2^3\*x3\-12\*x1^3\*x2^2\*x3^3\*x5\*x6\-6\*x1^3\*x2^2\*x3^2\*x5^5\*x7\+2\*x1^2\*x2^3\*x3^3\*x5\-2\*x1^2\*x2^3\*x3\*x4\-8\*x1^2\*x2^3\*x3\*x5\*x7\-2\*x1^2\*x2^2\*x3\*x7^4\+10\*x1^2\*x2^2\+4\*x1^2\*x2\*x3^2\*x5\*x6\+4\*x1^2\*x2\*x3\*x5^5\*x7\+12\*x1^2\*x3^4\*x5^2\*x6^2\+2\*x1^2\*x3^3\*x5^6\*x6\*x7\+12\*x1^2\*x3^2\*x5^10\*x7^2\-12\*x1\*x2^2\*x3^2\*x5\-4\*x1\*x2^2\*x4\-2\*x1\*x2^2\*x5\*x7\-6\*x1\*x2\*x3^4\*x5^2\*x6\+2\*x1\*x2\*x3^3\*x5^6\*x7\+8\*x1\*x2\*x3^2\*x4\*x5\*x6\+2\*x1\*x2\*x3^2\*x5^2\*x6\*x7\+4\*x1\*x2\*x3\*x4\*x5^5\*x7\-6\*x1\*x2\*x3\*x5^6\*x7^2\-14\*x1\*x2\*x7^4\+10\*x1\*x3^2\*x5\*x6\*x7^4\+2\*x1\*x3\*x5^5\*x7^5\+13\*x2^2\*x3^4\*x5^2\+4\*x2^2\*x3^2\*x4\*x5\-12\*x2^2\*x3^2\*x5^2\*x7\+10\*x2^2\*x4^2\+14\*x2^2\*x5^2\*x7^2\+8\*x2\*x3^2\*x5\*x7^4\+2\*x2\*x4\*x7^4\+4\*x2\*x5\*x7^5\+12\*x7^8\):I\>=0:=byletterms:List\(Real×\\timesReal\):=\[\(0,1\),\(10,\-x1^2\*x2^2\*x3/10\-x1\*x2/5\+2\*x1\*x3^2\*x5\*x6/5\+x1\*x3\*x5^5\*x7/5\+x2\*x3^2\*x5/5\+x2\*x4\+x7^4/10\),\(48/5,\-11\*x1^2\*x2^2\*x3/48\+x1\*x2\+7\*x1\*x3^2\*x5\*x6/24\+x1\*x3\*x5^5\*x7/4\-7\*x2\*x3^2\*x5/12\-5\*x2\*x5\*x7/48\-17\*x7^4/24\),\(667/48,\-7\*x1^2\*x2^2\*x3/23\+62\*x1\*x3^2\*x5\*x6/667\-132\*x1\*x3\*x5^5\*x7/667\-316\*x2\*x3^2\*x5/667\+x2\*x5\*x7\+62\*x7^4/667\),\(0,x2\*x3\*x5\),\(9289/1334,\-2755\*x1^2\*x2^2\*x3/9289\+8622\*x1\*x3^2\*x5\*x6/9289\+3676\*x1\*x3\*x5^5\*x7/9289\+594\*x2\*x3^2\*x5/9289\+x7^4\),\(57461/9289,\-18159\*x1^2\*x2^2\*x3/57461\-18281\*x1\*x3^2\*x5\*x6/57461\+4839\*x1\*x3\*x5^5\*x7/57461\+x2\*x3^2\*x5\),\(0,x3^4\),\(163073/57461,\-187911\*x1^2\*x2^2\*x3/163073\+x1\*x3^2\*x5\*x6\-151490\*x1\*x3\*x5^5\*x7/163073\),\(670239/163073,x1^2\*x2^2\*x3\-838684\*x1\*x3\*x5^5\*x7/670239\),\(0,x1\*x3\*x5^5\),\(292711/670239,x1\*x3\*x5^5\*x7\)\]have:I=\(terms\.map\(fun\(p,k\)=\>p\*k^2\)\)\.sum:=byunfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]linear\_combinationh1rw\[this\]unfoldtermssimponly\[List\.map\_cons,List\.map\_nil,List\.sum\_cons,List\.sum\_nil\]positivity