論文の概要: Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models

• arxiv url: http://arxiv.org/abs/2309.12941v1
• Date: Fri, 22 Sep 2023 15:42:43 GMT
• ステータス: 処理完了
• システム内更新日: 2023-09-25 13:58:28.951081
• Title: Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models
• Title（参考訳）: trusta: 形式的手法と大規模言語モデルによる保証ケースの推論
• Authors: Zezhong Chen, Yuxin Deng, Wenjie Du
• Abstract要約: Trustworthiness Derivation Tree Analyzer (Trusta)は、TDTを自動構築し検証するデスクトップアプリケーションである。 バックエンドにはPrologインタプリタが内蔵されており、制約解決器Z3とMONAによってサポートされている。 Trustaは自然言語のテキストから形式的な制約を抽出し、解釈と検証を容易にする。
• 参考スコア（独自算出の注目度）: 4.005483185111992
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Assurance cases can be used to argue for the safety of products in safety engineering. In safety-critical areas, the construction of assurance cases is indispensable. Trustworthiness Derivation Trees (TDTs) enhance assurance cases by incorporating formal methods, rendering it possible for automatic reasoning about assurance cases. We present Trustworthiness Derivation Tree Analyzer (Trusta), a desktop application designed to automatically construct and verify TDTs. The tool has a built-in Prolog interpreter in its backend, and is supported by the constraint solvers Z3 and MONA. Therefore, it can solve constraints about logical formulas involving arithmetic, sets, Horn clauses etc. Trusta also utilizes large language models to make the creation and evaluation of assurance cases more convenient. It allows for interactive human examination and modification. We evaluated top language models like ChatGPT-3.5, ChatGPT-4, and PaLM 2 for generating assurance cases. Our tests showed a 50%-80% similarity between machine-generated and human-created cases. In addition, Trusta can extract formal constraints from text in natural languages, facilitating an easier interpretation and validation process. This extraction is subject to human review and correction, blending the best of automated efficiency with human insight. To our knowledge, this marks the first integration of large language models in automatic creating and reasoning about assurance cases, bringing a novel approach to a traditional challenge. Through several industrial case studies, Trusta has proven to quickly find some subtle issues that are typically missed in manual inspection, demonstrating its practical value in enhancing the assurance case development process.
• Abstract（参考訳）: 保証ケースは、安全工学における製品の安全性を主張するのに使用できる。 安全クリティカルな地域では、保証ケースの構築は不可欠である。 TDT(Trustworthiness Derivation Trees)は、形式的手法を取り入れた保証ケースを強化し、保証ケースに関する自動推論を可能にする。 我々は,tdtの自動構築と検証を目的としたデスクトップアプリケーションであるtrusta(trustworthiness derivation tree analyzer)を提案する。 このツールはバックエンドにprologインタプリタを内蔵しており、制約解決ツールz3とmonaがサポートしている。 したがって、算術、集合、ホーン節などを含む論理式に関する制約を解くことができる。 Trustaはまた、大きな言語モデルを使用して、保証ケースの作成と評価をより便利にする。 対話的な人間による検査と修正が可能である。 chatgpt-3.5,chatgpt-4,palm 2などの言語モデルを用いて保証ケースの生成を行った。 実験では, マシン生成症例とヒト生成症例の50%-80%の類似性を示した。 加えて、trustaは自然言語のテキストから形式的な制約を抽出でき、解釈と検証のプロセスが容易になる。 この抽出は、人間のレビューと修正の対象であり、自動化された効率と人間の洞察を混ぜ合わせています。 私たちの知る限り、これは保証ケースの自動作成と推論における大規模な言語モデルの初めての統合であり、従来の課題に新しいアプローチをもたらす。 インダストリアルケーススタディを通じて、トラスタは手動検査で見落とされる微妙な問題を素早く発見し、保証ケースの開発プロセスを強化する実践的な価値を証明した。

関連論文リスト

