SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

What the math gives to ML

The paper's transferable asset is a formal method for certifying that a mathematical reformulation preserves feasible solutions and the ordering of global objectives rather than merely matching empirical solver outputs. This can be adapted to neural-network graph rewrites, structured pruning, parameter tying, and loss-preserving reparameterizations by treating the original and transformed models as two constrained optimization problems. The most practical first target is small piecewise-linear subnetworks or compression transformations, where bounded SMT queries can certify exact functional or objective-order equivalence and reject unsafe compiler transformations before large-scale training.