TorchLean: Formalizing Neural Networks in Lean

• URL: http://arxiv.org/abs/2602.22631v1
• Date: Thu, 26 Feb 2026 05:11:44 GMT
• Title: TorchLean: Formalizing Neural Networks in Lean
• Authors: Robert Joseph George, Jennifer Cruden, Xiangru Zhong, Huan Zhang, Anima Anandkumar,
• Abstract summary: We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
• Score: 71.68907600404513
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks are increasingly deployed in safety- and mission-critical pipelines, yet many verification and analysis results are produced outside the programming environment that defines and runs the model. This separation creates a semantic gap between the executed network and the analyzed artifact, so guarantees can hinge on implicit conventions such as operator semantics, tensor layouts, preprocessing, and floating-point corner cases. We introduce TorchLean, a framework in the Lean 4 theorem prover that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification. TorchLean unifies (1) a PyTorch-style verified API with eager and compiled modes that lower to a shared op-tagged SSA/DAG computation-graph IR, (2) explicit Float32 semantics via an executable IEEE-754 binary32 kernel and proof-relevant rounding models, and (3) verification via IBP and CROWN/LiRPA-style bound propagation with certificate checking. We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification, alongside mechanized theoretical results including a universal approximation theorem. These results demonstrate a semantics-first infrastructure for fully formal, end-to-end verification of learning-enabled systems.

Related papers

• Learning with Boolean threshold functions [0.013714053458441644]
  We develop a method for training neural networks on sparse data in which the values at all nodes are strictly $pm 1$.<n>Across a range of tasks, this method provides a viable and efficient foundation for learning in neural systems.
  arXiv  Detail & Related papers  (2026-02-19T16:07:25Z)
• Autonomous Chain-of-Thought Distillation for Graph-Based Fraud Detection [73.9189065770752]
  Graph-based fraud detection on text-attributed graphs (TAGs) requires jointly modeling rich textual semantics and relational dependencies.<n>We propose FraudCoT, a unified framework that advances TAG-based fraud detection through autonomous, graph-aware chain-of-thought (CoT) reasoning and scalable LLM-GNN co-training.
  arXiv  Detail & Related papers  (2026-01-30T13:12:12Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  We develop a sheaf/cohomology and causal emergence perspective to Transformer Circuits.<n>EICS combines (i) a normalized sheaf inconsistency computed from local Jacobians and activations, with (ii) a Gaussian EI proxy for circuit-level causal emergence.<n>We provide practical guidance on score interpretation, computational overhead (with fast and exact modes), and a toy sanity-check analysis.
  arXiv  Detail & Related papers  (2025-09-08T18:54:56Z)
• A Constructive Framework for Nondeterministic Automata via Time-Shared, Depth-Unrolled Feedforward Networks [0.0]
  We present a formal and constructive simulation framework for nondeterministic finite automata (NFAs) using time-shared, depth-unrolled feedforward networks (TS-FFNs)<n>Our formulation symbolically encodes automaton states as binary vectors, transitions as sparse matrix transformations, and nondeterministic branching-including $varepsilon$-closures-as compositions of shared thresholded updates.
  arXiv  Detail & Related papers  (2025-05-30T01:18:35Z)
• LASE: Learned Adjacency Spectral Embeddings [9.227991604045416]
  We learn nodal Adjacency Spectral Embeddings (ASE) from graph inputs.<n>LASE is interpretable, parameter efficient, robust to inputs with unobserved edges.<n>LASE layers combine Graph Convolutional Network (GCN) and fully-connected Graph Attention Network (GAT) modules.
  arXiv  Detail & Related papers  (2024-12-23T17:35:19Z)
• VeriFlow: Modeling Distributions for Neural Network Verification [3.510536859655114]
  Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks.<n>We propose the VeriFlow architecture as a flow-based density model tailored to allow any verification approach to restrict its search to some data distribution of interest.
  arXiv  Detail & Related papers  (2024-06-20T12:41:39Z)
• Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach [64.23331120621118]
  This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks. We introduce a related embedded network and show that the embedded network can be used to provide an $ell_infty$-norm box over-approximation of the reachable sets of the original network. We apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.
  arXiv  Detail & Related papers  (2022-08-08T03:13:24Z)
• DAIS: Automatic Channel Pruning via Differentiable Annealing Indicator Search [55.164053971213576]
  convolutional neural network has achieved great success in fulfilling computer vision tasks despite large computation overhead. Structured (channel) pruning is usually applied to reduce the model redundancy while preserving the network structure. Existing structured pruning methods require hand-crafted rules which may lead to tremendous pruning space.
  arXiv  Detail & Related papers  (2020-11-04T07:43:01Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  We propose a first-order dual SDP algorithm that requires memory only linear in the total number of network activations. We significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.
  arXiv  Detail & Related papers  (2020-10-22T12:32:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.