External Search And Certificate Checking🔗

A search procedure chooses where to spend computation. α,β-CROWN's branch-and-bound method (Wang et al., 2021), for example, refines relaxations and splits domains until it can prune them or must continue searching. A sound certificate checker would allow those search choices to remain untrusted: any accepted evidence would have to imply the property regardless of how it was found.

For a leaf, the semantic claim is that a margin bound holds at every point of its sub-box. This is a quantified statement about a fixed network, even though a finite artifact may carry evidence for it. Checking only the exported endpoints and margins does not establish that statement.

TorchLean's leaf format currently checks a narrower set of facts: dimensions, containment, root coverage, witness indices, and comparisons among exported numbers. It can detect inconsistent fields. A consistently misapplied sign or axis convention can still pass, because the artifact has no network or transfer rules against which to check that convention.

The phrase checked by Lean covers everything from parsing a JSON file to replaying every bound computation and deriving a theorem. TorchLean's leaf checker sits near the parsing end. The certificate chapter derives its predicates line by line; this chapter starts one step earlier, at the producer, and follows the data outward.

Producer Artifact Export🔗

The external verifier's terminal-domain data must be converted to TorchLean's schema. The adapter export_leaf_artifact.py does the translation. It accepts the field names external tools actually use, normalizes them, computes a witness coordinate, and writes the checked format.

The bundled raw dump is written in α,β-CROWN's vocabulary, not TorchLean's:

{
  "root": {
    "lo": [-1.0, -1.0],
    "hi": [1.0, 1.0]
  },
  "domains": [
    {
      "x_L": [-1.0, -1.0],
      "x_U": [1.0, 1.0],
      "lower_bounds": [1.0],
      "thresholds": [0.0]
    }
  ]
}

Run the whole producer-to-checker path on it:

# Normalize the bundled terminal-domain dump and check the
# resulting leaf document.
python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input NN/Examples/Verification/AbCrown/example_raw_leaf_dump.json \
  --out /tmp/torchlean-abcrown-artifact.json \
  --check

The --check option runs scripts/lake.sh exe verify -- abcrown-leaf on the file it just wrote. The exported artifact is

{
  "format": "abcrown_leaf_artifact_v0_1",
  "input_dim": 2,
  "leaves": [
    {
      "hi": [1.0, 1.0],
      "lb": [1.0],
      "lo": [-1.0, -1.0],
      "threshold": [0.0],
      "witness_idx": 0,
      "witness_margin": 1.0
    }
  ],
  "root": {
    "hi": [1.0, 1.0],
    "lo": [-1.0, -1.0]
  }
}

The writer sorts keys and puts one array element per line, so the file on disk is taller than the listing above, which is reflowed to fit the page. The field names and their order are the real ones. Sorted keys are not a stylistic preference: two runs of the exporter on the same input produce byte-identical files, which makes the artifact diffable in review and hashable in a report.

The adapter first normalizes field names. A leaf's lower box may arrive as lo, input_lo, x_L, x_l, domain_lo, or lower; lower bounds may use lb, lower_bound, lower_bounds, output_lb, or margin_lb. _get_any selects the first present field from its alias list and raises ArtifactExportError if none is present. It does not infer whether the producer used a field with the intended meaning or reject conflicting aliases merely because both are present. The Lean parser receives the normalized spelling.

The witness is computed, not trusted. The adapter picks the coordinate with the largest positive margin lb[i] - threshold[i] and records both the index and the margin. When the index is present, the checker validates that coordinate. The schema also permits an omitted index, in which case the checker searches for a positive margin. Neither route validates the underlying network bound.

When witness_margin is supplied, the checker also requires a witness index and compares that margin with the computed subtraction using an absolute tolerance of 1e-6. This is bookkeeping agreement, not exact equality. The strict lb[i] > threshold[i] test itself uses no tolerance.

For the bundled domain, the witness calculation is 1.0 - 0.0 = 1.0, so index zero is the only possible choice. input_dim = 2 comes from the two endpoint coordinates, while the bound and threshold arrays have length one. This tells us that the domain is two-dimensional and carries one property expression. The converter can establish those lengths and arithmetic relationships from the supplied data. It cannot infer what network expression the producer placed in that one-element bound vector.

A leaf with no positive margin is rejected at export time. Feed the adapter a domain whose lower bound sits below its threshold:

