論文の概要: TorchLean: Formalizing Neural Networks in Lean

• arxiv url: http://arxiv.org/abs/2602.22631v1
• Date: Thu, 26 Feb 2026 05:11:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-27 18:41:22.538027
• Title: TorchLean: Formalizing Neural Networks in Lean
• Title（参考訳）: TorchLean: リーンでニューラルネットワークを形式化する
• Authors: Robert Joseph George, Jennifer Cruden, Xiangru Zhong, Huan Zhang, Anima Anandkumar,
• Abstract要約: 本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。 我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: ニューラルネットワークは、安全とミッションクリティカルなパイプラインにますますデプロイされているが、モデルを定義して実行するプログラミング環境の外で、多くの検証と分析結果が生成される。 この分離によって、実行されたネットワークと分析されたアーティファクト間のセマンティックギャップが生成されるため、オペレータのセマンティクス、テンソルレイアウト、前処理、浮動小数点コーナーケースなどの暗黙の規則を保証できる。 我々は、Lean 4定理証明のフレームワークであるTorchLeanを紹介します。これは、学習したモデルを、実行と検証によって共有される単一の正確なセマンティクスで、第一級の数学的オブジェクトとして扱うものです。 TorchLeanは,(1)オペタグ付きSSA/DAG計算グラフIRの共有モード,(2) 実行可能なIEEE-754 binary32カーネルおよび証明関連丸めモデルによる明示的なFloat32セマンティクス,(3) IBPおよびCROWN/LiRPAスタイルのバウンドプロパゲーションによる検証,などを備えたPyTorchスタイルの検証APIを統一する。 我々は、証明されたロバスト性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証、および普遍近似定理を含む機械的理論結果について、TorchLeanのエンドツーエンド性を検証した。 これらの結果は、学習可能なシステムの完全形式的なエンドツーエンド検証のためのセマンティクスファーストのインフラを実証している。

関連論文リスト

• Autonomous Chain-of-Thought Distillation for Graph-Based Fraud Detection [73.9189065770752]
  テキスト分散グラフ(TAG)上のグラフベースの不正検出には、リッチテキストセマンティクスとリレーショナル依存関係を共同でモデル化する必要がある。 我々は,自律型グラフ認識チェーン(CoT)推論とスケーラブルなLLM-GNN協調学習を通じて,TAGに基づく不正検出を促進する統一フレームワークであるFraudCoTを提案する。
  論文  参考訳（メタデータ） (2026-01-30T13:12:12Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  本研究では,トランスフォーマー回路のシャーフ/コホモロジーと因果出現の視点を開発する。 EICSは(i)局所ジャコビアンとアクティベーションから計算された正規化棚の不整合と(ii)回路レベルの因果発生のためのガウスEIプロキシを組み合わせる。 本稿では,スコアの解釈,計算オーバーヘッド(高速かつ高精度なモード),およびおもちゃの健全性チェック分析に関する実践的ガイダンスを提供する。
  論文  参考訳（メタデータ） (2025-09-08T18:54:56Z)
• A Constructive Framework for Nondeterministic Automata via Time-Shared, Depth-Unrolled Feedforward Networks [0.0]
  非決定論的有限オートマトン(NFA)の時間分割・深度制御型フィードフォワードネットワーク(TS-FFN)を用いたフォーマルで建設的なシミュレーションフレームワークを提案する。 我々の定式化は、二進ベクトルとしてのオートマトン状態、スパース行列変換としての遷移、および共有しきい値更新の合成としての$varepsilon$-closuresを含む非決定的分岐を含む非決定論的分岐を象徴的に符号化する。
  論文  参考訳（メタデータ） (2025-05-30T01:18:35Z)
• LASE: Learned Adjacency Spectral Embeddings [9.227991604045416]
  グラフ入力から結節隣接スペクトル埋め込み(ASE)を学習する。 LASEは解釈可能で、パラメータ効率が高く、未観測のエッジを持つ入力に対して堅牢である。 LASEレイヤは、Graph Convolutional Network (GCN)と完全に接続されたGraph Attention Network (GAT)モジュールを組み合わせる。
  論文  参考訳（メタデータ） (2024-12-23T17:35:19Z)
• Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach [64.23331120621118]
  本稿では,暗黙的ニューラルネットワークのトレーニングとロバスト性検証のための理論的および計算的枠組みを提案する。 組込みネットワークを導入し、組込みネットワークを用いて、元のネットワークの到達可能な集合の超近似として$ell_infty$-normボックスを提供することを示す。 MNISTデータセット上で暗黙的なニューラルネットワークをトレーニングするためにアルゴリズムを適用し、我々のモデルの堅牢性と、文献における既存のアプローチを通じてトレーニングされたモデルを比較する。
  論文  参考訳（メタデータ） (2022-08-08T03:13:24Z)
• DAIS: Automatic Channel Pruning via Differentiable Annealing Indicator Search [55.164053971213576]
  畳み込みニューラルネットワークは,計算オーバーヘッドが大きいにもかかわらず,コンピュータビジョンタスクの実行において大きな成功を収めている。 構造的(チャネル)プルーニングは、通常、ネットワーク構造を保ちながらモデルの冗長性を低減するために適用される。 既存の構造化プルーニング法では、手作りのルールが必要であり、これは大きなプルーニング空間に繋がる可能性がある。
  論文  参考訳（メタデータ） (2020-11-04T07:43:01Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  本稿では,ネットワークアクティベーションの総数にのみ線形なメモリを必要とする一階二重SDPアルゴリズムを提案する。 L-inf の精度は 1% から 88% ,6% から 40% に改善した。 また,変分オートエンコーダの復号器に対する2次安定性仕様の厳密な検証を行った。
  論文  参考訳（メタデータ） (2020-10-22T12:32:29Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。