AttentionVerify

LiRPA/IBP certificate checker: attention-like softmax graph.

This example builds a compact computation graph: input -> matmul -> softmax -> matmul, seeds a small input box, and checks a JSON certificate produced by an external IBP/LiRPA tool.

References:

• IBP: "On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models" (arXiv:1810.12715): https://arxiv.org/abs/1810.12715
• CROWN (background): https://arxiv.org/abs/1811.00866
• auto_LiRPA (common reference implementation): https://github.com/Verified-Intelligence/auto_LiRPA

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

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

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

Small fixed graph with one softmax node, used to exercise certificate checking.

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

Seed deterministic weights for the two matmul nodes in buildGraph.

def NN.Examples.Verification.LiRPA.AttentionVerify.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.AttentionVerify.verifyCert (path : String) : IO Unit

Check an IBP certificate JSON against this attention graph.

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