Paper

{
  "raw_xml": "<entry>\n    <id>http://arxiv.org/abs/2602.22631v1</id>\n    <title>TorchLean: Formalizing Neural Networks in Lean</title>\n    <updated>2026-02-26T05:11:44Z</updated>\n    <link href='https://arxiv.org/abs/2602.22631v1' rel='alternate' type='text/html'/>\n    <link href='https://arxiv.org/pdf/2602.22631v1' rel='related' title='pdf' type='application/pdf'/>\n    <summary>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.</summary>\n    <category scheme='http://arxiv.org/schemas/atom' term='cs.MS'/>\n    <category scheme='http://arxiv.org/schemas/atom' term='cs.LG'/>\n    <category scheme='http://arxiv.org/schemas/atom' term='cs.LO'/>\n    <category scheme='http://arxiv.org/schemas/atom' term='cs.PL'/>\n    <category scheme='http://arxiv.org/schemas/atom' term='math.NA'/>\n    <published>2026-02-26T05:11:44Z</published>\n    <arxiv:comment>35 pages, multiple figures and tables</arxiv:comment>\n    <arxiv:primary_category term='cs.MS'/>\n    <author>\n      <name>Robert Joseph George</name>\n    </author>\n    <author>\n      <name>Jennifer Cruden</name>\n    </author>\n    <author>\n      <name>Xiangru Zhong</name>\n    </author>\n    <author>\n      <name>Huan Zhang</name>\n    </author>\n    <author>\n      <name>Anima Anandkumar</name>\n    </author>\n  </entry>"
}