論文の概要: Early Verification of Legal Compliance via Bounded Satisfiability Checking

• arxiv url: http://arxiv.org/abs/2209.04052v3
• Date: Sun, 28 May 2023 02:29:19 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-24 14:54:49.941458
• Title: Early Verification of Legal Compliance via Bounded Satisfiability Checking
• Title（参考訳）: 境界満足度検査による法的コンプライアンスの早期検証
• Authors: Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik
• Abstract要約: 計量一階時間論理(MFOTL)は、法的な性質を特定するためのリッチな形式主義を提供する。 MFOTLをベースとした早期システム開発における検証のためのソリューションは存在しない。 MFOTLの実用的,健全かつ完全満足度チェック手法を提案する。
• 参考スコア（独自算出の注目度）: 4.304202636346692
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Legal properties involve reasoning about data values and time. Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties. While MFOTL has been successfully used for verifying legal properties over operational systems via runtime monitoring, no solution exists for MFOTL-based verification in early-stage system development captured by requirements. Given a legal property and system requirements, both formalized in MFOTL, the compliance of the property can be verified on the requirements via satisfiability checking. In this paper, we propose a practical, sound, and complete (within a given bound) satisfiability checking approach for MFOTL. The approach, based on satisfiability modulo theories (SMT), employs a counterexample-guided strategy to incrementally search for a satisfying solution. We implemented our approach using the Z3 SMT solver and evaluated it on five case studies spanning the healthcare, business administration, banking and aviation domains. Our results indicate that our approach can efficiently determine whether legal properties of interest are met, or generate counterexamples that lead to compliance violations.
• Abstract（参考訳）: 法的特性には、データ値と時間に関する推論が含まれる。 計量一階時間論理(mfotl)は、法的性質を特定するための豊富な形式を提供する。 MFOTLは実行時監視による運用システム上の法的特性の検証に成功しているが、要求によってキャプチャされた初期システム開発におけるMFOTLベースの検証のためのソリューションは存在しない。 MFOTLで形式化された法的特性とシステム要件が与えられた場合、その特性のコンプライアンスは満足度チェックによって要求に基づいて検証することができる。 本稿では,mfotlの実用的,音質的,完全性(所定のバウンド内)の充足性チェック手法を提案する。 充足性モジュラー理論(smt)に基づいたこのアプローチでは、満足のいく解を漸進的に探索するために反例誘導戦略を用いる。 本手法をZ3 SMTソルバを用いて実施し,医療・経営・銀行・航空分野にまたがる5つのケーススタディで評価した。 提案手法は, 利害関係の法的性質が満たされているか否かを効率よく判断し, コンプライアンス違反につながる反例を生成できることを示す。

関連論文リスト

• Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo [55.452453947359736]
  Twisted Sequential Monte Carlo(TSMC)に基づく新しい検証手法を提案する。 TSMCを大規模言語モデルに適用し、部分解に対する将来的な報酬を推定する。 このアプローチは、ステップワイドなヒューマンアノテーションを必要としない、より直接的なトレーニングターゲットをもたらす。
  論文  参考訳（メタデータ） (2024-10-02T18:17:54Z)
• Optimizing Numerical Estimation and Operational Efficiency in the Legal Domain through Large Language Models [13.067312163677933]
  本稿では,Large Language Modelsと特殊設計のプロンプトを統合して,法的な人工知能(LegalAI)アプリケーションにおける精度要件に対処する手法を提案する。 本手法を検証するために,精度指向の LegalAI タスクに適したキュレートデータセットを提案する。
  論文  参考訳（メタデータ） (2024-07-26T18:46:39Z)
• Rethinking Legal Compliance Automation: Opportunities with Large Language Models [2.9088208525097365]
  我々は、(テキスト)法的アーティファクトの試験は、まず文よりも広い文脈で行うべきであると論じる。 これらの制約に対処するために,コンプライアンス分析手法を提案する。
  論文  参考訳（メタデータ） (2024-04-22T17:10:27Z)
• Auditing large language models: a three-layered approach [0.0]
  大規模言語モデル(LLM)は人工知能(AI)研究における大きな進歩を表している。 LLMはまた、重大な倫理的・社会的課題と結びついている。 これまでの研究は、監査を有望なガバナンスメカニズムとして取り上げてきた。
  論文  参考訳（メタデータ） (2023-02-16T18:55:21Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-08-12T17:03:50Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。 我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。 本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
  論文  参考訳（メタデータ） (2022-06-15T11:39:45Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Stateless and Rule-Based Verification For Compliance Checking Applications [1.7403133838762452]
  本稿では,インテリジェントなコンプライアンスチェックシステムを構築するための形式的な論理ベースのフレームワークを提案する。 SARVは、ステートレスおよびルールベースの検証問題の全体的な検証プロセスを単純化するために設計された検証フレームワークである。 300のデータ実験に基づいて、SARVベースのコンプライアンスソリューションは、3125レコードのソフトウェア品質データセット上で機械学習メソッドよりも優れています。
  論文  参考訳（メタデータ） (2022-04-14T17:31:33Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。 このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
  論文  参考訳（メタデータ） (2021-08-27T15:04:11Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)

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

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