Classifier Training And Verification🔗

The maintained workflow trains a 2 -> 8 -> 2 ReLU classifier: two input coordinates, eight hidden units, and two output scores. Its eight training examples separate by the sign of the first coordinate. Positive first coordinates have class-zero labels; negative first coordinates have class-one labels. Training fits that distinction with one-hot cross-entropy and SGD. Verification then fixes the resulting weights and asks about the model that was actually trained:

-- Keep the parameters produced by these 120 training steps.
let trained ← trainer.train dataset { steps := 120 }
-- Ask whether class zero stays strictly ahead throughout
-- the input box.
let report ← trained.verify center
  (radius := 0.10)
  (norm := .inf)
  (property := .topLabel 0)
report.printSummary

Tensor shapes use the public notation: [] for a scalar tensor, [n] for a vector, and [m, n] for a matrix. The call above does not expose recursive shape constructors, graph nodes, flat boxes, or parameter stores.

Run it with either maintained CPU arithmetic mode:

# Run the classifier workflow with its default CPU scalar
# backend.
lake exe verify -- torchlean-mlp-workflow
# Repeat using the executable IEEE binary32 scalar model.
lake exe verify -- torchlean-mlp-workflow --arithmetic ieee

A seeded run on both backends prints the same result:

mean_loss(before) = 0.978569
mean_loss(after) = 0.010960
prediction at center=[1.885023, -3.156008]
Alpha-Beta-CROWN lower=[1.639539, -3.572599] upper=[2.130507, -2.739417] label=0
  margin=4.378956 certified=true

The report lower-bounds class zero by 1.639539 and upper-bounds its only competitor by -2.739417. Their difference is the positive reported margin 4.378956, so the chosen bound pass reports certified=true for the requested input box. The semantic and arithmetic bridges below are required before interpreting that report as a theorem.

Read the loss lines as a description of fitting the training examples. Their decrease says nothing by itself about the entire perturbation region. The prediction at center line is a single forward evaluation: 1.885023 beats -3.156008, so the center receives class zero. The lower and upper arrays answer a different question. Their entries describe bounds on each score as the input varies. To protect class zero, the unfavorable comparison uses its lowest allowed score and class one's highest allowed score. Comparing the two center scores would miss that variation.

Here .inf means that each input coordinate may move independently by at most the radius. In real coordinates the intended region is [1.4, 1.6] × [-0.1, 0.1]. This geometric meaning is part of the verification request; the representation and rounding of its endpoints still belong to the arithmetic obligations below.

The reported margin subtracts the competitor's upper endpoint from class zero's lower endpoint. Using the displayed values gives:

4.378956

The flag tests the computed margin. The six-decimal endpoints above have also been rounded for display, so subtracting their printed values checks the displayed arithmetic, not the exact internal margin or a theorem about every point in the box.

A proof of the reported property would connect the source model to the lowered graph, show that the propagated boxes contain its outputs throughout the input region, and use the positive margin to compare the two logits. For native binary32 execution, the same argument also needs a bound on how far its outputs can move from those semantic values.

The obligations also localize maintenance. A lowering change affects the source-to-graph argument; a new CROWN activation affects bound propagation; and a CUDA deployment claim requires the native arithmetic link in addition to the real-valued theorem.

Semantic Target And Graph Boundary🔗

The verifier operates on the canonical NN.IR.Graph. An interval or affine form is meaningful only relative to a denotation of that same graph, parameter store, and input box. A lowering theorem is therefore part of a source-model claim.

TorchLean has two relevant forward correspondences. The typed first-order proved forward fragment lowers NN.Verification.Builtin.Proved.ForwardProgram values. Its constructors cover constants, parameters, arithmetic, ReLU, exp, log, inverse, matrix products, reshapes and permutations, softmax along any valid axis, axis-parametrized LayerNorm, linear and convolution layers, and MSE loss. Correctness.lowerForwardProgramToIR_wellFormed proves structural well-formedness, while Correctness.runForwardIR_eq_evalForward proves equality with the typed program evaluator.

