論文の概要: 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（参考訳）: 横方向拡散のためのツリーベース機械学習モデルの形式的検証
• 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モデルをデプロイするための検証修正検証エンジニアリングループと正式な認証を確立する。

関連論文リスト

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。 提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。 IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
  論文  参考訳（メタデータ） (2026-09-09T17:59:04Z)
• FLY-EVAL++: An Evidence-Driven Evaluation Protocol for Safety-Constrained Flight Prediction with Large Language Models [45.90905049052029]
  FLY-EVAL++は,安全クリティカル環境下での大規模言語モデルに対するエビデンス駆動評価プロトコルである。 PilotBench設定を履歴条件および多段階予測タスクで拡張することにより、FLY-EVAL++ for Flight Trajectory and Attitude Prediction (FTAP)をインスタンス化する。 本結果より, 安全クリティカル領域の評価は, 精度中心の報告のみに頼るのではなく, 制約満足度と構造的妥当性を明示的に測定すべきであることが示唆された。
  論文  参考訳（メタデータ） (2026-09-03T16:00:02Z)
• Measuring Stability and Failure Behavior in Language Models Under Structured Perturbations [0.5076419064097734]
  ストレステスト推論モデルのための、グレード付き、多家族対応のフェールアウェアフレームワークを提案する。 それぞれの問題を7つのファミリーにまたがる複数のレベルの重大さのはしごに沿ってゆがめている。 すべてのテストは、その測定された重症度によって評価され、ラベル付けされる。
  論文  参考訳（メタデータ） (2026-08-22T23:46:11Z)
• Confidently Wrong: Exception Chain Collapse in Frontier LLM Rule Evaluation [0.0]
  フェデレーションクラスをフロンティアの大規模言語モデルで文書化する。 故障は最初の観測で再現されるが、経験的表面は不安定である。 規制されたフロンティアモデルの正確性は、注意を払わずにシフトする移動したコンプライアンス境界である。
  論文  参考訳（メタデータ） (2026-07-25T22:40:02Z)
• Neurosymbolic Auditing of Natural-Language Software Requirements [0.30079490585515345]
  本稿では,このアイデアを医療デバイスソフトウェア要求に対して運用するニューロシンボリックパイプラインであるVERIMEDを提案する。 VERIMED における LLM に基づくアプローチは曖昧さに敏感な要求を低減できることを示す。
  論文  参考訳（メタデータ） (2026-05-13T17:43:13Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。 VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。 我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
  論文  参考訳（メタデータ） (2026-04-12T00:52:27Z)
• Towards Counterfactual Explanation and Assertion Inference for CPS Debugging [0.0]
  本稿では,サイバー物理システムのための実証的説明とアサーションに基づくキャラクタリゼーションフレームワークであるDeCaFを紹介する。 テスト入力がフェールすると、DeCaFは入力信号の反ファクト変化を生成し、テストが通過しないよう変換する。 提案手法は,3つの反事実生成器と2つの因果モデルを組み合わせて,成功の主張を推測する。
  論文  参考訳（メタデータ） (2026-04-09T00:53:00Z)
• Structural Rigidity and the 57-Token Predictive Window: A Physical Framework for Inference-Layer Governability in Large Language Models [0.0]
  現在のAIの安全性は、行動監視とトレーニング後のアライメントに依存している。 実験的な測定は、これらのアプローチは検出可能な事前コミット信号を生成しないことを示している。 本稿では,トランスフォーマー推論のダイナミクスを制約満足度モデルに結合するエネルギーベースのガバナンスフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-04-04T00:08:17Z)
• 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)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  生成のための教師なし共形推論フレームワークを提案する。 我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。 その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
  論文  参考訳（メタデータ） (2025-09-26T23:40:47Z)
• 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)
• Addressing Misspecification in Simulation-based Inference through Data-driven Calibration [43.811367860375825]
  本研究は, モデル不特定性を克服するフレームワークであるロPEを導入し, 実世界の小キャリブレーションによる地下構造パラメータの測定を行った。 4つの合成課題と2つの実世界の問題により、RoPEはベースラインを上回り、情報的およびキャリブレーションされた信頼区間を一貫して返却することを示した。
  論文  参考訳（メタデータ） (2024-05-14T16:04:39Z)
• 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)
• Precise Statistical Analysis of Classification Accuracies for Adversarial Training [43.25761725062367]
  この問題を治療するために、近年、様々な敵の訓練手順が提案されている。 我々は,逆向きに訓練されたミニマックスモデルの標準とロバストな精度を正確に評価する。
  論文  参考訳（メタデータ） (2020-10-21T18:00:53Z)

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

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