論文の概要: Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia

• arxiv url: http://arxiv.org/abs/2510.20514v1
• Date: Thu, 23 Oct 2025 12:59:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-25 03:08:17.926625
• Title: Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia
• Title（参考訳）: 実践的帰納的検証に向けて:産業・学界における質的研究から
• Authors: Lea Salome Brugger, Xavier Denis, Peter Müller,
• Abstract要約: 帰納的検証は、あるシステムが意図した振る舞いを公開することを保証する効果的な方法である。 選択したプロジェクトでは有効性や実現可能性があることが証明されているが、導出検証は依然として主流のテクニックではない。 本研究は, 導出検証を成功させる要因と, 広く普及しないための根本的課題について検討する。
• 参考スコア（独自算出の注目度）: 2.6359922261359716
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, deductive verification is still not a mainstream technique. To pave the way to widespread use, we present a study investigating the factors enabling successful applications of deductive verification and the underlying issues preventing broader adoption. We conducted semi-structured interviews with 30 practitioners of verification from both industry and academia and systematically analyzed the collected data employing a thematic analysis approach. Beside empirically confirming familiar challenges, e.g., the high level of expertise needed for conducting formal proofs, our data reveal several underexplored obstacles, such as proof maintenance, insufficient control over automation, and usability concerns. We further use the results from our data analysis to extract enablers and barriers for deductive verification and formulate concrete recommendations for practitioners, tool builders, and researchers, including principles for usability, automation, and integration with existing workflows.
• Abstract（参考訳）: 帰納的検証は、あるシステムが意図した振る舞いを公開することを保証する効果的な方法である。 選択したプロジェクトでは有効性や実現可能性があることが証明されているが、導出検証は依然として主流のテクニックではない。 本研究は, 提案手法を広く活用するために, 導出検証を成功させる要因と, 広く普及しないための根本的課題について検討する。 本研究は, 産学・産学両分野の検証実践者30人と半構造化インタビューを行い, テーマ分析手法を用いて収集したデータを体系的に分析した。 例えば、正式な証明を行うのに必要な高いレベルの専門知識を実証的に確認するだけでなく、我々のデータは、証明の保守、自動化の制御の不十分、ユーザビリティの懸念など、未調査のいくつかの障害を明らかにします。 データ分析の結果をさらに活用して、推論検証のためのイネーラやバリアを抽出し、ユーザビリティ、自動化、既存のワークフローとの統合といった原則を含む、実践者、ツールビルダー、研究者のための具体的なレコメンデーションを定式化しています。

関連論文リスト

• Towards Reliable Forgetting: A Survey on Machine Unlearning Verification [26.88376128769619]
  本稿では,機械学習の検証手法に関する最初の構造化された調査について述べる。 本稿では,現在の手法を行動検証とパラメトリック検証の2つの主要なカテゴリに分類する分類法を提案する。 基礎となる仮定、強度、限界を調べ、実践的なデプロイメントにおける潜在的な脆弱性を特定します。
  論文  参考訳（メタデータ） (2025-06-18T03:33:59Z)
• Measurement to Meaning: A Validity-Centered Framework for AI Evaluation [12.55408229639344]
  我々は、利用可能な証拠から得られる評価的クレームのタイプを推論するための構造化されたアプローチを提供する。 私たちのフレームワークは、機械学習の現代的なパラダイムに適しています。
  論文  参考訳（メタデータ） (2025-05-13T20:36:22Z)
• Advancing Embodied Agent Security: From Safety Benchmarks to Input Moderation [52.83870601473094]
  エンボディード・エージェントは、複数のドメインにまたがって大きな潜在能力を示す。 既存の研究は主に、一般的な大言語モデルのセキュリティに重点を置いている。 本稿では, エンボディエージェントの保護を目的とした新しい入力モデレーションフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-04-22T08:34:35Z)
• Understanding metric-related pitfalls in image analysis validation [59.15220116166561]
  この研究は、画像解析におけるバリデーションメトリクスに関連する落とし穴に関する情報にアクセスするための、初めての包括的な共通点を提供する。 バイオメディカル画像解析に焦点をあてるが、他の分野へ移行する可能性があるため、対処された落とし穴はアプリケーションドメイン全体にわたって一般化され、新しく作成されたドメインに依存しない分類に分類される。
  論文  参考訳（メタデータ） (2023-02-03T14:57:40Z)

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

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