STL: Surprisingly Tricky Logic (for System Validation)

要約

自律システムの動作を指定または学習するための形式的手法技術を開発する最近の研究の多くは、形式的仕様は解釈可能であり、システムをチェックするときに人間にとって役立つという信念に基づいています。
この仮定は頻繁に主張されていますが、検証されることはほとんどありません。
私たちは、事前に形式的手法に精通している人々とそうでない人々を混合して人体実験 (N = 62) を実施し、一連の信号時相論理 (STL) 制約がエージェントを危害から守り、攻撃を許可するかどうかを検証してもらいました。
グリッドワールドのキャプチャ ザ フラグ設定でタスクを完了するために使用します。
検証精度は $45\% \pm 20\%$ (平均 $\pm$ 標準偏差) でした。
仕様のグラウンドトゥルースの妥当性、被験者の形式的手法への精通度、および被験者の教育レベルが、検証の正しさを決定する重要な要素であることが判明しました。
参加者は肯定バイアスを示し、有効な仕様については精度が大幅に向上しましたが、無効な仕様については精度が大幅に低下しました。
さらに、参加者、特に形式的な手法に慣れている参加者は、自分の答えに自信過剰になる傾向があり、実際の正しさに関係なく同様に自信を持っています。
私たちのデータは、正式な仕様が本質的にシステムの検証に意味のある程度まで人間によって解釈可能であるという信念を裏付けていません。
データの表示と検証のトレーニングを人間工学に基づいて改善することをお勧めします。解釈可能性の主張が正式な手法の文献に戻る前にテストする必要があります。

要約(オリジナル)

Much of the recent work developing formal methods techniques to specify or learn the behavior of autonomous systems is predicated on a belief that formal specifications are interpretable and useful for humans when checking systems. Though frequently asserted, this assumption is rarely tested. We performed a human experiment (N = 62) with a mix of people who were and were not familiar with formal methods beforehand, asking them to validate whether a set of signal temporal logic (STL) constraints would keep an agent out of harm and allow it to complete a task in a gridworld capture-the-flag setting. Validation accuracy was $45\% \pm 20\%$ (mean $\pm$ standard deviation). The ground-truth validity of a specification, subjects’ familiarity with formal methods, and subjects’ level of education were found to be significant factors in determining validation correctness. Participants exhibited an affirmation bias, causing significantly increased accuracy on valid specifications, but significantly decreased accuracy on invalid specifications. Additionally, participants, particularly those familiar with formal methods, tended to be overconfident in their answers, and be similarly confident regardless of actual correctness. Our data do not support the belief that formal specifications are inherently human-interpretable to a meaningful degree for system validation. We recommend ergonomic improvements to data presentation and validation training, which should be tested before claims of interpretability make their way back into the formal methods literature.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google