{
  "root": { "lo": [-1.0, -1.0], "hi": [1.0, 1.0] },
  "domains": [
    {
      "x_L": [-1.0, -1.0], "x_U": [1.0, 1.0],
      "lower_bounds": [-0.25], "thresholds": [0.0]
    }
  ]
}

Save that input as /tmp/torchlean-raw-nowitness.json, then run:

python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input /tmp/torchlean-raw-nowitness.json \
  --out /tmp/torchlean-nowitness.json

The export fails before writing the requested artifact. This format represents leaves with positive witnesses; a domain without one cannot be encoded in this positive-witness format. For a root-region claim, such a failure cannot be repaired by simply dropping that domain. Its region still needs coverage and a valid bound.

For instrumenting a verifier in place, the same script exposes the function directly:

# Call the adapter after collecting terminal leaves from the
# external search.
from scripts.verification.abcrown.export_leaf_artifact import \
    write_abcrown_leaf_artifact

write_abcrown_leaf_artifact(
    root_lo=original_property_lo,
    root_hi=original_property_hi,
    leaves=terminal_verified_leaves,
    out_path="leaf_artifact.json",
)

The call belongs after the search has collected its terminal leaves. TorchLean does not vendor α,β-CROWN or the neural-controller repositories: their Python, CUDA, and solver dependencies stay in their own environments, and the core Lean build needs only the exported JSON.

Root Boxes And Leaf Coverage🔗

The root endpoints identify the property region. Omitting them lets the adapter construct an envelope from the leaves, which changes what the containment check refers to.

Here is a two-leaf dump that splits the unit square down the middle, with no root recorded:

{
  "domains": [
    { "x_L": [-1.0, -1.0], "x_U": [0.0, 1.0],
      "lower_bounds": [0.5], "thresholds": [0.0] },
    { "x_L": [0.0, -1.0], "x_U": [1.0, 1.0],
      "lower_bounds": [1.25], "thresholds": [0.0] }
  ]
}

Save it as /tmp/torchlean-raw-2leaf.json:

python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input /tmp/torchlean-raw-2leaf.json \
  --out /tmp/torchlean-2leaf.json --check

The adapter derives the following root from the leaves:

"root": { "lo": [-1.0, -1.0], "hi": [1.0, 1.0] }

Each leaf lies inside this envelope by construction. The check establishes containment in that derived box, but the box supplies no independent evidence of the original property region. A run record must retain the original root if the claim is about that region.

Now supply a root twice as large as the region the leaves actually cover:

python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input /tmp/torchlean-raw-2leaf.json \
  --out /tmp/torchlean-2leaf-wide.json \
  --root-lo=-2,-2 --root-hi=2,2 --check

The leaves cover [-1,1]^2. The declared property region is [-2,2]^2. Every leaf passes containment, but the current checker rejects the artifact because the leaves do not cover the root. Coverage is a union condition over all leaves. The checker uses the supplied endpoints to check that condition without requiring the producer's search tree.

An accepted abcrown-leaf artifact passes checks that each listed leaf is a well-formed sub-box of the declared root, the leaves cover that root, and each carries a witness that passes its own arithmetic test. The lower bounds themselves remain the producer's claims: coverage does not establish their validity for the network.

The wide-root example separates two questions that often get compressed into “the boxes look right.” Each leaf is a valid subdomain of the declared root. But a point such as (1.5, 0.0) belongs to that root and to neither represented leaf. Even perfect network bounds on the leaves would say nothing about that point. A root-region theorem must be able to take an arbitrary root input, locate a leaf containing it, and apply the leaf's bound. The coverage evidence supplies exactly that middle step.

Coverage can also fail when the root is correct. This next dump records the intended root [-1,1]^2 and two leaves, leaving a strip in the middle that neither leaf covers. This is the kind of gap a lost branch-and-bound subtree could leave.

{
  "root": {
    "lo": [-1.0, -1.0],
    "hi": [1.0, 1.0]
  },
  "domains": [
    { "x_L": [-1.0, -1.0], "x_U": [0.0, 1.0],
      "lower_bounds": [0.5], "thresholds": [0.0] },
    { "x_L": [0.5, -1.0], "x_U": [1.0, 1.0],
      "lower_bounds": [1.25], "thresholds": [0.0] }
  ]
}

