論文の概要: 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人と半構造化インタビューを行い, テーマ分析手法を用いて収集したデータを体系的に分析した。
例えば、正式な証明を行うのに必要な高いレベルの専門知識を実証的に確認するだけでなく、我々のデータは、証明の保守、自動化の制御の不十分、ユーザビリティの懸念など、未調査のいくつかの障害を明らかにします。
データ分析の結果をさらに活用して、推論検証のためのイネーラやバリアを抽出し、ユーザビリティ、自動化、既存のワークフローとの統合といった原則を含む、実践者、ツールビルダー、研究者のための具体的なレコメンデーションを定式化しています。
関連論文リスト
- Leveraging LLM Parametric Knowledge for Fact Checking without Retrieval [60.25608870901428]
信頼性は、大規模言語モデル(LLM)上に構築されたエージェントAIシステムの中核研究課題である
本研究では,任意の自然言語クレームの検証に焦点をあて,検索なしで事実チェックを行うタスクを提案する。
論文 参考訳（メタデータ） (2026-03-05T18:42:51Z) - An Investigation on How AI-Generated Responses Affect SoftwareEngineering Surveys [3.183470571353323]
本研究では,大規模言語モデル (LLM) がソフトウェア工学のサーベイでいかに誤用されているかを考察する。
我々は2025年にProlificプラットフォームを通じて行われた2回の調査からのデータを分析した。
ソフトウェア工学のサーベイにおいて、データの真正性は新たな妥当性の次元として認識される。
論文 参考訳（メタデータ） (2025-12-19T11:17:05Z) - Measuring what Matters: Construct Validity in Large Language Model Benchmarks [103.53142193393931]
大規模言語モデル(LLM)を評価することは、その能力を評価し、デプロイ前に安全性や堅牢性の問題を特定するために重要である。
自然言語処理と機械学習における主要なカンファレンスから445のベンチマークを体系的にレビューする。
結果の妥当性を損なう現象,課題,評価指標に関連するパターンを見いだす。
論文 参考訳（メタデータ） (2025-11-03T17:39:40Z) - Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
We present WebDetective, a benchmark of hint-free multi-hop questions with a control Wikipedia sandbox。
25の最先端モデルに対する我々の評価は、すべてのアーキテクチャにまたがる体系的な弱点を明らかにしている。
私たちはエージェントワークフローであるEvidenceLoopを開発し、ベンチマークが特定する課題を明示的にターゲットしています。
論文 参考訳（メタデータ） (2025-10-01T07:59:03Z) - AI-Driven Tools in Modern Software Quality Assurance: An Assessment of Benefits, Challenges, and Future Directions [0.0]
この研究は、現代のAI指向ツールを品質保証プロセスに統合するメリット、課題、および展望を評価することを目的としている。
この研究は、AIがQAに変革をもたらす可能性を実証しているが、これらの技術を実装するための戦略的アプローチの重要性を強調している。
論文 参考訳（メタデータ） (2025-06-19T20:22:47Z) - Towards Reliable Forgetting: A Survey on Machine Unlearning Verification [26.88376128769619]
本稿では,機械学習の検証手法に関する最初の構造化された調査について述べる。
本稿では,現在の手法を行動検証とパラメトリック検証の2つの主要なカテゴリに分類する分類法を提案する。
基礎となる仮定、強度、限界を調べ、実践的なデプロイメントにおける潜在的な脆弱性を特定します。
論文 参考訳（メタデータ） (2025-06-18T03:33:59Z) - Re-evaluation of Logical Specification in Behavioural Verification [0.0]
本研究では,行動モデルに対する自動論理仕様法を実証的に検証する。
自動推論における適応的性能不規則性の必要性を示唆する性能不規則性を特定する。
自己最適化解法によってこれらの非効率に対処することは、自動推論の安定性を高めることができる。
論文 参考訳（メタデータ） (2025-05-23T14:46:39Z) - 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) - Causality can systematically address the monsters under the bench(marks) [64.36592889550431]
ベンチマークはさまざまなバイアス、アーティファクト、リークに悩まされている。
モデルは、調査の不十分な障害モードのため、信頼できない振る舞いをする可能性がある。
因果関係はこれらの課題を体系的に解決するための 理想的な枠組みを提供します
論文 参考訳（メタデータ） (2025-02-07T17:01:37Z) - Understanding metric-related pitfalls in image analysis validation [59.15220116166561]
この研究は、画像解析におけるバリデーションメトリクスに関連する落とし穴に関する情報にアクセスするための、初めての包括的な共通点を提供する。
バイオメディカル画像解析に焦点をあてるが、他の分野へ移行する可能性があるため、対処された落とし穴はアプリケーションドメイン全体にわたって一般化され、新しく作成されたドメインに依存しない分類に分類される。
論文 参考訳（メタデータ） (2023-02-03T14:57:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。