omnibias.verify
Certified neural-network verification. Propagates rigorous enclosures
(intervals / multivariate Taylor models from omnibias.core.verified) through a
trained network, with branch-and-bound over the input box, to produce
theorem-grade certificates.
import omnibias.verify as ov
Every enclosure provably contains the true output set (sound by
construction). The procedure is not complete — branch-and-bound may return
UNKNOWN rather than over-claim.
Network model
| Symbol | Role |
|---|---|
Network, Layer, VerifiedLayer | the verifiable network model |
LinearLayer, ReLULayer, GELULayer, TanhLayer, SigmoidLayer, MaxPoolLayer | layer types |
IntervalMatrix | interval-valued matrix |
SUPPORTED_ACTIVATIONS, KERNELS | capability tables |
verified_layers, verified_layer_bundle, VerifiedLayerBundle | weight ingestion bundles |
Weight ingestion from the differentiable backends lives in
omnibias.verify.torch / omnibias.verify.jax (import explicitly).
Propagation
interval_propagate · taylor_propagate · interval_jacobian ·
output_range · taylor_output_bounds · linear_image · affine_layer ·
reachable_box · scalar_readout_range.
Enclosures
relu_enclosure · relu_taylor · gelu_enclosure · max_enclosure ·
gauss_cdf_iv · compose_sigma · compose_gelu · jet_remainder_iv.
Certificates
| Symbol | Certifies |
|---|---|
certify_robustness → RobustnessCertificate | local robustness of a classifier |
lipschitz_bound | a certified Lipschitz constant |
monotonicity → MonotonicityCertificate | monotonicity in chosen inputs |
certify_no_dead_unit | no permanently dead unit |
certify_agreement_margin, agreement_margin_iv | agreement margins |
certify_pinn_aposteriori → CertifiedPDEPipelineResult | an a-posteriori PINN residual bound |
Result containers: BoundResult, RangeResult, CertifiedBound.
Example
from omnibias.verify import certify_robustness
cert = certify_robustness(network, x0, epsilon=0.03)
print(cert) # holds / UNKNOWN, with the enclosing bounds