Save the dump as /tmp/torchlean-raw-hole.json:

python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input /tmp/torchlean-raw-hole.json \
  --out /tmp/torchlean-hole.json --check

Both leaves pass the local containment and witness checks, yet neither covers a point whose first coordinate lies strictly between 0.0 and 0.5. The CLI's separate coverage check rejects this artifact. We can inspect why local checks alone are insufficient using the same two local predicates the leaf checker uses:

[(true, true), (true, true)]

(true, false)

Both leaves pass both local checks, and (0.25, 0.0) is inside the root and inside no leaf. The displayed experiment stops before the CLI's coverage check. It shows why passing the local checks alone leaves the property on [-1,1]^2 unresolved, even if we grant the claimed bound on each leaf.

Root coverage requires a separate union-of-boxes check or evidence of a complete partition. The current leavesCoverRoot implementation collects sorted distinct endpoints on each axis and checks the resulting closed grid cells. Every cell must lie in at least one leaf. Axes on which every leaf spans the root need no subdivision. The check refuses a grid exceeding one million cells, so a large artifact can require another representation or checking strategy. In several dimensions, sorting by a single coordinate would be insufficient.

false

true

(true, false, true)

Artifact Rejection Tests🔗

The certificate chapter evaluates the checker's predicates one at a time inside Lean. To exercise the command-line path as well, start from the good artifact above, change one field in a separate copy, and check that the process rejects it.

Push a leaf coordinate outside the root, hi[1] = 2.0, and save the copy as /tmp/torchlean-escaped.json:

scripts/lake.sh exe verify -- abcrown-leaf /tmp/torchlean-escaped.json

Leave the arithmetic alone and inflate only the bookkeeping field, witness_margin = 5.0 where the real margin is 1.0. Save this copy as /tmp/torchlean-margin.json:

scripts/lake.sh exe verify -- abcrown-leaf /tmp/torchlean-margin.json

Point the witness past the end of the bound vector, witness_idx = 3 in a one-element lb. Save this copy as /tmp/torchlean-idx.json:

scripts/lake.sh exe verify -- abcrown-leaf /tmp/torchlean-idx.json

The diagnostics distinguish containment, prune, and margin failures. An out-of-range index also prevents margin recomputation, so that edit can fail more than one check. The CLI prints the leaf counts before raising an error, giving the caller both a failing exit status and a location to inspect.

The margin-only edit illustrates why a redundant field can be useful. The lower bound still exceeds its threshold, but the recorded subtraction disagrees with those arrays. That detects an inconsistent artifact without asserting that the underlying network is unsafe.

A caller using these examples in a script should treat a nonzero status as failure of the requested artifact check, then use the diagnostic to identify the field. Rejection by the exporter or checker identifies inconsistent or insufficient artifact data. It does not provide a counterexample to the underlying network property.

Neural Controllers🔗

The leaf workflow exports and checks terminal-domain data. The Lyapunov workflows add training and bound propagation, with different choices about where those computations run. They learn a Lyapunov function and a controller together, then seek a certificate for the pair, following Chang et al. (2019).

A controller adds a time-dependent meaning to the output. Its action changes the system's next state, and a candidate Lyapunov function assigns a scalar value to each state. To reason about decay, we compare that value with its derivative along the system's dynamics. The network may represent the controller, the candidate function, or both; the desired inequality is about the closed-loop system assembled from them.

This is related to the classifier margin argument. In both cases, a universal statement about many inputs is reduced to signs of sound bounds. A classifier needs the chosen score difference to remain positive. A Lyapunov argument needs appropriate positivity and decrease conditions, along with the other hypotheses of the stability result being used. The sign calculation can be short once the bounds are available; establishing what those bounds refer to is the harder part.

• twostage-pythononly-certgen calls the external CROWN producer and writes a Lean module. The generated numbers enter as a LyapunovCert, and Lean proves their sign conditions. The theorem transferring those signs to the Lyapunov functions still assumes LyapunovCert.ValidFor, because this path does not replay the external verifier. Running it needs a .pth checkpoint and the producer's Python environment.

• twostage-hybrid-van-stage2 treats PyTorch as an untrusted initializer. Stage one trains in float32 and exports the parameters as raw bit patterns; stage two loads those bits into FloatLib binary32, refines, and runs the IBP and CROWN box check inside Lean.

