Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models

要約

保証事例は、安全工学において製品の安全性を主張するために使用できます。
安全性が重要な領域では、保証ケースの構築が不可欠です。
信頼性導出ツリー (TDT) は、形式的な手法を組み込むことで保証ケースを強化し、保証ケースに関する自動推論を可能にします。
私たちは、TDT を自動的に構築および検証するように設計されたデスクトップ アプリケーションである Trustworthiness Derivation Tree Analyzer (Trusta) を紹介します。
このツールにはバックエンドに Prolog インタープリターが組み込まれており、制約ソルバー Z3 および MONA によってサポートされています。
したがって、算術、集合、ホーン節などを含む論理式に関する制約を解決できます。Trusta はまた、保証ケースの作成と評価をより便利にするために大規模な言語モデルも利用しています。
これにより、人間によるインタラクティブな検査と修正が可能になります。
保証ケースを生成するために、ChatGPT-3.5、ChatGPT-4、PaLM 2 などのトップ言語モデルを評価しました。
私たちのテストでは、機械が生成したケースと人間が作成したケースの間に 50% ～ 80% の類似性があることが示されました。
さらに、Trusta は自然言語のテキストから形式的制約を抽出できるため、解釈と検証のプロセスが容易になります。
この抽出は人間によるレビューと修正の対象となり、自動化された効率と人間の洞察を最大限に融合させます。
私たちの知る限り、これは保証ケースの自動作成と推論において大規模な言語モデルを初めて統合したものであり、従来の課題に新しいアプローチをもたらしました。
Trusta は、いくつかの業界ケーススタディを通じて、手動検査では通常見落とされるいくつかの微妙な問題を迅速に発見することを証明し、保証ケース開発プロセスを強化する上での実際的な価値を実証しました。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google