論文の概要: 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 12:00:26.05403
• 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:
• 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でテクニックを実装し、複数のオープンソースコードベースで評価しています。 我々の実証分析は、自動化と性能のトレードオフを実証し、選択量化器の管理により、開発者は異なる文脈で適切なレベルの自動化を選択できることを示した。

関連論文リスト

• 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)
• 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)

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

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