The second correspondence starts from canonical IR rather than the typed source language. denoteAll_eq_of_lowerToForwardGraph proves that a successful lowering to the forward-only IRExec.ForwardGraph preserves denotation for every input, with NoRawLog as its only side condition. A third, smaller fact sits underneath both: NN.IR.Graph.checkShapes_sound proves that the shapes declared in an accepted graph are the shapes its denotation computes.

Both are Lean semantic equalities over an abstract scalar Context. They are not statements that a PyTorch module, CUDA kernel, or vendor library agrees with the graph. General API lowering also does not inherit the typed-fragment theorem merely because it returns the same IR type.

The following signatures are checked against the imported NN modules when the page builds. They expose the scalar type, accepted fragment, and success conditions needed to apply each result.

@lowerForwardProgramToIR_wellFormed : ∀ {α : Type} [inst : TorchLean.Storage α] [inst_1 : Context α]
  {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape}
  (p : NN.Verification.Builtin.Proved.ForwardProgram α paramShapes inShape outShape)
  (params : TorchLean.TensorPack α paramShapes),
  (NN.Verification.Builtin.Proved.lowerForwardProgramToIR p params).graph.wellFormed = true

@runForwardIR_eq_evalForward : ∀ {α : Type} [inst : TorchLean.Storage α] [inst_1 : Context α]
  {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape}
  (p : NN.Verification.Builtin.Proved.ForwardProgram α paramShapes inShape outShape)
  (params : TorchLean.TensorPack α paramShapes) (x : TorchLean.Tensor α inShape),
  NN.Verification.Builtin.runForwardIR (NN.Verification.Builtin.Proved.lowerForwardProgramToIR p params) x =
    NN.Verification.Builtin.Proved.evalForward p params x

@denoteAll_eq_of_lowerToForwardGraph : ∀ {α : Type} [inst : TorchLean.Storage α] [inst_1 : Context α] (g : NN.IR.Graph)
  (payload : NN.IR.Payload α) (exec : ForwardGraph α),
  NoRawLog g →
    lowerToForwardGraph g payload = Except.ok exec →
      ∀ (x : TorchLean.Tensor α exec.inShape),
        g.denoteAll payload { shape := exec.inShape, tensor := x } = Except.ok (exec.denoteAll x)

@NN.IR.Graph.checkShapes_sound : ∀ {α : Type} [inst : TorchLean.Storage α] [inst_1 : Context α] (g : NN.IR.Graph)
  (payload : NN.IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)),
  g.checkShapes = Except.ok () →
    g.denoteAll payload input = Except.ok vals →
      ∀ (i : ℕ) (hi : i < g.nodes.size) (hiv : i < vals.size), vals[i].shape = g.nodes[i].outShape

Each #check prints a declaration's type. It does not execute the model or apply the theorem to this classifier. In the first output, read everything before the final expression as the data the theorem accepts; the expression ending in wellFormed = true is what it establishes. The second output ends in an equality between two evaluators, both given the same parameters and input. That equality is the link needed when a bound on one representation is to say something about the other.

In these signatures, ∀ means “for every,” {...} contains arguments Lean can often infer, and [...] requests an interface instance, such as the scalar operations in Context α. An arrow P → Q says that a proof of P yields a proof of Q. Long namespaces tell Lean which definition is meant; the important reading order is the objects, then the hypotheses, then the conclusion. For example, the third output needs both NoRawLog g and successful lowering before it gives equality for every input x.

The typed-program results need no additional success premise: the program constructors, shapes, and scalar interfaces already restrict the objects they accept. The IR-to-forward-graph result instead assumes that lowering returns Except.ok exec. It also requires NoRawLog g, excluding all raw-log nodes, even those whose inputs would be positive. The canonical evaluator checks the logarithm's input domain, while the pure forward graph applies the total scalar operation. Public IO autograd performs its own domain validation; that does not change this pure theorem's premise.

Shape soundness has a different role. Once shape checking and denotation both succeed, it identifies the shape of each computed value with the declaration at the corresponding node. It supplies no existence result for the value table: successful denotation is an assumption.

IBP🔗

Interval bound propagation assigns each node a box. For an affine layer

y=Wx+b,\qquad x\in[\ell,u],

the usual sign split gives

\ell_y=W^+\ell+W^-u+b,\qquad u_y=W^+u+W^-\ell+b,