• twostage-torchlean-cegis-van does initialization, sampled training, PGD-style candidate search, refinement, and the final bound check in Lean, with no external stage one at all.

Run the all-in-Lean workflow with its default settings:

scripts/lake.sh exe verify -- twostage-torchlean-cegis-van

The hybrid runner re-exports its stage-one weights when asked:

scripts/lake.sh exe verify -- twostage-hybrid-van-stage2 --stage1

Completing either workflow does not by itself establish the requested Lyapunov conditions. The conclusion depends on what the computed bounds prove about the penalty.

The objective adds two ReLU hinge penalties: one for the lower bound on the Lyapunov value, and one for its required decrease along the dynamics. Each penalty is the positive part of a constraint violation. In the exact real interpretation, their nonnegative sum is zero precisely when both encoded inequalities hold at that point. To establish those conditions throughout a box, one needs a sound upper bound of zero on the real penalty. A rounded zero alone needs an arithmetic argument as well. A lower endpoint near zero cannot establish the condition: the useful bound must control the upper endpoint throughout the region.

The reports distinguish sampled training and search losses from bounds on the whole box. The lowered IR node count describes the operation graph; tensor shapes determine how many scalar weights those operations use. The final IBP and CROWN intervals concern the scalar penalty over the selected box (Gowal et al., 2018)(Zhang et al., 2018). An upper bound above zero leaves the encoded condition unresolved. It does not by itself provide a violating point.

The hybrid log's “counterexample candidates” are search outputs to inspect. A candidate becomes evidence of a violated condition only after evaluating the intended property with the required semantics and confirming the violation. The positive-loss count reports the selected executable penalty at the sampled candidates. It does not explain the upper bound on all other states, and it is not a proof about trajectories of the dynamical system.

To compare verifier bounds, hold the model, parameters, input region, and scalar semantics fixed. Changing the network changes the function whose maximum is being bounded. Even for a fixed function, an upper bound alone does not reveal its own looseness; a matching lower estimate of the maximum helps measure that gap. Branching and refined relaxations, as in α,β-CROWN (Wang et al., 2021), can improve inconclusive bounds; auto_LiRPA (Xu et al., 2020) supplies bound propagation across more general graphs. A semantic claim still requires the checker-to-model theorem and its arithmetic assumptions.

{
  "format": "uint32-bits-as-decimal-strings",
  "dtype": "float32",
  "width": 500,
  "wC": ["3156207770", "1061300877"],
  ...
}

# Reinterpret each stored 32-bit pattern as a float.
import struct
[struct.unpack('<f', struct.pack('<I', b))[0]
 for b in (3156207770, 1061300877)]

-0.009760

0.758462

Coordinate Selection In Verifier Lowering🔗

The stage-two loss reads coordinates out of the state vector, x₁ and x₂ for the van der Pol dynamics, with Model.select. The lowering in Lowering/Builder.lean handles select on the leading axis by reading the supplied Fin index while constructing the graph. The index is fixed for that graph; having type Fin alone does not mean a value must be known at elaboration time. Selecting one coordinate becomes a constant one-hot projection: take a leading slice of length one, then reshape to remove that axis.

The slice is encoded as a one-hot matrix multiplication with reshapes. This agrees with selection over exact real arithmetic, but it also evaluates zero products and an accumulation. NaN, infinity, and signed-zero behavior need not match direct floating-point indexing.

indexSelect and scatterAdd take tensor-valued indices and remain outside this lowering fragment. That is a limit of the implemented translation and transfer rules, not a claim that indexed operations cannot be bounded. Selection on an inner axis is also rejected by this builder. The leading-axis case is sufficient for the state coordinates used by these two loss programs.

Lyapunov Certificate Validity🔗

The pipeline that generates a Lean module hands Lean a LyapunovCert: four numbers, plus a region.

The finite numbers cannot, on their own, imply anything about a real-valued dynamical system. The missing ingredient has a name in TorchLean, and it is a Prop:

@LyapunovCert.ValidFor : {α : Type} →
  [inst : Storage α] → [inst_1 : Context α] → {n : ℕ} → LyapunovCert α n → NeuralLyapunov α n → Prop

@RealCert.toCert : {n : ℕ} → RealCert n → LyapunovCert ℝ n

