論文の概要: Quantifying SMT Solver Instability for Formal Verification

• arxiv url: http://arxiv.org/abs/2610.12649v1
• Date: Thu, 08 Oct 2026 19:11:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-13 04:06:29.256364
• Title: Quantifying SMT Solver Instability for Formal Verification
• Title（参考訳）: 形式検証のためのSMTソルバー不安定性の定量化
• Abstract要約: ソフトウェア開発プロジェクトでは、プログラム検証が一般的になっています。 SMT不安定性(SMT instability)は、ソースコードの意味論的に等価な置換が解決または中断するのにはるかに長い時間がかかる現象である。 SMTの不安定性を測定するためのこれまでの努力は、それが生成する異常なランタイム分布のために定量化が困難であった。
• 参考スコア（独自算出の注目度）: 0.04369550829556577
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Program verification has become commonplace in software development projects, and much of its feasibility can be attributed to the potential of SMT solvers to automate model checking and other verification techniques. However, SMT instability, a phenomenon where semantically equivalent permutations of source code take much longer to solve or timeout, has been found to interrupt workflows and make software engineers more likely to avoid verification. Previous efforts to measure SMT instability have had difficulty quantifying it due to the abnormal runtime distributions it produces. In this paper, we use the coefficient of variation to model instability across an extensive dataset of SMT queries from three software domains. Our results show that SMT instability is significant in each area, and that it increases for queries that take longer on average. However, using a novel method to quantify instability, we show that a different approach is possible: if a solution were to optimize the structure of queries for runtime, rather than variance, instability could be mitigated while also improving overall solver performance.
• Abstract（参考訳）: プログラム検証はソフトウェア開発プロジェクトでは一般的になっており、その実現可能性の多くは、モデルチェックやその他の検証手法を自動化するSMTソルバの可能性に起因する。 しかし、SMTの不安定性は、ソースコードの意味論的に等価な置換が解決やタイムアウトにはるかに長い時間を要する現象であり、ワークフローを中断し、ソフトウェアエンジニアが検証を避けやすいようにしている。 SMTの不安定性を測定するためのこれまでの努力は、それが生成する異常なランタイム分布のために定量化が困難であった。 本稿では,3つのソフトウェア領域からのSMTクエリの広範囲なデータセットに対して,変動係数を用いて不安定性をモデル化する。 以上の結果から,SMTの不安定性は各領域で有意であり,平均よりも長いクエリが増加することが示唆された。 しかし,新しい手法を用いて不安定性を定量化することで,解法が分散ではなく実行時のクエリ構造を最適化するならば,不安定性を軽減できると同時に,全体的な解法性能も向上できることを示す。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。 我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
  論文  参考訳（メタデータ） (2026-04-26T14:34:49Z)
• Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic [2.8037951156321377]
  本稿では,FourierSMTを拡張性と並列性の高い連続変数最適化フレームワークとして導入する。 このフレームワークは、最大10,000変数と70万の制約で大規模なスケジューリングと配置の問題に対してベンチマークされており、8倍のスピードアップを実現している。
  論文  参考訳（メタデータ） (2026-03-24T07:22:30Z)
• Multi-Scale Finetuning for Encoder-based Time Series Foundation Models [67.95907033226585]
  時系列基礎モデル (TSFM) は, 時系列予測において印象的なゼロショット性能を示す。 直感的な微調整はパフォーマンスの向上をもたらすが、TSFMの能力を完全に活用するには不十分である、と我々は主張する。 マルチスケール・ファインタニング(MSFT)は,マルチスケール・モデリングをファインタニング・プロセスに明示的に統合する,シンプルながら汎用的なフレームワークである。
  論文  参考訳（メタデータ） (2025-06-17T01:06:01Z)
• A Comparative Study of SMT and MILP for the Nurse Rostering Problem [3.2117987125606517]
  本研究では,多種多様な実世界のスケジューリング制約をモデル化可能な汎用制約定式化を提案する。 我々は、学術的および現実世界にインスパイアされたロスター問題に関して、Z3 と Gurobi を比較した。
  論文  参考訳（メタデータ） (2025-05-15T14:12:39Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Considering Nonstationary within Multivariate Time Series with Variational Hierarchical Transformer for Forecasting [12.793705636683402]
  MTS内の非定常性と固有特性を考慮した強力な階層的確率的生成モジュールを開発した。 次に、階層時間系列変分変換器(HTV-Trans)という、明確に定義された変動生成動的モデルに対する変換器と組み合わせる。 HTV-Transは強力な確率モデルであり、MTSの表現表現を学習し、予測タスクに適用する。
  論文  参考訳（メタデータ） (2024-03-08T16:04:36Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。 我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。 本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
  論文  参考訳（メタデータ） (2022-06-15T11:39:45Z)

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

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