論文の概要: STL: Surprisingly Tricky Logic (for System Validation)

• arxiv url: http://arxiv.org/abs/2305.17258v1
• Date: Fri, 26 May 2023 21:01:26 GMT
• ステータス: 処理完了
• システム内更新日: 2023-05-30 20:52:01.985979
• Title: STL: Surprisingly Tricky Logic (for System Validation)
• Title（参考訳）: STL: 意外とトリッキーなロジック(システム検証用)
• Authors: Ho Chit Siu, Kevin Leahy, and Makai Mann
• Abstract要約: 検証正当性を決定する上では,仕様書の真正性,形式的手法に精通した被験者の親密性,教育水準が重要な要因であることが判明した。 参加者は肯定バイアスを示し、有効仕様の精度は大幅に向上したが、無効仕様の精度は著しく低下した。
• 参考スコア（独自算出の注目度）: 0.04301276597844757
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.
• Abstract（参考訳）: 自律システムの振る舞いを特定または学習するための形式的手法を開発する最近の研究の多くは、形式的仕様がシステムをチェックする際に人間にとって有用であるという信念に基づいている。 しばしば主張されるが、この仮定は滅多にテストされない。 人体実験(N = 62)を,前もって形式的手法に慣れていなかった人々を対象に実施し,信号時間論理(STL)の制約がエージェントに害を与えないようにし,グリッドワールド・キャプチャー・ザ・フラッグ・セッティングでタスクを完了させるかどうかを検証した。 検証精度は$45\% \pm 20\%$(平均$\pm$標準偏差)であった。 その結果, 仕様の真正性, 形式的手法に親しみ, 教育水準が, 検証正当性を決定する重要な要因であることが判明した。 被験者は肯定バイアスを示し,有効仕様の精度は著しく向上したが,無効仕様の精度は有意に低下した。 さらに、特に形式的手法に精通した参加者は、回答に過度に自信を持ち、実際の正確性に関係なく同様に自信を持つ傾向にあった。 私たちのデータは、形式的仕様は本質的に人間に解釈可能であり、システム検証に有意義な程度である、という信念をサポートしていません。 データ提示と検証トレーニングの人間工学的改善を推奨し、解釈可能性の主張が形式的な手法の文献に戻す前にテストすべきである。

関連論文リスト

• FactTest: Factuality Testing in Large Language Models with Finite-Sample and Distribution-Free Guarantees [41.78390564658645]
  幻覚や非現実的コンテンツを生成するための大規模言語モデル(LLM)は、高い領域での信頼性を損なう。 FactTest は LLM が与えられた質問に対する正しい回答を確実に提供できるかどうかを統計的に評価する新しいフレームワークである。 本研究では,FactTestが幻覚を効果的に検出し,未知の疑問に答えることを禁じるモデルの能力を向上させることにより,40%以上の精度向上を実現していることを示す。
  論文  参考訳（メタデータ） (2024-11-04T20:53:04Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  本研究では,自然言語フィードバック型検証器Math-Minosを提案する。 実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-06-20T06:42:27Z)
• Consistent Validation for Predictive Methods in Spatial Settings [17.44650272751289]
  空間予測タスクは 天気予報や大気汚染の研究 その他の科学的取り組みの鍵です 検証のための古典的なアプローチでは、バリデーションで利用可能な場所と、予測したい場所(テスト)の間のミスマッチを処理できません。 我々は、検証データが任意に密になるにつれて、検証が任意に正確になる検証方法を定式化する。
  論文  参考訳（メタデータ） (2024-02-05T21:33:22Z)
• Efficient Conformal Prediction under Data Heterogeneity [79.35418041861327]
  コンフォーマル予測(CP)は不確実性定量化のための頑健な枠組みである。 非交換性に対処するための既存のアプローチは、最も単純な例を超えて計算不可能なメソッドにつながる。 この研究は、比較的一般的な非交換可能なデータ分布に対して証明可能な信頼セットを生成する、CPに新しい効率的なアプローチを導入する。
  論文  参考訳（メタデータ） (2023-12-25T20:02:51Z)
• Understanding and Mitigating Classification Errors Through Interpretable Token Patterns [58.91023283103762]
  容易に解釈可能な用語でエラーを特徴付けることは、分類器が体系的なエラーを起こす傾向にあるかどうかを洞察する。 正しい予測と誤予測を区別するトークンのパターンを発見することを提案する。 提案手法であるPremiseが実際によく動作することを示す。
  論文  参考訳（メタデータ） (2023-11-18T00:24:26Z)
• Testing for Overfitting [0.0]
  オーバーフィッティング問題について議論し、トレーニングデータによる評価に標準値と集中値が成立しない理由を説明する。 本稿では,モデルの性能をトレーニングデータを用いて評価できる仮説テストを紹介し,議論する。
  論文  参考訳（メタデータ） (2023-05-09T22:49:55Z)
• CAFA: Class-Aware Feature Alignment for Test-Time Adaptation [50.26963784271912]
  テスト時間適応(TTA)は、テスト時にラベルのないデータにモデルを適応させることによって、この問題に対処することを目的としている。 本稿では,クラス認識特徴アライメント(CAFA, Class-Aware Feature Alignment)と呼ばれる単純な機能アライメント損失を提案する。
  論文  参考訳（メタデータ） (2022-06-01T03:02:07Z)
• Conformal prediction for the design problem [72.14982816083297]
  機械学習の現実的な展開では、次にテストすべきデータを選択するために予測アルゴリズムを使用します。 このような設定では、トレーニングデータとテストデータの間には、異なるタイプの分散シフトがある。 このような環境で予測の不確実性を定量化する手法を提案する。
  論文  参考訳（メタデータ） (2022-02-08T02:59:12Z)
• Exploring the Capacity of a Large-scale Masked Language Model to Recognize Grammatical Errors [3.55517579369797]
  トレーニングデータの5～10%は、BERTに基づく誤り検出法で、非言語モデルに基づく手法と同等の性能を実現するのに十分であることを示す。 また、擬似誤差データを用いて、様々な種類の誤りを認識するための学習ルールにおいて、実際にそのような優れた特性を示すことを示す。
  論文  参考訳（メタデータ） (2021-08-27T10:37:14Z)
• Information-Theoretic Probing with Minimum Description Length [74.29846942213445]
  我々は,最小記述長 (MDL) を持つ情報理論探索法である標準プローブの代替案を提案する。 MDL Probingでは、ラベルを予測するためのプローブのトレーニングが、データを効果的に送信するための教えとして再キャストされる。 これらの手法は結果に一致し、標準プローブよりも情報的かつ安定であることを示す。
  論文  参考訳（メタデータ） (2020-03-27T09:35:38Z)

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

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