Clinch

The content on this page was written by AI under human supervision.

Clinch (Certified Local Interval-Newton Convergence for Hierarchies) proves that a fitted optimum of a hierarchical statistical model is a strict local optimum, or says exactly why it cannot. The input is the fitted parameter vector and an evaluator for the model's gradient and Hessian written in ball arithmetic. The output is a certificate that a small box around the candidate contains exactly one stationary point, with a positive-definite Hessian throughout, or a refusal naming the test that failed.

What it does

An optimizer reports convergence when the gradient is small, and everything computed afterward (standard errors, likelihood-ratio tests, model comparison) assumes the optimizer stopped at a true strict local minimum. Clinch either proves that assumption or reports why it cannot. It works in ball arithmeticevery number is stored as a midpoint and a radius that provably contains the true value, so all rounding error is tracked (Arb, through python-flint) and applies the Krawczyk test, an interval form of Newton's method. With $F$ the gradient, $H(X)$ the Hessian enclosed over a box $X$ around the candidate $\tilde x$, and $C$ an approximate inverse of the midpoint Hessian, showing that

$$K(X) \;=\; \tilde x - C\,F(\tilde x) + \bigl(I - C\,H(X)\bigr)(X - \tilde x)$$

lies strictly inside $X$ proves that a zero of $F$ exists in $X$ and is unique there. A second test proves every symmetric matrix in $H(X)$ positive definite, so that zero is a strict local minimum.

Hierarchical (mixed, random-effects) models have a block-arrow Hessian: independent diagonal blocks, one per group of latent parameters, coupled only through a dense border of global parameters. The kernel Clinch calls, baller.certify.block_krawczyk in Baller, runs both tests block by block with an interval Schur complement on the border; about 5,600 coordinates in 582 blocks certify in roughly 90 seconds at the default 192-bit precision. Clinch adds the model evaluators, the choice of box, the handling of bounds, and the certificate files.

Clinch returns one of four verdicts. CERTIFIED-INTERIOR is the statement above with no bound active. CERTIFIED-CORNER applies when coordinates sit exactly on bounds you declared: the free coordinates certify and the sign of each active bound's multiplier is proven over the box, giving a strict local minimum of the bounded problem. REFUSED names what failed and by what margin: a block or the border that did not contract, a block that is not positive definite, a candidate too far from stationary, or the 30-minute time budget. OUT-OF-SCOPE means the evaluator does not cover the model's parameter layout.

The box is chosen by the code. Radii are scaled per coordinate by the local curvature and start at twice the candidate's own Newton step; boxes 1, 2, 4 and 8 times that size are tried, and no radius may exceed one curvature standard deviation. A wide box around a poorly converged point would be a true statement of little value, so Clinch refuses and reports how far from stationary the candidate is; expect this for a point taken straight from a general-purpose optimizer. The remedy is newton_polish, a few structured Newton steps, followed by a certificate at the polished point, reported separately with its distance from the original.

Limits. Every statement from engine.certify is local; it claims nothing about global optimality. The objective must be smooth over the box. The certified target is the unclipped objective, so an evaluator for a model that clips probabilities must check each clip over the box and report any it cannot prove inactive. The evaluator must use ball arithmetic end to end (the jets module helps); a quantity whose enclosure leaves its domain becomes a refusal. The evaluators included cover the large hierarchical ecological model the package was first written for (species-, genus- and family-level effects under shared global parameters) and Etienne's sampling formula from neutral community ecology. For another model you write an object with the same small interface (dims, part, F(x), H(x)); the synthetic test problem SynthOracle in the Routines list is a complete short example.

Examples

Run the self-test. From tools/clinch/ in a checkout that also contains tools/baller/:

python3 selftest.py

The script runs the acceptance tests from a fresh scratch directory (they refuse to run from inside the package tree) and prints a PASS or FAIL line per test, L1 through L8, then an OVERALL line. The self-contained tests certify a synthetic optimum whose exact rational solution is known, refuse a constructed saddle point naming the offending block, and certify a mean-centered (equality-constrained) variant of the same problem including positive definiteness of its reduced Hessian. Others check that three precisions agree, that a starved precision refuses, and that an evaluator error becomes a refusal rather than a crash. L3, L6 and one part of L4 read stored results of BootLoops' reference fits, which are not distributed; on a public checkout they report the missing files and the script still ends with a line beginning clinch selftest PASS and exit status 0.

Certify a known optimum from Python. Test L1 reduced to its core, on the synthetic test problem (two latent blocks of sizes 3 and 2, three global parameters, exact optimum known):

import sys
sys.path.insert(0, "tools/baller"); sys.path.insert(0, "tools/clinch")
sys.path.insert(0, "tools/clinch/battery")
import clinch
clinch.verify(quiet=True)
from synthetic import SynthOracle, exact_optimum
from clinch import engine, cert
zs_ex, g_ex = exact_optimum()
theta = [float(v) for v in zs_ex[0] + zs_ex[1] + g_ex]
res = engine.certify(SynthOracle(), theta, prec=128)
assert res["verdict"] == "CERTIFIED-INTERIOR", res["verdict"]
cert.write_cert(res, out_dir, "synthetic")

res holds the verdict, the per-coordinate radius range (radius_min, radius), the precision, and the box sizes tried. Under krawczyk it lists the contraction margin of each named block and of the border (each provably below 1), and under pd the positive-definiteness margins (each provably above 0). write_cert writes CERT.json with those fields plus STATEMENT.txt, one plain paragraph stating what was proven, into out_dir (any writable directory). The same test then certifies a candidate held exactly at a declared lower bound with engine.certify(base, list(th), bounds=(lo, None), prec=128), which returns CERTIFIED-CORNER with the certified multiplier signs under kkt; without bounds that candidate is REFUSED with failed == "fat-ball".

Polish, then certify. An interior candidate refused as too far from stationary is polished and certified again, as in the manual's quick start:

thp, prcpt = engine.newton_polish(o, theta)     # labeled second product
resp = engine.certify(o, thp)                   # polished-center cert

prcpt["distance_inf"] is the largest coordinate change the polish made; report it beside the certificate so a reader knows which point was certified.

Routines

Command line

Python package clinch

Etienne-model adapter (adapters/etienne/)

Other included parts (code only; the studies' data and stored results are not distributed, and each script that needs them stops with a message when its environment variable is unset)

Requirements and source

Python 3 with python-flint (Arb ball arithmetic), NumPy and mpmath, plus Baller beside Clinch (tools/baller/, or set CLINCH_BALLER_DIR). Run the tests with python3 selftest.py from the package directory. The code is tools/clinch/ in BootLoops' bootloops-dev repository (GitHub organization BootLoops-ai), released under the MIT license, with GUIDE.md (summary) and MANUAL.md (full detail) beside it.

← back to the tools index