論文の概要: Tunable Automation in Automated Program Verification

• arxiv url: http://arxiv.org/abs/2512.03926v1
• Date: Wed, 03 Dec 2025 16:27:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-04 20:02:55.368309
• Title: Tunable Automation in Automated Program Verification
• Title（参考訳）: 自動プログラム検証におけるTunable Automation
• Authors: Alexander Y. Bai, Chris Hawblitzel, Andrea Lattuada,
• Abstract要約: SMTベースの検証ツールは、量子化器のインスタンス化を扱う場合、自動化とパフォーマンスの緊張に直面する。 本稿では,検証コンテキストにおける量化事実の可利用性に対するきめ細かい制御を可能にする機構を提案する。 我々は、Rustベースの検証ツールであるVerusにテクニックを実装し、それを複数のオープンソースで評価しています。
• 参考スコア（独自算出の注目度）: 42.02726718338287
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Automated verification tools based on SMT solvers have made significant progress in verifying complex software systems. However, these tools face a fundamental tension between automation and performance when dealing with quantifier instantiation -- the primary source of incompleteness and verification slowdown in SMT-based verifiers. Tools choose between aggressive quantifier instantiation that provides more automation but longer verification times, or conservative instantiation that responds quickly but may require more manual proof hints. We present a mechanism that enables fine-grained control over the availability of quantified facts in verification contexts, allowing developers to selectively tune the level of automation. Our approach lets library authors provide different pre-defined automation levels while giving end-users the ability to further customize quantifier availability at the module, function, or proof context level. We implement our techniques in Verus, a Rust-based verification tool, and evaluate them on multiple openly available codebases. Our empirical analysis demonstrates the automation-performance tradeoff and that selective quantifier management enables developers to select the appropriate level of automation in different contexts.
• Abstract（参考訳）: SMTソルバに基づく自動検証ツールは、複雑なソフトウェアシステムの検証に大きな進歩をもたらした。 しかしながら、これらのツールは、定量化器のインスタンス化を扱う際に、自動化とパフォーマンスの根本的な緊張に直面する。 ツールは、より自動化されているが、より長い検証時間を提供するアグレッシブな定量化と、素早く応答するがより手動の証明ヒントを必要とする保守的なインスタンス化のどちらかを選択する。 本稿では,検証コンテキストにおける定量化事実の可用性を詳細に制御し,開発者が自動化レベルを選択的に調整できる機構を提案する。 当社のアプローチでは,ライブラリの作者が定義済みのさまざまな自動化レベルを提供しながら,モジュールや関数,あるいは証明コンテキストレベルでの定量化の可用性をさらにカスタマイズすることが可能になる。 私たちはRustベースの検証ツールであるVerusでテクニックを実装し、複数のオープンソースコードベースで評価しています。 我々の実証分析は、自動化と性能のトレードオフを実証し、選択量化器の管理により、開発者は異なる文脈で適切なレベルの自動化を選択できることを示した。

関連論文リスト

• Auditable DevOps Automation via VSM and GQM [0.0]
  本稿では、エンドツーエンドの配信システムを可視化し、遅延、リワーク、ハンドオフを定量化する統合フレームワークである textitVSM-GQM-DevOps を提案する。 このフレームワークは、観測された無駄からゴールに沿った質問、メトリクス、自動化候補まで、トレーサビリティを運用し、防御可能な優先順位付けアプローチを提供する。
  論文  参考訳（メタデータ） (2026-01-07T04:36:24Z)
• AutoEDA: Enabling EDA Flow Automation through Microservice-Based LLM Agents [15.41283323575065]
  AutoEDAは、標準化されたスケーラブルな自然言語エクスペリエンスに特化したモデルコンテキストプロトコル(MCP)を通じて並列学習を活用する、EDA自動化のためのフレームワークである。 実験の結果、既存の手法と比較して、自動化の精度と効率が向上し、スクリプトの品質も向上した。
  論文  参考訳（メタデータ） (2025-08-01T18:23:57Z)
• AutoAct: Automatic Agent Learning from Scratch for QA via Self-Planning [54.47116888545878]
  AutoActはQAのための自動エージェント学習フレームワークである。 大規模アノテートデータやクローズドソースモデルからの合成計画軌道は依存していない。
  論文  参考訳（メタデータ） (2024-01-10T16:57:24Z)
• TaskBench: Benchmarking Large Language Models for Task Automation [82.2932794189585]
  タスク自動化における大規模言語モデル(LLM)の機能を評価するためのフレームワークであるTaskBenchを紹介する。 具体的には、タスクの分解、ツールの選択、パラメータ予測を評価する。 提案手法は, 自動構築と厳密な人的検証を組み合わせることで, 人的評価との整合性を確保する。
  論文  参考訳（メタデータ） (2023-11-30T18:02:44Z)
• Lemur: Integrating Large Language Models in Automated Program Verification [10.221822902660458]
  自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 本稿では,音声自動検証手法として計算をインスタンス化し,一連の合成および競合ベンチマークの実践的改善を実証する。
  論文  参考訳（メタデータ） (2023-10-07T16:44:53Z)
• The Devil is in the Errors: Leveraging Large Language Models for Fine-grained Machine Translation Evaluation [93.01964988474755]
  AutoMQMは,大規模な言語モデルに対して,翻訳におけるエラーの識別と分類を求めるプロンプト技術である。 テキスト内学習と微調整によるラベル付きデータの影響について検討する。 次に, PaLM-2モデルを用いてAutoMQMを評価し, スコアのプロンプトよりも性能が向上することがわかった。
  論文  参考訳（メタデータ） (2023-08-14T17:17:21Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• Unsupervised Automata Learning via Discrete Optimization [4.5726613073750135]
  与えられたラベルなし単語の多元集合から決定論的有限オートマトン(DFA)を学習するためのフレームワークを提案する。 この問題は計算的に困難であることが示され,制約最適化に基づく3つの学習アルゴリズムが開発された。 DFAの全体的な解釈性を改善するため,最適化問題に対する新たな正規化手法を導入する。
  論文  参考訳（メタデータ） (2023-03-24T16:19:15Z)
• Automated Machine Learning Techniques for Data Streams [91.3755431537592]
  本稿では、最先端のオープンソースAutoMLツールを調査し、ストリームから収集したデータに適用し、時間とともにパフォーマンスがどのように変化するかを測定する。 この結果から,既製のAutoMLツールで十分な結果が得られることが示されたが,概念ドリフトや検出,適応といった手法が適用されれば,予測精度を時間とともに維持することが可能になる。
  論文  参考訳（メタデータ） (2021-06-14T11:42:46Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。 ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。 サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
  論文  参考訳（メタデータ） (2020-09-08T16:42:55Z)

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

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