TorchLean: Formalizing Neural Networks in Lean

神经网络正日益被部署于安全关键型与任务关键型系统中，然而目前许多验证与分析工作却在定义并运行模型的编程环境之外展开。这种分离在实际执行的网络与被分析的对象之间造成了语义鸿沟，致使相关安全性保证往往依赖于一系列隐含约定，例如算子语义、张量内存布局、预处理流程以及浮点运算中的边界情况。为此，我们提出了 TorchLean——一个构建于 Lean 4 定理证明器之上的框架，它将学习所得的模型视为一等数学对象，并为模型的执行与验证统一提供单一、精确且共享的语义。TorchLean 实现了三方面的统一：（1）一套经形式化验证、类 PyTorch 风格的 API，支持即时执行（eager）与编译执行（compiled）两种模式，并均向下编译至同一套带算子标签的静态单赋值（SSA）/有向无环图（DAG）计算图中间表示（IR）；（2）通过一个可执行的 IEEE-754 binary32 内核及具备证明相关性的舍入建模机制，显式地刻画 float32 浮点语义；（3）支持基于区间传播（IBP）以及 CROWN/LiRPA 风格的界传播方法进行验证，并配备可验证的证书检查机制。我们端到端地在多个典型场景中对 TorchLean 进行了实证验证，包括：神经网络的认证鲁棒性、物理信息神经网络（PINN）的物理一致性残差界分析，以及基于李雅普诺夫（Lyapunov）风格的神经控制器验证；此外，还完成了若干机械化理论成果的形式化证明，其中包括通用逼近定理（universal approximation theorem）。上述成果共同表明，TorchLean 构建了一种以语义为先（semantics-first）的基础设施，为学习赋能系统（learning-enabled systems）提供了真正全程形式化、端到端可验证的坚实支撑。

神经网络在安全关键系统中的部署日益广泛，但当前验证与分析通常在脱离实际执行环境（如PyTorch）的独立形式化框架中进行，导致语义鸿沟——执行行为（算子语义、张量布局、预处理、IEEE-754浮点细节）与验证假设不一致，使形式保证依赖未明确定义的隐式约定，威胁可信性与可复现性。这是一个尚未被系统解决的新问题：缺乏端到端统一语义的、可执行且可验证的神经网络基础设施。

提出TorchLean——首个将学习模型作为Lean 4中一等数学对象的框架，通过三重统一设计实现语义一致性：(1) PyTorch风格API（支持eager/compiled模式）统一降级至带操作符标签的SSA/DAG中间表示；(2) 显式、可执行的Float32语义（基于IEEE-754 binary32标准）与证明相关的舍入模型；(3) 内置IBP与CROWN/LiRPA式区间界传播，并支持证书检查。核心新意在于‘语义优先’（semantics-first）：执行与验证共享同一形式化定义，消除跨工具链的语义漂移。

端到端验证三个典型场景：(1) 认证鲁棒性（CIFAR-10/100上L∞扰动）；(2) 物理信息神经网络（PINN）的残差界认证（含Navier-Stokes方程约束）；(3) Lyapunov式神经控制器稳定性验证（倒立摆等非线性系统）。理论贡献包含在Lean 4中完全机械化证明的通用逼近定理（Universal Approximation Theorem）。所有代码开源（Lean 4项目），IR与浮点内核可执行并用于测试，验证结果生成可检查证书。值得深入的方向包括：扩展至混合精度/FP16、支持动态图与控制流、与硬件验证（如FPGA）联合建模。

Neural Networks as Programs: A Verified Framework (POPL'23); VeriNet: A Tool for Verifying Neural Networks (CAV'21); ERAN: Efficient Robustness Analysis for Neural Networks (ICML'20); LiRPA: Certified Robustness with Tighter Bounds (NeurIPS'21); DeepPoly: Complete and Scalable Neural Network Verification (CAV'18); CertiCoq: Verified Compilation of Coq to C (POPL'22); Lean 4’s Mathlib formalization of real analysis and IEEE-754