TorchLean

6.13. Two-Stage Verification Workflows🔗

Two stage workflows are the "train and verify in Python, then post-check in Lean" path. In this repo that means Python training and α,β-CROWN on one side, and Lean evaluation, autograd, and post-checks in TorchLean on the other.

TorchLean does not vendor the Two-Stage / α,β-CROWN repository. The core TorchLean library and lake build do not require that Python stack. If you want to run the external producer workflow, clone the Two-Stage repository separately. TorchLean no longer carries that producer as a submodule.

The workflow has four stages:

  • Python training, Julia simulation, or α,β-CROWN produces a checkpoint, JSON artifact, or bound report.

  • TorchLean parses the artifact into typed Lean data.

  • A TorchLean checker replays the supported computation, checks structure, or records an explicit oracle boundary.

  • The final report says which part was proved in Lean, which part was recomputed, and which part remains trusted external evidence.

6.13.1. Scope🔗

Below is how TorchLean connects Python training and α,β-CROWN runs to Lean replay and checking. For flags and solver options on the Python side, follow the Two-Stage repository; those details change independently of TorchLean.

To run a verifier tool, use lake exe verify -- list and the tool names in NN.Verification.CLI API, then read the sections here for what Lean actually checks.

6.13.2. What TorchLean Provides🔗

TorchLean supports the Python-first verification pattern: an external producer writes an artifact, then Lean parses, replays, or structurally checks it. The current Two Stage checker handles a small leaf artifact JSON format exported from α,β-CROWN: abcrown-leaf (see the certificate guide for what this does and does not check).

6.13.3. Quick Run (From TorchLean)🔗

The Two Stage checker is registered in the unified verification CLI, so the easiest place to start is:

lake exe verify -- list

For debugging certificate export and import, the leaf checker is the usual starting point:

lake exe verify -- abcrown-leaf

6.13.4. Minimal Setup (One-Time)🔗

Clone the external producer only if you want to generate fresh α,β-CROWN / Two-Stage artifacts:

  • git clone https://github.com/Verified-Intelligence/Two-Stage_Neural_Controller_Training.git Two-Stage_Neural_Controller_Training

The Python verifier dependencies are managed by the external Two-Stage / α,β-CROWN repositories; TorchLean does not try to own that environment. Local α,β-CROWN runs follow those repositories' instructions; artifact export is described in Certificates.

6.13.5. What Is Actually Checked🔗

It is important to be explicit about trust boundaries. The Lean pipelines re-evaluate models against TorchLean's semantics, including the chosen scalar domain such as IEEE32Exec, and run TorchLean's bound propagation and checkers on the resulting graphs. The abcrown-leaf JSON artifacts are structural leaf artifacts today: TorchLean can parse them and check their declared shape and metadata, but they do not yet carry a fully checkable proof of the bound computation.

Certificates checked against the shared IR semantics: see the RealCert-style artifacts in Certificates.

For the Lean declarations, open the verification CLI and the α,β-CROWN leaf checker. The external producer checkout is separate, and sample assets are kept in NN/Examples/Verification/AbCrown/.

6.13.6. Reproducibility Notes🔗

Two stage workflows depend on both the Lean checker and the external producer environment. The short checklist that helps most is to pin the external producer commit, record the Python environment used for the external verifier, and record the scalar backend selected for the Lean replay. That makes it much easier to compare a Lean replay against the original Python run later.

Broader verifier map: Verification. Float32 execution details: Floating-Point Semantics.

6.13.7. References🔗

  • TorchLean paper (Two-Stage case study context): https://arxiv.org/abs/2602.22631

  • α,β-CROWN codebase: https://github.com/Verified-Intelligence/alpha-beta-CROWN

  • β-CROWN / α,β-CROWN paper: https://arxiv.org/abs/2103.06624