論文の概要: 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は自然言語のテキストから形式的な制約を抽出でき、解釈と検証のプロセスが容易になる。
この抽出は、人間のレビューと修正の対象であり、自動化された効率と人間の洞察を混ぜ合わせています。
私たちの知る限り、これは保証ケースの自動作成と推論における大規模な言語モデルの初めての統合であり、従来の課題に新しいアプローチをもたらす。
インダストリアルケーススタディを通じて、トラスタは手動検査で見落とされる微妙な問題を素早く発見し、保証ケースの開発プロセスを強化する実践的な価値を証明した。
関連論文リスト
- 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。
3DGenはテストスイートに準拠した3D仕様を生成する。
論文 参考訳(メタデータ) (2024-04-16T07:53:28Z) - Exploring Safety Generalization Challenges of Large Language Models via Code [126.80573601180411]
本稿では,自然言語入力をコード入力に変換するフレームワークであるCodeAttackを紹介する。
我々の研究は、コード入力に対するこれらのモデルの共通の安全性の脆弱性を明らかにした。
CodeAttackと自然言語の分布ギャップが大きくなると、安全性の一般化が弱くなる。
論文 参考訳(メタデータ) (2024-03-12T17:55:38Z) - Emulated Disalignment: Safety Alignment for Large Language Models May Backfire! [65.06450319194454]
大規模言語モデル(LLM)は、人間との安全な会話を確保するために安全アライメントを行う必要がある。
本稿では,安全アライメントを逆転し,有害な言語モデルを生成することを実証する推論時アタック手法を提案する。
論文 参考訳(メタデータ) (2024-02-19T18:16:51Z) - 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) - Safety Analysis in the Era of Large Language Models: A Case Study of
STPA using ChatGPT [11.27440170845105]
人間の介入なしにChatGPTを使用することは、信頼性に関する問題が原因で不十分になるかもしれないが、慎重に設計すれば、人間の専門家より優れる可能性がある。
意味的複雑さの変化や、一般的なプロンプトガイドラインの使用において、統計的に有意な違いは見つからない。
論文 参考訳(メタデータ) (2023-04-03T16:46:49Z) - On the Reliability and Explainability of Language Models for Program
Generation [15.569926313298337]
自動プログラム生成手法の能力と限界について検討する。
私たちは、コード変換に大きく貢献するトークンを強調するために、高度な説明可能なAIアプローチを採用しています。
解析の結果,言語モデルではコード文法や構造情報を認識できるが,入力シーケンスの変化に対するロバスト性は限られていることがわかった。
論文 参考訳(メタデータ) (2023-02-19T14:59:52Z) - A Survey on Uncertainty Toolkits for Deep Learning [3.113304966059062]
ディープラーニング(DL)における不確実性推定のためのツールキットに関する第1回調査について述べる。
モデリングおよび評価能力に関する11のツールキットについて検討する。
最初の2つは、それぞれのフレームワークに大きな柔軟性とシームレスな統合を提供するが、最後の2つは、より大きな方法論的スコープを持っている。
論文 参考訳(メタデータ) (2022-05-02T17:23:06Z) - LaMDA: Language Models for Dialog Applications [75.75051929981933]
LaMDAは、ダイアログに特化したトランスフォーマーベースのニューラルネットワークモデルのファミリーである。
注釈付きデータで微調整し、モデルが外部の知識ソースを参照できるようにすると、大幅な改善がもたらされる。
論文 参考訳(メタデータ) (2022-01-20T15:44:37Z) - TextFlint: Unified Multilingual Robustness Evaluation Toolkit for
Natural Language Processing [73.16475763422446]
NLPタスク(TextFlint)のための多言語ロバスト性評価プラットフォームを提案する。
普遍的なテキスト変換、タスク固有の変換、敵攻撃、サブポピュレーション、およびそれらの組み合わせを取り入れ、包括的な堅牢性分析を提供する。
TextFlintは、モデルの堅牢性の欠点に対処するために、完全な分析レポートとターゲットとした拡張データを生成します。
論文 参考訳(メタデータ) (2021-03-21T17:20:38Z) - Efficient statistical validation with edge cases to evaluate Highly
Automated Vehicles [6.198523595657983]
自動運転車の大規模展開は、まだ解決されていない多くの安全上の課題にもかかわらず、差し迫っているようだ。
既存の標準は、検証が要求をカバーするテストケースのセットだけを必要とする決定論的プロセスに焦点を当てています。
本稿では, 自動生成テストケースを最悪のシナリオに偏り付け, システムの挙動の統計的特性を計算するための新しい手法を提案する。
論文 参考訳(メタデータ) (2020-03-04T04:35:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。