where W^+=\max(W,0) and W^-=\min(W,0). Monotone activations transform endpoints; ReLU maps [\ell,u] to [\max(0,\ell),\max(0,u)]. Elementwise multiplication needs all endpoint products.

For one weighted input, a nonnegative weight preserves the order of the endpoints and a nonpositive weight reverses it. Splitting the weight into these two parts gives the lower and upper bounds below. Summing this scalar argument across a row gives the affine-layer rule.

The graph proof applies local enclosure arguments like these at each node in topological order. The induction maintains enclosure for every earlier value, so a node can use the bounds on its parents. Tensor dimensions, parameter lookup, and missing values must also agree between the bound pass and the semantic evaluator. Directed floating arithmetic adds the obligation that rounded endpoints remain on the enclosing side of the exact result.

The generic real soundness theorem is cert_encloses_semantics. It requires:

• TopoSorted g;

• Supported g;

• exact local certificate consistency CertLocalOK;

• exact local value consistency SemLocalOK;

• InputsEnclosed.

It concludes that each available certificate box encloses the matching semantic value. The current Supported predicate contains input, constant, detach, addition, subtraction, elementwise multiplication, ReLU, linear, matrix multiplication, tanh, sigmoid, softplus, safe logarithm, sine, and cosine nodes.

The proof-side real evaluator has the stronger end-to-end theorem runIBP?_encloses_evalGraphRec. It proves that the particular real runIBP? construction encloses evalGraphRec, under topological order, supported operations, and enclosed inputs.

The executable engine is now covered as well, on a named core. runIBP_eq_runIBP? proves that the engine's runIBP computes exactly the proof-side pass on graphs whose nodes are all in EngineCore (input, constant, detach, addition, subtraction, elementwise multiplication, ReLU, linear, matrix multiplication, softplus, and safe logarithm), provided the semantic-support guard succeeds and the proof-side pass produced a box at every node (IBPCovers). runIBP_encloses_evalGraphRec then gives enclosure for the executable engine directly. Both are stated over ℝ; the transcendental node kinds outside EngineCore and every rounded scalar remain outside these two theorems.

cert_encloses_semantics : ∀ (g : NN.MLTheory.CROWN.Graph) (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (cert : Array (Option (NN.MLTheory.CROWN.FlatBox ℝ))) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)),
  TopoSorted g →
    Supported g →
      CertLocalOK g ps cert →
        SemLocalOK g ps inputs vals →
          InputsEnclosed g ps inputs →
            ∀ id < g.nodes.size,
              match cert[id]!, vals[id]! with
              | some B, some v => EnclosesBox B v
              | x, x_1 => True

runIBP?_encloses_evalGraphRec : ∀ (g : NN.MLTheory.CROWN.Graph) (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs : Std.HashMap ℕ Val),
  TopoSorted g →
    Supported g →
      InputsEnclosed g ps inputs →
        ∀ id < g.nodes.size,
          match (runIBP? g ps)[id]!, (evalGraphRec g ps inputs)[id]! with
          | some B, some v => EnclosesBox B v
          | x, x_1 => True

runIBP_eq_runIBP? : ∀ (g : NN.MLTheory.CROWN.Graph) (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ),
  TopoSorted g →
    EngineCore g → g.crownGraphSemanticsSupported ps = true → IBPCovers g (runIBP? g ps) → g.runIBP ps = runIBP? g ps

runIBP_encloses_evalGraphRec : ∀ (g : NN.MLTheory.CROWN.Graph) (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs : Std.HashMap ℕ Val),
  TopoSorted g →
    EngineCore g →
      IBPCovers g (runIBP? g ps) →
        InputsEnclosed g ps inputs →
          ∀ id < g.nodes.size,
            ∀ (B : NN.MLTheory.CROWN.FlatBox ℝ) (v : Val),
              (g.runIBP ps)[id]! = some B → (evalGraphRec g ps inputs)[id]! = some v → EnclosesBox B v

The first two conclusions examine a pair of optional entries. Enclosure is asserted only when both a box and a semantic value are present; the other cases return True. Thus these theorems can justify an available bound without promising that the pass produces every bound an application needs. IBPCovers supplies the separate coverage condition in the executable-engine results.

