論文の概要: Formal verification of tree-based machine learning models for lateral spreading

• arxiv url: http://arxiv.org/abs/2603.16983v1
• Date: Tue, 17 Mar 2026 16:27:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-19 18:32:57.321407
• Title: Formal verification of tree-based machine learning models for lateral spreading
• Title（参考訳）: 横方向拡散のためのツリーベース機械学習モデルの形式的検証
• Authors: Krishna Kumar,
• Abstract要約: 本稿では,Satifiability Modulo Theories (SMT) 解法において,学習木アンサンブルを論理式として符号化する。 4つの測地学的仕様は決定可能な論理式として定式化され、2011年のクライストチャーチ地震の横分散データセットで訓練されたXGBoostアンサンブルとEBM(Explainable Boosting Machines)の両方に対してSMTを介して検証される。 完全に制約されたESMは4つの仕様のうち3つを満たす。
• 参考スコア（独自算出の注目度）: 1.8935043109084546
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Machine learning models for geotechnical hazard prediction can achieve high accuracy while learning physically inconsistent relationships from sparse or biased training data. Current remedies (post-hoc explainability, such as SHAP and LIME, and training-time constraints) either diagnose individual predictions approximately or restrict model capacity without providing exhaustive guarantees. This paper encodes trained tree ensembles as logical formulas in a Satisfiability Modulo Theories (SMT) solver and checks physical specifications across the entire input domain, not just sampled points. Four geotechnical specifications (water table depth, PGA monotonicity, distance safety, and flat-ground safety) are formalized as decidable logical formulas and verified via SMT against both XGBoost ensembles and Explainable Boosting Machines (EBMs) trained on the 2011 Christchurch earthquake lateral spreading dataset (7,291 sites, four features). The SMT solver either produces a concrete counterexample where a specification fails or proves that no violation exists. The unconstrained EBM (80.1% accuracy) violates all four specifications. A fully constrained EBM (67.2%) satisfies three of four specifications, demonstrating that iterative constraint application guided by verification can progressively improve physical consistency. A Pareto analysis of 33 model variants reveals a persistent trade-off, as none of the variants studied achieve both greater than 80% accuracy and full compliance with the specified set. SHAP analysis of specification counterexamples shows that the offending feature can rank last, demonstrating that post-hoc explanations do not substitute for formal verification. These results establish a verify-fix-verify engineering loop and a formal certification for deploying physically consistent ML models in safety-critical geotechnical applications.
• Abstract（参考訳）: ジオテクニカルハザード予測のための機械学習モデルは、スパースやバイアス付きトレーニングデータから物理的に矛盾する関係を学習しながら高い精度を達成することができる。 現在の治療(SHAPやLIMEのようなポストホックな説明可能性、トレーニング時間制約)は、徹底的な保証を提供することなく、個々の予測を概ね診断するか、モデルのキャパシティを制限するかのいずれかである。 本稿では、学習した木アンサンブルをSMT(Satifiability Modulo Theories)ソルバの論理式として符号化し、サンプリングされた点だけでなく、入力領域全体にわたる物理的仕様をチェックする。 4つの測地学的仕様(水位深度、PGA単調性、距離安全性、平地安全)は決定可能な論理式として定式化され、2011年のクライストチャーチ地震横分散データセット(7,291箇所、4つの特徴)で訓練されたXGBoostアンサンブルと説明可能なブースティングマシン(EBM)の両方に対してSMTを介して検証される。 SMTソルバは、仕様が失敗するか、違反がないことを証明した具体的な反例を生成する。 EBM(80.1%の精度)は4つの仕様全てに違反している。 完全に制約されたEMM (67.2%) は4つの仕様のうち3つを満たすものであり、検証によってガイドされる反復的制約アプリケーションは、物理的一貫性を徐々に改善できることを示した。 33のモデル変種に対するパレート解析では、どの変種も80%以上の精度と指定された集合への完全準拠を達成できないため、永続的なトレードオフが示される。 仕様反例のSHAP分析は、攻撃的特徴が最後にランク付けできることを示し、ホック後の説明が正式な検証に代わらないことを示した。 これらの結果は、安全クリティカルな地学応用に物理的に一貫したMLモデルをデプロイするための検証修正検証エンジニアリングループと正式な認証を確立する。