ValidFor cert lyap states enclosure of the supplied Lyapunov value and orbital-derivative functions throughout the region. The four numeric fields alone cannot establish it. A producer must supply checkable evidence for that proposition, or the generated theorem must retain it as a hypothesis.

In the first output, LyapunovCert α n → NeuralLyapunov α n → Prop says that ValidFor takes certificate data and a pair of functions and produces a proposition. That proposition needs a proof. The second output ends in LyapunovCert ℝ n, a data type: toCert repackages the real endpoints into the canonical record. The types already expose the distinction between constructing bounds and proving that they apply to the supplied functions.

For a concrete instance, take the one-dimensional candidate V(x)=x^2 on [1,2], with dynamics x'=-x and orbital derivative -2x^2. RealCert carries the numbers, and RealCert.toCert builds the boxed region from them:

The example can establish that evidence directly. The enclosure has two halves: on the region, V lies in [1,4], and its orbital derivative lies in [-8,-2]:

The region gives 1\le x\le2, hence 1\le x^2\le4 and -8\le-2x^2\le-2. The supplied orbital derivative is consistent with the scalar dynamics x'=-x: the derivative of V(x)=x^2 is 2x, and (2x)(-x)=-2x^2. NeuralLyapunov itself stores the value and orbital-derivative functions independently, so a controller application must establish that connection as well. This example proves sign and range conditions on [1,2]; it does not prove equilibrium stability or invariance of that region.

With the proof in hand, the analytic conclusion follows from the theorem that consumes it:

The two norm_num calls are the sign conditions on the numbers, vLower > 0 and derivativeUpper < 0. In the numeric-only generated-module path, these are the obligations that can be discharged from the imported numbers. Spelling the theorem out at n=1 names the three hypotheses; the example compiles only if the real theorem has exactly this shape:

The hypothesis enclosure supplies ValidFor on the region. The next two hypotheses compare real certificate endpoints with zero. A generated module that leaves ValidFor as a hypothesis proves a conditional sign result. It does not establish that the external verifier's bounds apply to the intended dynamical system.

In a controller workflow the producer searches for a policy u_\theta and a candidate V, aiming at

V(x)\geq 0,\qquad \nabla V(x)\cdot f(x,u_\theta(x)) \leq-\alpha\|x\|^2.

Exporting terminal boxes with positive numeric margins does not prove those inequalities. To close the gap, an artifact would have to identify the model and parameter hash, the state-space root region, the exact dynamics and scalar semantics, every partition leaf, replayable bounds for V and its Lie derivative, and the coverage and boundary conditions. TorchLean's other RealCert-style and IR-based checkers show stronger replay patterns, but each command should be read on its own terms rather than credited by association with the name of an external solver.

Recording A Run🔗

A useful run record lets another person recover the claim and repeat the check. Keep the raw producer dump, the normalized artifact, the exact commands and their outputs, and the source and dependency revisions used for that run. The bundled dump above exercises the exporter and checker; evaluating an external solver additionally requires its repository revision, Python and solver environment, model checkpoint hash, and property file.

Record the dtype, device, numerical settings, original input region, and meaning of each output margin alongside those files. A lower-bound vector changes meaning when the model, property, or margin convention changes. The leaf format does not identify all of those inputs, so a record outside the artifact must supply them. Reproducing the numbers still leaves the semantic proof obligations described below.

Workflow Limits And Proof Obligations🔗

The leaf workflow checks that exported data satisfy its structural contract. Its current limits are concrete:

• Bounded coverage checking. The endpoint-grid check rejects missing regions, as in the wide-root and hole examples above. It refuses grids with more than one million cells.

• No replay. The lower bounds are read, not recomputed against the network.

• No soundness lemma for the predicates. boxWithin, refutesThreshold, and refutesThresholdAt in Util/Tensor.lean are Bool functions with no theorem tying them to a Prop-level statement about box inclusion or margin refutation. The endpoint-grid coverage check likewise has no theorem connecting acceptance to set-theoretic coverage. The local predicates compute the stated comparisons, and the certificate chapter evaluates them on both sides of every boundary, but a reader who wants a proof rather than a test will not find one yet.

The Lyapunov runners additionally compute bounds on a graph lowered from the trained TorchLean program. A completed controller argument needs an upper bound establishing the penalty condition, coverage of the intended region, and proofs connecting the selected checker and arithmetic to the Lyapunov hypotheses.