🤖 AI

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

This paper introduces NSPI, a neuro-symbolic framework that leverages large language models to propose approximate Sum-of-Squares conjectures and symbolic computation to refine them into exact, machine-checked Lean proofs, thereby achieving scalable automated proving of polynomial inequalities with up to 10 variables.

Original authors: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Published 2026-05-18

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to prove that a complex, multi-layered cake is always "sweet enough" (mathematically, non-negative) no matter how you slice it or change the ingredients. In the world of mathematics, this is called proving a polynomial inequality.

For a long time, mathematicians have had two main ways to do this, but both have had major flaws:

The "Pure Logic" Method (Symbolic): This is like trying to solve the cake problem by writing out every single chemical reaction of the ingredients on a chalkboard. It's perfectly accurate, but if the cake has too many ingredients (variables), the chalkboard fills up instantly, and the method crashes. It's too slow and messy for big problems.
The "AI Guessing" Method (LLMs): This is like asking a very smart, creative chef to guess the recipe. The chef is fast and good at small cakes, but when the cake gets huge and complicated, the chef starts hallucinating ingredients that don't exist or making math errors. They can't prove their answer is 100% true.

This paper introduces a new team called NSPI (Neuro-Symbolic Polynomial Inequality proving). Think of NSPI as a perfect partnership between a creative chef and a rigorous quality inspector.

Here is how their "assembly line" works, step-by-step:

Step 1: The Creative Chef (The LLM)

First, the team asks a Large Language Model (the "Chef") to look at a difficult math problem. The Chef doesn't try to do the hard math immediately. Instead, it uses its creativity to guess a structure.

The Analogy: Imagine the Chef says, "I bet this cake is made of three specific layers of sugar cubes stacked together."
In math terms, the LLM guesses a Sum-of-Squares (SOS) decomposition. It suggests, "This complicated expression is probably just the sum of a few simpler things squared."
Crucial Point: The Chef's guess is usually an approximation. It's close, but it might have tiny decimal errors (like saying a sugar cube weighs 1.0000001 grams instead of exactly 1).

Step 2: The Quality Inspector (Symbolic Correction)

The Chef's guess is passed to the "Quality Inspector," which is a powerful computer algebra system.

The Analogy: The Inspector takes the Chef's rough sketch and uses a microscope to fix the tiny errors. It uses a technique called Newton's Method (a mathematical way to zoom in on the exact answer) and Rational Recovery (turning messy decimals into clean, exact fractions).
If the Chef guessed the layers were "roughly" 1.5, 2.3, and 0.7, the Inspector calculates the exact numbers: 3/2, 23/10, and 7/10.
Now, the guess has been turned into a perfect, exact mathematical certificate.

Step 3: The Courtroom Judge (Lean Verification)

Finally, the team takes this exact certificate to a "Judge" named Lean.

The Analogy: Lean is a strict, unblinking judge who checks every single step of the Inspector's work. It doesn't care about "feeling" or "guessing." It only accepts proofs that are logically airtight.
Because the Inspector provided an exact certificate, the Judge can easily verify: "Yes, if you square these exact numbers and add them up, you get the original cake. And since squares are always positive, the cake is always sweet."
The Judge then issues a machine-checked proof that is 100% guaranteed to be correct.

Why is this a big deal?

The paper tested this team on 522 very hard math problems, some with up to 10 different variables (ingredients).

The Old Logic Methods gave up when the problems got too big (too many ingredients).
The Old AI Methods got confused and made mistakes on the big problems.
The NSPI Team succeeded where others failed. They could solve problems with 10 variables that no other method could touch.

The Bottom Line

The paper claims that by letting an AI guess the shape of the solution and then using math tools to fix the details and a computer to verify the truth, they have built a system that can solve complex inequality problems faster and more reliably than ever before. They didn't just guess; they built a bridge from a "good guess" to a "proven fact."

What they did NOT claim:

They did not say this will cure diseases or predict the stock market.
They did not claim this works for every type of math problem, only for proving that certain polynomial expressions are always positive.
They did not claim this replaces human mathematicians entirely, but rather automates a very specific, difficult type of reasoning.

Technical Summary: From LLM-Generated Conjectures to Lean Formalizations

Problem Statement

Automated proving of polynomial inequalities is a fundamental challenge in mathematical reasoning, particularly for high-dimensional and multivariate cases. Existing approaches face significant scalability limitations:

Purely Symbolic Methods: While providing strong guarantees, methods based on Sum-of-Squares (SOS) decomposition and Semidefinite Programming (SDP) suffer from combinatorial explosion and rapid growth in intermediate expressions as the number of variables or degree increases. They often fail to produce structured, human-readable proofs.
Purely LLM-Based Methods: Large Language Models (LLMs) integrated with proof assistants (e.g., Lean, Isabelle) have shown promise but are limited by the scarcity of high-quality formalized training data. They struggle with complex algebraic inequalities, particularly those exceeding 5 variables, and often lack the ability to generate rigorous, machine-checkable certificates.

