Exact SOS certificates
Repairing floating-point SOS solutions into exact certificates a proof assistant can check.
SOS solvers work in floating point, so the certificates they return are almost right: the polynomial identity is off by tiny residues, and the Gram matrices are only numerically positive semidefinite. This project turns those near-misses into exact rational certificates that a proof assistant can check.
Exact arithmetic, live in your browser. The polynomial is written as \(p = m^\top Q\, m\) with \(m = (1, x, y, x^2, xy, y^2)\):
The starting matrix stands in for an interior-point solver's answer: close to the boundary of the PSD cone, with errors around \(10^{-7}\). Step through the pipeline or change the rounding precision. This demo uses the simplest repair (spread each coefficient's residue evenly over its Gram entries, then test with an exact LDLᵀ factorization), which can fail when rounding is coarse; try 1 or 3 bits. The repair in my dissertation instead solves for a diagonally dominant correction as a linear program over the rationals, so positive semidefiniteness holds by construction. The Lean block is a sketch, with long fractions shortened.
Where the certificates come from
A barrier certificate for a polynomial system is a set of polynomial identities. Schematically, over a semialgebraic domain described by polynomials \(p_i, q_i, r_i\),
\[B \equiv \textstyle\sum_i \alpha_i\, p_i + \alpha_0, \qquad -B \equiv \textstyle\sum_i \beta_i\, q_i + \beta_0, \qquad -\nabla B \cdot f + \lambda B \equiv \textstyle\sum_i \sigma_i\, r_i + \sigma_0,\]where every multiplier \(\alpha, \beta, \sigma\) is a sum of squares: \(m(x)^\top Q\, m(x)\) for some positive semidefinite Gram matrix \(Q\). If the identities hold exactly and every \(Q\) is PSD, the barrier conditions follow (a Positivstellensatz argument). The successive and repulsive certificates on the other project pages are all of this form.
What goes wrong
A solver that reports success can still hand back something that is not a proof:
- Identity drift. Rounding the solution leaves a small nonzero residue \(r(x) = p(x) - m(x)^\top Q\, m(x)\). This is the most common failure.
- Borderline definiteness. The smallest eigenvalue of \(Q\) is near zero, or slightly negative, and the margin is below the solver’s tolerance.
- No rational solution nearby. \(Q\) may be PSD but irrational, so any rational rounding breaks the identity.
- Tight margins. Nearly active constraints give nearly singular Gram matrices, and rounding amplifies the drift.
The repair
- Solve the SOS program in double precision to get \(Q_{\mathrm{fp}}\).
- Round to rationals and compute the residue \(r(x)\) exactly; it becomes the target of the repair.
- Absorb the residue with a slack whose Gram matrix is constrained to be diagonally dominant, which is a linear program in the matrix entries.
- Re-solve that linear program in exact rational arithmetic (CDDLib, from Julia). The result \(Q_{\mathbb{Q}}\) satisfies \(m^\top Q_{\mathbb{Q}}\, m = p\) exactly, and diagonal dominance implies \(Q_{\mathbb{Q}} \succeq 0\) with no eigenvalue computation at all.
- Factor \(Q_{\mathbb{Q}} = L D L^\top\) to write \(p\) as an explicit sum of squares with rational coefficients, and export it.
The exported certificate is checked in Lean 4: the polynomial identities close by normalizing both sides, the coefficient signs by exact arithmetic, and the Positivstellensatz entailment from those facts. What used to rest on a solver’s tolerance becomes a machine-checked proof (Wajid, 2026).