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.

翻译：神经网络正日益部署于安全和任务关键型流程中，然而许多验证与分析结果是在定义和运行模型的编程环境之外产生的。这种分离造成了执行网络与分析工件之间的语义鸿沟，使得保证可能依赖于隐式约定，如算子语义、张量布局、预处理及浮点数边界情况。我们提出TorchLean，一个基于Lean 4定理证明器的框架，将学习模型视为具有单一精确语义的一阶数学对象，该语义由执行与验证共享。TorchLean统一了：(1) 具有即时编译与编译两种模式的PyTorch风格验证API，可降级至共享的操作符标记SSA/DAG计算图中间表示；(2) 通过可执行的IEEE-754 binary32内核及证明相关的舍入模型实现显式Float32语义；(3) 通过IBP和CROWN/LiRPA风格的边界传播与证书检查进行验证。我们在认证鲁棒性、PINNs的物理信息残差边界及李雅普诺夫风格神经控制器验证上对TorchLean进行端到端验证，同时结合机械化理论结果（包括通用逼近定理）。这些成果展示了一种语义优先的基础设施，可用于学习赋能系统的完全形式化端到端验证。