• Automatic Instantiation of Assurance Cases from Patterns Using Large Language Models [6.314768437420443]
  大きな言語モデル(LLM)は、特定のパターンに従う保証ケースを生成することができる。 LLMは保証ケースの自動生成の可能性を秘めているが、その能力は人間の専門家と比べても劣っている。
  論文  参考訳（メタデータ） (2024-10-07T20:58:29Z)
• FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows" [74.7488607599921]
  FaithEvalは、コンテキストシナリオにおける大規模言語モデル(LLM)の忠実度を評価するためのベンチマークである。 FaithEvalは4.9Kの高品質な問題で構成され、厳格な4段階のコンテキスト構築と検証フレームワークを通じて検証されている。
  論文  参考訳（メタデータ） (2024-09-30T06:27:53Z)
• Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP [1.2189422792863451]
  本稿では, セマンティックルールに基づく分析機能を備えた Assurance 2.0 の拡張手法を提案する。 本稿では, 論理的整合性, 妥当性, 不整合性など, 保証事例のユニークな意味的側面について考察する。
  論文  参考訳（メタデータ） (2024-08-21T15:22:43Z)
• Automatic Generation of Behavioral Test Cases For Natural Language Processing Using Clustering and Prompting [6.938766764201549]
  本稿では,大規模言語モデルと統計的手法の力を活用したテストケースの自動開発手法を提案する。 4つの異なる分類アルゴリズムを用いて行動テストプロファイルを分析し、それらのモデルの限界と強みについて議論する。
  論文  参考訳（メタデータ） (2024-07-31T21:12:21Z)
• What Makes and Breaks Safety Fine-tuning? A Mechanistic Study [64.9691741899956]
  安全性の微調整は、大規模な言語モデル(LLM)を、安全なデプロイメントのための人間の好みに合わせるのに役立つ。 安全でない入力の健全な側面をキャプチャする合成データ生成フレームワークを設計する。 これを用いて,3つのよく知られた安全微調整手法について検討する。
  論文  参考訳（メタデータ） (2024-07-14T16:12:57Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal Behaviors [64.9938658716425]
  安全でないユーザリクエストを認識して拒否する、大規模な言語モデル(LLM)の既存の評価は、3つの制限に直面している。 まず、既存の手法では、安全でないトピックの粗い粒度を使い、いくつかのきめ細かいトピックを過剰に表現している。 第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。 第3に、既存の評価は大きなLCMに頼っているため、コストがかかる可能性がある。
  論文  参考訳（メタデータ） (2024-06-20T17:56:07Z)
• ASSERT: Automated Safety Scenario Red Teaming for Evaluating the Robustness of Large Language Models [65.79770974145983]
  ASSERT、Automated Safety Scenario Red Teamingは、セマンティックなアグリゲーション、ターゲットブートストラップ、敵の知識注入という3つの方法で構成されている。 このプロンプトを4つの安全領域に分割し、ドメインがモデルの性能にどのように影響するかを詳細に分析する。 統計的に有意な性能差は, 意味的関連シナリオにおける絶対分類精度が最大11%, ゼロショット逆数設定では最大19%の絶対誤差率であることがわかった。
  論文  参考訳（メタデータ） (2023-10-14T17:10:28Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。 大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
  論文  参考訳（メタデータ） (2023-07-25T14:20:51Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• On the Reliability and Explainability of Language Models for Program Generation [15.569926313298337]
  自動プログラム生成手法の能力と限界について検討する。 私たちは、コード変換に大きく貢献するトークンを強調するために、高度な説明可能なAIアプローチを採用しています。 解析の結果,言語モデルではコード文法や構造情報を認識できるが,入力シーケンスの変化に対するロバスト性は限られていることがわかった。
  論文  参考訳（メタデータ） (2023-02-19T14:59:52Z)
• LaMDA: Language Models for Dialog Applications [75.75051929981933]
  LaMDAは、ダイアログに特化したトランスフォーマーベースのニューラルネットワークモデルのファミリーである。 注釈付きデータで微調整し、モデルが外部の知識ソースを参照できるようにすると、大幅な改善がもたらされる。
  論文  参考訳（メタデータ） (2022-01-20T15:44:37Z)

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

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