The core challenge is to bridge the gap between heuristic discovery and rigorous formal verification, enabling automated proving of unconstrained polynomial inequalities in high-dimensional settings (up to 10 variables) with machine-checked correctness.

Methodology: NSPI Framework

The authors propose NSPI (Neuro-Symbolic SOS-based Polynomial Inequality Proving), a framework that integrates the complementary strengths of LLMs and symbolic computation into an end-to-end pipeline. The process consists of three main stages:

1. Neural Conjecture (LLM-Guided SOS Generation)

Instead of using LLMs merely for search guidance, NSPI elevates them to primary conjecture generators.

Data Construction: The authors construct a large-scale dataset of non-negative polynomial–SOS pairs using two novel strategies:
- Computation-Driven: Generating Gram matrices via spectral shifting or LMI optimization to ensure positive semi-definiteness (PSD) with controlled coefficients.
- Structure-Driven: Exploiting algebraic structures like diagonally dominant (dd) and scaled diagonally dominant (sdd) matrices, which guarantee PSD properties by design.
Training: A two-stage training scheme is employed:
- Cold Start: Supervised Fine-Tuning (SFT) on over one million synthetic polynomial-SOS pairs to establish foundational structural reasoning.
- Progressive Reinforcement Learning: Curriculum-based Group Relative Policy Optimization (GRPO) is applied to challenging instances (increasing variable counts from 3–5 to 9–10). The reward function combines accuracy (numerical fidelity), format adherence, and algebraic structure penalties to ensure the LLM generates plausible SOS structures.
Output: The LLM proposes an approximate SOS decomposition (a sum of squared terms) for a given polynomial.

2. Symbolic Correction (Exact Rational Recovery)

To transform the LLM's approximate conjecture into a rigorous proof, a symbolic correction module refines the output:

Gauss–Newton Refinement: The approximate SOS structure is refined using Newton-type iterative methods to minimize the backward error between the conjectured sum-of-squares and the target polynomial. This yields a high-precision numerical Gram matrix.
Rational Recovery: The numerical matrix is converted into an exact rational PSD matrix. Depending on whether the solution lies in the interior or on the boundary of the PSD cone, the system employs orthogonal projection or truncated LDL $^\top$ factorization combined with simultaneous Diophantine approximation. This step ensures the resulting SOS certificate is exact and free of floating-point errors.

3. Formal Verification (Lean Proof Generation)

The exact rational SOS certificate is automatically converted into a machine-checkable Lean proof.

Proof Templates: Pre-defined Lean templates are populated with the exact SOS terms.
Verification: The Lean prover verifies two conditions:
1. Equality: The target polynomial equals the expanded SOS expression (verified via linear_combination).
2. Nonnegativity: The SOS expression is non-negative (verified via the positivity tactic, which recursively applies rules like $x^2 \ge 0$ ).

Key Contributions

Neuro-Symbolic Pipeline: The proposal of NSPI, an end-to-end framework that automates the generation of complete formal proofs for polynomial inequalities by chaining neural conjecture, symbolic correction, and formal verification.
Principled Reliability Bridge: A novel method for integrating LLM-based heuristic generation with symbolic exact certification. This transforms neural conjectures into machine-checkable proofs, enabling scalability to high-dimensional multivariate cases (up to 10 variables) without relying on massive amounts of pre-existing formalized training data.
Benchmark and Evaluation: The construction of PolyIneqBench, a challenging benchmark containing 522 inequality problems (3 to 10 variables), including real-world competition problems and synthetic high-dimensional instances. Extensive experiments demonstrate that NSPI outperforms state-of-the-art symbolic solvers (Maple, Z3), pure LLM provers (DeepSeek-Prover-V2, Goedel-Prover), and existing hybrid systems (LIPS), particularly in high-dimensional scenarios.

Experimental Results

Performance: On PolyIneqBench, NSPI achieved a pass rate of 11.7% for 10-variable problems, whereas symbolic methods (Maple, Z3) and pure LLM provers dropped to near 0% or single digits.
Efficiency: NSPI maintained the lowest average execution time among successful solvers, demonstrating a speedup of over 10x compared to several LLM-based provers.
Scalability: The progressive reinforcement learning strategy successfully shifted the model's capability boundary toward higher dimensions, with performance gains observed as the curriculum moved from 3–5 variables to 9–10 variables.
Ablation: Experiments confirmed that both the synthetic cold-start training and the curriculum-based GRPO are critical for the system's success.

Significance and Claims

The paper claims to establish a new paradigm in neuro-symbolic theorem proving where LLMs function as core symbolic conjecture engines rather than mere search guides. By treating LLMs as generators of symbolic priors (SOS structures) and relying on symbolic computation for precision and formal verification for correctness, the approach addresses the data scarcity bottleneck of pure neural methods and the scalability limits of pure symbolic methods.

The authors position NSPI as a significant extension of the frontier for automated polynomial inequality proving, successfully handling high-dimensional cases (up to 10 variables) that were previously intractable for existing automated systems. The work demonstrates that combining heuristic discovery with rigorous certification can substantially broaden the practical scope of automated mathematical reasoning.