関連論文リスト

• Certainty-Validity: A Diagnostic Framework for Discrete Commitment Systems [0.0]
  「マシーン学習評価尺度」は、全てのエラーが等価な離散的なコミットメントシステムであると仮定する。 信頼不正確」な振る舞いは、モデルが曖昧なデータの中で構造を幻覚させる場所である。 推論システムのための「Good Training」は、精度ではなく、Certainty-Validity Scoreの最大化によって定義されなければならない。
  論文  参考訳（メタデータ） (2026-02-10T21:53:02Z)
• The Drill-Down and Fabricate Test (DDFT): A Protocol for Measuring Epistemic Robustness in Language Models [0.0]
  現在の言語モデル評価は、理想的な条件下でモデルが知っていることを計測するが、現実的なストレス下でそれをどれだけ堅牢に知っているかは測定しない。 本稿では,ロバスト性を測定するプロトコルであるDrill-Down Fabricate Test (DDFT)を紹介する。 フラッグシップモデルはスケールにもかかわらず脆さを示すのに対して、小さなモデルは堅牢なパフォーマンスを実現することができる。
  論文  参考訳（メタデータ） (2025-12-29T20:29:09Z)
• Geometric Calibration and Neutral Zones for Uncertainty-Aware Multi-Class Classification [0.0]
  この研究は情報幾何学と統計的学習を橋渡しし、厳密な検証を必要とするアプリケーションにおいて不確実性を認識した分類の正式な保証を提供する。 アデノ関連ウイルスの分類に関する実証的な検証は、2段階のフレームワークが72.5%のエラーをキャプチャし、34.5%のサンプルを遅延させ、自動決定エラー率を16.8%から6.9%に下げていることを示している。
  論文  参考訳（メタデータ） (2025-11-26T01:29:49Z)
• Migration as a Probe: A Generalizable Benchmark Framework for Specialist vs. Generalist Machine-Learned Force Fields [1.572216094651749]
  機械学習力場(MLFF)は、分子動力学スケールでのアブ初期レベルの精度を実現することによって、計算材料科学を変革している。 研究者たちは、スペシャリストモデルをスクラッチから訓練するか、ファウンデーショナリストのファンデーションモデルを使うべきか、ハイブリッドアプローチを使うべきか? 本稿では, 弾性バンドトラジェクトリを用いて診断プローブとして評価する, 欠陥マイグレーション経路を用いたベンチマークフレームワークを提案する。 微調整モデルでは、運動特性に対するゼロショットおよびゼロショットのアプローチよりも大幅に優れるが、長距離物理学の部分的な損失を示す。
  論文  参考訳（メタデータ） (2025-08-27T13:24:41Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
  論文  参考訳（メタデータ） (2025-07-07T10:30:05Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Diagnosing and Rectifying Fake OOD Invariance: A Restructured Causal Approach [51.012396632595554]
  不変表現学習(IRL)は、不変因果的特徴から環境から切り離されたラベルへの予測を促進する。 最近の理論的結果は、IRLによって回復されたいくつかの因果的特徴は、訓練環境ではドメイン不変のふりをするが、目に見えない領域では失敗する。 本研究では,RS-SCMに関する条件付き相互情報に基づく手法を開発し,その効果を巧みに補正する。
  論文  参考訳（メタデータ） (2023-12-15T12:58:05Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  大規模言語モデル(LLM)では、不確実性の原因を特定することが、信頼性、信頼性、解釈可能性を改善するための重要なステップである。 本稿では,LLMのための不確実性分解フレームワークについて述べる。 提案手法は,入力に対する一連の明確化を生成し,それらをLLMに入力し,対応する予測をアンサンブルする。
  論文  参考訳（メタデータ） (2023-11-15T05:58:35Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)

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

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