GruVerify

LiRPA/IBP certificate checker: GRU-style gate fragment.

This example builds a small nonlinear graph with sigmoid, tanh, and an elementwise multiply: x -> linear -> sigmoid x -> linear -> tanh mul_elem(sigmoid(x), tanh(x))

It is a focused fragment that exercises common RNN nonlinearities in the LiRPA certificate checker.

References:

• IBP: arXiv:1810.12715 https://arxiv.org/abs/1810.12715
• auto_LiRPA (reference implementation / exporter inspiration): https://github.com/Verified-Intelligence/auto_LiRPA

Export (Python): python3.12 scripts/verification/lirpa/export_gru_cert.py

Run (Lean): lake exe verify -- lirpa-gru [NN/Examples/Verification/LiRPA/gru_gate_cert.json]

def NN.Examples.Verification.LiRPA.GruVerify.buildGraph : MLTheory.CROWN.Graph

Small nonlinear graph exercising sigmoid, tanh, and mul_elem.

def NN.Examples.Verification.LiRPA.GruVerify.seedParamsFloat : MLTheory.CROWN.Graph.ParamStore Float

Seed deterministic linear weights for the two .linear nodes in buildGraph.

def NN.Examples.Verification.LiRPA.GruVerify.seedInputFloat (ps : MLTheory.CROWN.Graph.ParamStore Float) (eps : Float) : MLTheory.CROWN.Graph.ParamStore Float

Insert an L∞ input box of radius eps around a fixed center point.

def NN.Examples.Verification.LiRPA.GruVerify.verifyCert (path : String) : IO Unit

Check an IBP certificate JSON against this GRU-fragment graph.

This is wired into lake exe verify -- lirpa-gru [path].