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

• URL: http://arxiv.org/abs/2605.15445v1
• Date: Thu, 14 May 2026 22:02:31 GMT
• Title: From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
• Abstract summary: We propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for computation-inequality proving.<n>We further certify the inequality in Lean, yielding an end-to-end pipeline from discovery to machine-checked proof.
• Score: 9.397847333441417
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Influence-Guided Symbolic Regression: Scientific Discovery via LLM-Driven Equation Search with Granular Feedback [56.69850045068714]
  We introduce textitInfluence-Guided Regression (IGSR), a method that frames equation discovery as an iterative two-step process.<n>We demonstrate IGSRs effectiveness on a diverse suite of benchmarks, including LLM-SRBench, pharmacological PKPD models, an epidemiological simulation, and real-world genomic data.
  arXiv  Detail & Related papers  (2026-05-27T23:48:01Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
  We show that curriculum post-training avoids the exponential complexity bottleneck.<n>Under outcome-only reward signals, reinforcement learning finetuning achieves high accuracy with sample complexity.<n>We establish guarantees for test-time scaling, where curriculum-aware querying reduces both reward oracle calls and sampling cost from exponential to order.
  arXiv  Detail & Related papers  (2025-11-10T18:29:54Z)
• Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transformers [33.99209000786153]
  Certifying nonnegativity of quadratics is a well-known NP-hard problem.<n>A sufficient condition for nonnegativity is the Sum of 200 Squares (SOS) property.<n>We introduce the first learning Transformer-training algorithm to certify SOS criterion.
  arXiv  Detail & Related papers  (2025-10-15T11:42:38Z)
• Automated Proof of Polynomial Inequalities via Reinforcement Learning [4.246350085706678]
  This paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving inequalities.<n>We also implement a tool called APPIRL (Automated Proof of Polynomial Inequalities via Reinforcement)
  arXiv  Detail & Related papers  (2025-03-09T12:50:28Z)
• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  Large language models (LLMs) can prove mathematical theorems formally by generating proof steps within a proof system.<n>We introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods.<n>We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions.
  arXiv  Detail & Related papers  (2025-02-19T15:54:21Z)
• VLWE: Variety-based Learning with Errors for Vector Encryption through Algebraic Geometry [1.3824176915623292]
  Lattice-based cryptography is a foundation for post-quantum security.<n>This work introduces Variety-LWE (VLWE), a new structured lattice problem based on algebraic geometry.<n>We prove VLWE's security by reducing it to multiple independent instances, demonstrating resilience against classical and quantum attacks.
  arXiv  Detail & Related papers  (2025-02-11T06:04:24Z)
• Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization [4.2518927441106]
  Main bottleneck in existing methods is a computationally expensive quantifier elimination step.<n>We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula.<n>Our method offers a range of appealing theoretical properties combined with a strong practical performance.
  arXiv  Detail & Related papers  (2024-12-18T14:37:15Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure.<n>Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
  arXiv  Detail & Related papers  (2024-10-17T12:48:14Z)
• Deep Generative Symbolic Regression [83.04219479605801]
  Symbolic regression aims to discover concise closed-form mathematical equations from data. Existing methods, ranging from search to reinforcement learning, fail to scale with the number of input variables. We propose an instantiation of our framework, Deep Generative Symbolic Regression.
  arXiv  Detail & Related papers  (2023-12-30T17:05:31Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.