AF: Small: Trusting Inference About Polynomial Inequalities with Certificates

This project develops new methods to help computers automatically verify that certain mathematical statements involving polynomial inequalities are true. Polynomials are widely used to model real-world systems including many scientific and engineering applications. Polynomial optimization under constraints plays a foundational role in a wide range of domains, including robotics, aerospace systems, cyber-physical systems, control theory, quantum information, and machine learning. The research will create tools that not only test these mathematical statements about polynomials but also produce clear, trustworthy evidence—called certificates—to explain why they are correct. These advances will improve the safety and reliability of complex systems such as autonomous vehicles and intelligent controllers. This project investigates the problem of certifying the nonnegativity of a polynomial inequality over the real values defined by a finite basis of polynomial inequalities — a core question in real algebraic geometry with significant implications for verification, stability analysis, and systems modeling – and, if so, produce nonnegative multipliers for the basis elements exhibiting a proof. The research develops two complementary approaches to generate certificates of nonnegativity: (i) Algebraic approach – Leveraging Groebner basis methods and introducing a novel N-basis framework, the project explores nonnegativity-preserving rewriting techniques and generation of N-polynomials from finite sets of polynomials (N-completion) to construct finite bases that certify implication between polynomial inequalities. A degree-bound strategy will ensure termination and tractability. (ii) Geometric approach – Building on Positivstellensatz theory, the project aims to construct certificates via membership in quadratic modules and preorderings. Even though the membership for a finitely generated quadratic module can be decided using general methods including cylindrical algebraic decomposition with its various extensions including critical point methods, generating certificates showing evidence about correct reasoning is elusive. A compositional method for generating certificates from factored polynomials will be extended from univariate to multivariate cases. The project will identify structural properties of basis elements and associated semi-algebraic sets to construct equivalent intermediate bases to enable efficient certificate computation. The anticipated outcomes of this project include new symbolic-numeric algorithms and formal guarantees for reasoning about polynomial inequalities, with potential applications in software verification, neural network certification, and optimization in engineering and physical sciences. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.