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 := linf)
  (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.
scripts/lake.sh exe verify -- torchlean-mlp-workflow
# Repeat using the executable IEEE binary32 scalar model.
scripts/lake.sh exe verify -- torchlean-mlp-workflow --arithmetic ieee

The following illustrative values show how to read an abridged report. Rerun the commands above to obtain the current workflow's output; this table does not establish agreement between backends:

avg_loss(on samples)=0.011495
prediction at center=[3.252241, -1.435592]
CROWN lower=[2.956110, -1.593903] upper=[3.548373, -1.277281] label=0
  margin=4.233391 certified=true

The report lower-bounds class zero by 2.956110 and upper-bounds its only competitor by -1.277281. Their difference is the positive reported margin 4.233391, 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.

The loss describes fitting the training examples. A small training loss 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 linf 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.233391

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.

The forward correspondence is a lowering theorem. 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 two-axis transposes, 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.

A smaller fact sits underneath it: NN.IR.Graph.checkShapes_sound proves that the shapes declared in an accepted graph are the shapes its denotation computes.

Both are Lean semantic statements 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

@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 last output needs successful shape checking and successful denotation before it says anything about a value's shape.

The typed-program results need no additional success premise: the program constructors, shapes, and scalar interfaces already restrict the objects they accept. The equality includes errors, so a raw logarithm of a nonpositive input fails in the same way on both sides.

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, concatenation, convolution, 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 has a separate theorem 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, concatenation, convolution, 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 ℝ; operations outside EngineCore and every rounded scalar remain outside these two theorems.

Rounded endpoints have the full forward theorem runIBP_encloses_all in DirectedIBPFullSoundness. It requires LawfulBoundOps, LawfulNonlinearBoundOps, and LawfulMinBoundOps, together with a nonnegative real interpretation of the backend's fixed normalizationEpsilon. The reals and the rounded-real FP32 model satisfy these scalar requirements.

Every box the executable runIBP returns encloses the real value of its node, provided parents precede their consumers, the seed boxes contain the real inputs, and the real point satisfies RealNodeEquation at each node. These equations use the actual coordinate maps, reductions, normalization formulas, and real interpretations of stored parameters; convolution uses the exact spatial operation. Supported transfers include convolution, binary matrix multiplication, structural operations, and normalization. The proof derives their intermediate enclosures by induction. Invalid shapes, missing parameters, and unavailable arithmetic transfers can still leave an entry as none; the theorem establishes enclosure whenever a box is returned. Grouped scaled contractions have a separate numerical-certificate range rule; the direct IBP and CROWN passes currently reject them.

Random nodes use the actual real Spec.Random.uniform and Spec.Random.mask values at Spec.Random.keyOf seed id and the node's row-major coordinate. Uniform nodes have no parents; a mask has one existing scalar parent supplying its keep probability. The lemmas in RandomSupport prove that each uniform value lies in [0,1) and each mask value is zero or one, with keep probabilities zero and one giving the corresponding constant masks. Support follows from these seeded source equations. Agreement with a separate rounded or native random implementation remains a numerical correspondence question. These are the IR's own random-node semantics. Model lowering currently rejects runtime random draws because their keys count random calls rather than IR nodes; it must not silently substitute a different mask. Deterministic evaluation-mode dropout does not draw a mask.

GraphPoint.ofRunIBPAll feeds these bounds to the backward proof and derives its node equations from RealNodeEquation. For checked convolution, positive dilation makes each affine coefficient a stored weight or zero, so interpreting that coefficient agrees with the real spatial operation. This step does not assume that ordinary rounded addition is exact. Structural operations use the same coordinate maps in both directions.

The public theorem backwardObjectiveBox_encloses_runIBP_all in DirectedBackwardEvaluation then connects successful forward IBP, directed backward propagation, and final interval evaluation. It requires exact affine reassociation to be disabled, as it is for FP32, consistent node identifiers, valid input and output dimensions, an objective of the output dimension, and an enclosing input box. Every successful .ok query contains the real objective. No intermediate enclosure or additional backward node equation is assumed.

For a graph in the ibpForwardSupported core, runIBP_encloses, GraphPoint.ofRunIBP, and backwardObjectiveBox_encloses_runIBP use NodeEquation directly. These theorems need no LawfulMinBoundOps instance or normalization-epsilon assumption, since the core excludes the operations that require them.

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

# 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 And Alpha-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;

• phasedCrown_transfer_sound

show that the proposition-level alpha-CROWN step, without and with ReLU phases, satisfies CrownTransferSound under its explicit real-semantic and enclosure hypotheses. The phased 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 phasedCrown_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 outputBoxPhasedCROWN? seeds IBP with the requested input box. On backends that support exact affine reassociation, runPhasedCROWN takes those intervals, infers every ReLU phase they already force, and rechecks it while replaying affine bounds. Unstable phases remain unsplit and use the default alpha relaxation. Rounded scalar backends instead use directed CROWN; nearest-rounded affine coefficients cannot be treated as exact-real enclosures. Both paths are distinct from the external Alpha-Beta-CROWN optimizer's branch-and-bound search.