論文の概要: 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions

• arxiv url: http://arxiv.org/abs/2305.05731v2
• Date: Mon, 29 Jan 2024 21:31:53 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-31 19:40:59.390005
• Title: 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
• Title（参考訳）: スタンドに車を停める」:SMTベースのオラクルが意思決定を調査
• Authors: Samuel Judson and Matthew Elacqua and Filip Cano and Timos Antonopoulos and Bettina K\"onighofer and Scott J. Shapiro and Ruzica Piskac
• Abstract要約: 最小限の仮定の下では、自動推論はアルゴリズムの振る舞いを厳格に問うことができることを示す。 我々は、検証やレビューボードなどの説明責任プロセスを、非現実的な論理探索や抽象リファインメントループとしてモデル化する。 われわれのフレームワークを実装し、その実用性を実証的な自動車事故のシナリオで実証する。
• 参考スコア（独自算出の注目度）: 4.170056099990699
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We model accountability processes, such as trials or review boards, as Counterfactual-Guided Logic Exploration and Abstraction Refinement (CLEAR) loops. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. In order to do so, for a decision algorithm $\mathcal{A}$ we use symbolic execution to represent its logic as a statement $\Pi$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario.
• Abstract（参考訳）: 害の余波における原則的説明責任は、アルゴリズムによる意思決定の信頼できる設計とガバナンスに不可欠である。 法理論は、エージェントをスタンドに置き、彼らの行動と横断的な検査の意図を従わせるという、実行可能性を評価するための最優先の方法を提供する。 最小の仮定の下では、自動推論は、法的事実発見の敵対的プロセスのように、アルゴリズムの振る舞いを厳格に問うことができる。 我々は、試験やレビューボードなどの説明責任プロセスを、対実ガイド型論理探索と抽象リファインメント(CLEAR)ループとしてモデル化する。 我々は,人間研究者が適応的に定式化したように,記号実行と満足度変調理論(SMT)の形式的手法を用いて,エージェントの行動に関するクエリを現実的および反現実的シナリオで排出する。 そのためには、決定アルゴリズム $\mathcal{a}$ に対して、決定可能理論 $\texttt{qf_fpbv}$ において、その論理を$\pi$ として表現するために記号的実行を使用する。 われわれのフレームワークを実装し、その実用性を実証的な自動車事故のシナリオで実証する。

関連論文リスト

• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• LogicGame: Benchmarking Rule-Based Reasoning Abilities of Large Language Models [87.49676980090555]
  大規模言語モデル(LLM)は、様々なタスクにまたがる顕著な能力を示し、複雑な問題解決能力を示している。 LLMの包括的なルール理解、実行、計画能力を評価するために設計された新しいベンチマークであるLogicGameを紹介する。
  論文  参考訳（メタデータ） (2024-08-28T13:16:41Z)
• Demystifying Reinforcement Learning in Production Scheduling via Explainable AI [0.7515066610159392]
  深層強化学習(Dep Reinforcement Learning, DRL)はスケジューリング問題の解法としてよく用いられる手法である。 DRLエージェントは、短い計算時間で実行可能な結果を提供するのが得意だが、その推論はいまだに不透明である。 フロー生産における特殊DRLエージェントのスケジューリング決定の背後にある理由を説明するために,2つの説明可能なAI(xAI)フレームワークを適用した。
  論文  参考訳（メタデータ） (2024-08-19T09:39:01Z)
• Logicbreaks: A Framework for Understanding Subversion of Rule-based Inference [20.057611113206324]
  本研究では,大規模言語モデル (LLM) を早急に規定された規則に従う方法について検討する。 LLMはそのような規則を忠実に従えるが、悪意のあるプロンプトは理想化された理論的なモデルさえも誤解させる可能性があることを証明している。
  論文  参考訳（メタデータ） (2024-06-21T19:18:16Z)
• Logic Rules as Explanations for Legal Case Retrieval [9.240902132139187]
  本稿では,ケースレベルの論理則と法レベルの論理則を学習することで,訴訟の一致を推論する枠組みを提案する。 論理則の論理性と解釈性から、NS-LCRは忠実な説明性を備えている。
  論文  参考訳（メタデータ） (2024-03-03T09:22:21Z)
• Automated legal reasoning with discretion to act using s(LAW) [0.294944680995069]
  倫理的および法的懸念は、自動化された推論者が人間の理解可能な言葉で正当化する必要がある。 パターンのセットに従って曖昧な概念をモデル化するために、ASPを述語するためのトップダウン実行モデルであるs(CASP)を使うことを提案する。 我々は、s(LAW)と呼ばれるフレームワークを実装して、適用可能な法律をモデル化、理由付け、正当化し、代表的なユースケースを翻訳(およびベンチマーク)することでそれを検証しました。
  論文  参考訳（メタデータ） (2024-01-25T21:11:08Z)
• OPERA:Operation-Pivoted Discrete Reasoning over Text [33.36388276371693]
  OPERA(オペラ)は、機械読解のための操作駆動型離散推論フレームワークである。 推論能力と解釈可能性を促進するために、軽量なシンボル操作をニューラルモジュールとして使用する。 DROPとRACENumのデータセットの実験は、OPERAの推論能力を示している。
  論文  参考訳（メタデータ） (2022-04-29T15:41:47Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Automated Machine Learning, Bounded Rationality, and Rational Metareasoning [62.997667081978825]
  有界合理性の観点から、自動機械学習(AutoML)と関連する問題を考察する。 リソース境界の下でアクションを取るには、エージェントがこれらのリソースを最適な方法で利用する方法を反映する必要がある。
  論文  参考訳（メタデータ） (2021-09-10T09:10:20Z)
• CausalCity: Complex Simulations with Agency for Causal Discovery and Reasoning [68.74447489372037]
  本稿では,因果探索と反事実推論のためのアルゴリズムの開発を目的とした,高忠実度シミュレーション環境を提案する。 私たちの作業の中核となるコンポーネントは、複雑なシナリオを定義して作成することが簡単になるような、テキストの緊急性を導入することです。 我々は3つの最先端の手法による実験を行い、ベースラインを作成し、この環境の可利用性を強調する。
  論文  参考訳（メタデータ） (2021-06-25T00:21:41Z)
• On Exploiting Hitting Sets for Model Reconciliation [53.81101846598925]
  ヒューマン・アウェア・プランニングにおいて、プランニング・エージェントは、その計画がなぜ最適なのかを人間に説明する必要があるかもしれない。 この手法はモデル和解と呼ばれ、エージェントはモデルと人間のモデルの違いを調和させようとする。 我々は,計画の領域を超えて拡張されたモデル和解のための論理ベースのフレームワークを提案する。
  論文  参考訳（メタデータ） (2020-12-16T21:25:53Z)

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

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