The names describe the pieces of the graph induction. TopoSorted puts a node's parents before that node. Supported restricts the operations to those with a proved transfer rule. CertLocalOK says that the stored boxes follow those rules, and SemLocalOK says that the stored values follow the graph's evaluator. InputsEnclosed starts the induction by placing the actual input values inside the input boxes. For the classifier, the conclusion we ultimately need is enclosure at the output node; these hypotheses explain how the proof can reach that node.

runIBP_eq_runIBP? identifies the executable real pass with the proof-side construction under its listed guards. Substituting that equality into the proof-side enclosure result gives a theorem about the engine. No second arithmetic argument is needed for that substitution.

IBP   lo=[-4.000000] hi=[4.000000]
CROWN lo=[-2.000000] hi=[2.000000]

corner value: -2.000000
corner value: 2.000000
corner value: -2.000000
corner value: 2.000000

-- This import exposes verification on the ordinary
-- trained-model result.
import NN.API.Verification

-- Verification uses the trained weights retained in this
-- value.
let trained ← trainer.train dataset { steps := 120 }
-- Radius and norm define the input set; topLabel defines
-- the output property.
let report ← trained.verify center
  (radius := 0.10)
  (norm := .inf)
  (property := .topLabel 0)

# Wrap the same model with an interface that propagates
# bounds.
from auto_LiRPA import BoundedModule, BoundedTensor
from auto_LiRPA.perturbations import PerturbationLpNorm

model = BoundedModule(mlp, torch.empty_like(center))
# Each coordinate may vary by at most 0.10 around the
# center.
ptb = PerturbationLpNorm(norm=float("inf"), eps=0.10)
lb, ub = model.compute_bounds(
    x=(BoundedTensor(center, ptb),), method="alpha-CROWN")
# Compare class zero's lower bound with class one's upper
# bound.
print((lb[0, 0] - ub[0, 1]).item())

CROWN, Alpha-CROWN, And Alpha-Beta-CROWN🔗

CROWN (Zhang et al., 2018) propagates affine lower and upper forms rather than only boxes. Bounding a network by a convex outer approximation and then optimizing inside it predates CROWN (Wong and Kolter, 2018); CROWN obtains bounds with a backward pass. At an uncertain ReLU with \ell<0<u, the secant upper relaxation is

\operatorname{ReLU}(z) \le \frac{u}{u-\ell}(z-\ell),

while a lower relaxation may use a slope \alpha constrained to a valid range. Alpha-CROWN optimizes these slopes. Alpha-beta-CROWN (Wang et al., 2021) additionally records branch phases: an active branch uses z\ge 0, and an inactive branch uses z\le 0. Splitting on a phase can tighten the relaxation, at the cost of additional bound passes.

TorchLean's generic theorem crown_checker_encloses_semantics takes an exact CrownCertLocalOK hypothesis and a separate CrownTransferSound proof. The local transfer theorems

• alphaCrown_transfer_sound;

• alphaBetaCrown_transfer_sound

show that the proposition-level alpha and alpha-beta step functions satisfy CrownTransferSound under their explicit real-semantic and enclosure hypotheses. The alpha-beta step rejects phase choices inconsistent with the current IBP interval.

The transfer theorems take the IBP boxes as an assumption, IBPEnclosesVals. The composed corollaries discharge it from the IBP soundness theorem. alphaCrown_cert_encloses_semantics and alphaBetaCrown_cert_encloses_semantics' conclude enclosure from topological order, supported operations, locally consistent boxes and values, enclosed inputs, valid slopes, and a certificate that replays the affine step; alphaCrown_cert_encloses_evalGraphRec fixes the boxes to runIBP? and the values to evalGraphRec, so only the graph, input, slope, and certificate hypotheses remain. These are the forms a caller should cite.

The executable runAlphaBetaCROWN pass first runs IBP, infers every ReLU phase already forced by the interval, and rechecks that phase while replaying affine bounds. Unstable phases remain unsplit and use the default alpha relaxation. This is a useful native fixed-relaxation pass; it is not the external Alpha-Beta-CROWN optimizer's branch-and-bound search.