# 訓練不変条件 ## 定義 訓練不変条件(training invariant)とは、正常な DL 訓練プロセスにおいて常に成立すべき規則であり、違反がサイレントエラーの指標となる命題である。[[TrainCheck]](OSDI 2025)が定式化した概念で、Daikon 等の従来の不変条件推論が扱う低レベル変数関係(idx < len 等)ではなく、DL 訓練固有の**高レベル意味的規則**——分散並列における重みの整合性、API 呼び出し順序、オプティマイザの状態更新——を対象とする。(Source: [[@2025__OSDI__Training with Confidence - Catching Silent Errors in Deep Learning Training with Automated Proactive Checks]]) **不変条件の形式**: `(前提条件(e), 関係(a, b))` の対。前提条件は「この規則がいつ適用されるか」を規定し、偽陽性の削減と別パイプラインへの転用を可能にする。前提条件を推論できない不変条件は「浅い」として廃棄される。 **5 種の関係テンプレート**: - `Consistent(Va, Vb)`: Va と Vb が変化しながらも互いに一致し続ける(分散訓練の重み整合性等) - `EventContain(Ea, Eb)`: Ea 実行中に Eb が必ず発生する(Optimizer.step 内でのパラメータ更新確認等) - `APISequence(Ia, Ib, ...)`: 指定 API が指定順に全て呼ばれる(zero_grad → backward 等) - `APIArg(Ia, is_distinct)`: API 引数の一貫性または区別の保証 - `APIOutput(Ia, bound_type)`: API 出力の属性制約 **前提条件の 4 型**: CONSTANT(特定値で固定)・CONSISTENT(値不変)・UNEQUAL(レコード間で異なる)・EXIST(全レコードに存在) **推論アルゴリズム(3 段階)**: 1. 仮説生成: トレース中の全変数ペア/API に各関係テンプレートを候補適用 2. 仮説検証: 通過例・不通過例を収集 3. 前提条件推論: 通過/不通過例を弁別する条件集合を演繹(統計的有意性でプルーニング) **転用可能性**: 推論された不変条件は、推論に使ったパイプラインとは異なるパイプラインにも適用可能。PyTorch 固有不変条件の 23% は 16 以上のパイプラインに適用可能。前提条件付き不変条件は無条件不変条件より転用性が高い。 ## 横断的知見 (本概念について複数ソースの突き合わせによる知見は、2 ソース目以降の ingest で蓄積する。) - 訓練不変条件は Daikon 等の従来不変条件推論とは「観察の粒度」で根本的に異なる。Daikon は個々の変数値の関係(x > y 等)を抽出するのに対し、TRAINCHECK の不変条件は DL 訓練の意味的単位(分散ランク間の重み整合性・オプティマイザの状態遷移)を規則化する。DL 特有の非決定性(確率的最適化)は高レベルで観察することで回避できるという洞察が核心にある。(Source: [[@2025__OSDI__Training with Confidence - Catching Silent Errors in Deep Learning Training with Automated Proactive Checks]]) ## 未解決の問い - 前提条件の推論アルゴリズムは現在「最弱前提条件の近似」であり厳密ではない。静的プログラム解析と組み合わせることでより精密な前提条件を得られるか。コストに見合うか。 - 5 種の関係テンプレートは BLOOM-176B 等の事例分析から帰納的に設計された。どのようなサイレントエラーのクラスが未カバーのまま残るか。 - 形式的仕様(formal specification / type system)によるアプローチと、自動推論アプローチのトレードオフはどこにあるか。推論の限界を形式仕様で補完する「ハイブリッド」は成立するか。 - LLM ベースの訓練コード生成(Copilot 等)が普及すると、訓練パイプラインの多様性はどう変化するか。転用可能な不変条件の割合は増加するか、減少するか。 ## 関連 - [[DLトレーニングサイレントエラー]] — 訓練不変条件が検知対象とする障害クラス - [[TrainCheck]] — 訓練不変条件を自動推論・継続検証するフレームワーク(OSDI 2025) - [[Heisenbug]] — 再現困難な障害の上位概念。サイレントエラーの一形態 - [[非侵入プロファイリング]] — 低オーバーヘッド観測技法の関連概念 ## 出典 - [[@2025__OSDI__Training with Confidence - Catching Silent Errors in Deep Learning Training with Automated Proactive Checks]]