論文の概要: Towards Comprehensive Sampling of SMT Solutions
- arxiv url: http://arxiv.org/abs/2511.10326v1
- Date: Fri, 14 Nov 2025 01:45:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-14 22:53:22.816315
- Title: Towards Comprehensive Sampling of SMT Solutions
- Title（参考訳）: SMTソリューションの総合サンプリングに向けて
- Authors: Shuangyu Lyu, Chuan Luo, Ruizhi Shi, Wei Wu, Chanjuan Liu, Chunming Hu,
- Abstract要約: PanSamplerは、少数のソリューションで高いカバレッジを実現する新しいSMTサンプリングシステムである。
多様性を意識したSMTアルゴリズム、抽象構文木(AST)誘導スコアリング機能、ポストサンプリング最適化技術という3つの新しい手法が組み込まれている。
パンサンプラーは高い対象範囲に到達する能力が著しく向上する一方で、同じカバレッジレベルを達成するために現在のサンプルよりも少ないソリューションを必要としている。
- 参考スコア（独自算出の注目度）: 17.952635077005144
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This work focuses on effectively generating diverse solutions for satisfiability modulo theories (SMT) formulas, targeting the theories of bit-vectors, arrays, and uninterpreted functions, which is a critical task in software and hardware testing. Generating diverse SMT solutions helps uncover faults and detect safety violations during the verification and testing process, resulting in the SMT sampling problem, i.e., constructing a small number of solutions while achieving comprehensive coverage of the constraint space. While high coverage is crucial for exploring system behaviors, reducing the number of solutions is of great importance, as excessive solutions increase testing time and resource usage, undermining efficiency. In this work, we introduce PanSampler, a novel SMT sampler that achieves high coverage with a small number of solutions. It incorporates three novel techniques, i.e., diversity-aware SMT algorithm, abstract syntax tree (AST)-guided scoring function and post-sampling optimization technology, enhancing its practical performance. It iteratively samples solutions, evaluates candidates, and employs local search to refine solutions, ensuring high coverage with a small number of samples. Extensive experiments on practical benchmarks demonstrate that PanSampler exhibits a significantly stronger capability to reach high target coverage, while requiring fewer solutions than current samplers to achieve the same coverage level. Furthermore, our empirical evaluation on practical subjects, which are collected from real-world software systems, shows that PanSampler achieves higher fault detection capability and reduces the number of required test cases from 32.6\% to 76.4\% to reach the same fault detection effectiveness, leading to a substantial improvement in testing efficiency. PanSampler advances SMT sampling, reducing the cost of software testing and hardware verification.
- Abstract（参考訳）: 本研究は、ビットベクトル、配列、非解釈関数の理論を対象とし、満足度変調理論(SMT)の公式に対する多様な解を効果的に生成することに焦点を当て、ソフトウェアおよびハードウェアテストにおいて重要な課題である。
多様なSMTソリューションの生成は、検証およびテストプロセス中に障害を発見し、安全違反を検出するのに役立つ。
システムの振る舞いを探索するためには、高いカバレッジが不可欠ですが、過剰なソリューションがテスト時間とリソース使用量を増やし、効率を損なうため、ソリューションの数を減らすことが非常に重要です。
本研究では,少数のソリューションで高いカバレッジを実現する新しいSMTサンプリングシステムであるPanSamplerを紹介する。
多様性を意識したSMTアルゴリズム、抽象構文木(AST)誘導スコアリング機能、およびポストサンプリング最適化技術という3つの新しい技術が組み込まれており、実用性能が向上している。
反復的に解をサンプリングし、候補を評価し、局所探索を用いて解を洗練し、少数のサンプルで高いカバレッジを確保する。
実用的なベンチマーク実験により、パンサンプラーは高い対象範囲に到達する能力が非常に強く、同じカバレッジレベルを達成するために現在のサンプルよりも少ない解を必要とすることが示された。
さらに,実世界のソフトウェアシステムから収集した実践的対象に対する実証的な評価から,パンサンプラーは高い故障検出能力を実現し,同じ故障検出効率に達するために必要なテストケースの数を32.6\%から76.4\%に削減し,テスト効率を大幅に向上させることを示した。
PanSamplerはSMTサンプリングを進歩させ、ソフトウェアテストとハードウェア検証のコストを削減した。
関連論文リスト
- DetectAnyLLM: Towards Generalizable and Robust Detection of Machine-Generated Text Across Domains and Models [60.713908578319256]
タスク指向の知識で検出器を最適化するために,DDL(Direct Discrepancy Learning)を提案する。
そこで本研究では,最新のMGTD性能を実現する統合検出フレームワークであるTectAnyLLMを紹介する。
MIRAGEは5つのテキストドメインにまたがる10のコーパスから人書きテキストをサンプリングし、17個の最先端のLLMを使用して再生成または修正する。
論文 参考訳（メタデータ） (2025-09-15T10:59:57Z) - Requirements Coverage-Guided Minimization for Natural Language Test Cases [7.947774587906927]
テストスイートはサイズが大きくなる傾向があり、しばしば冗長なテストケースを含んでいる。
テストスイートの最小化は、要件カバレッジや障害検出機能といった重要な特性を維持しながら、そのような冗長性を取り除くことを目的としている。
要件ベーステスト用に設計された新しいTSMアプローチであるRTM(Requirement coverage-guided Test suite Minimization)を提案する。
論文 参考訳（メタデータ） (2025-05-26T13:55:33Z) - Add-One-In: Incremental Sample Selection for Large Language Models via a Choice-Based Greedy Paradigm [50.492124556982674]
本稿では,新しい選択型サンプル選択フレームワークを提案する。
個々のサンプル品質の評価から、異なるサンプルのコントリビューション値の比較へと焦点をシフトする。
われわれのアプローチをより大きな医療データセットで検証し、現実の応用における実用性を強調した。
論文 参考訳（メタデータ） (2025-03-04T07:32:41Z) - SMT(LIA) Sampling with High Diversity [12.198700284977962]
我々はCDCL(T)技術と局所探索を統合した最初のサンプリングフレームワークを開発した。
HighDiv は線形整数論の下で制約に対する非常に多様な解の集合を生成することができる。
論文 参考訳（メタデータ） (2025-02-25T07:53:46Z) - FastMCTS: A Simple Sampling Strategy for Data Synthesis [67.60823802317141]
我々はモンテカルロ木探索にインスパイアされた革新的なデータ合成戦略であるFastMCTSを紹介する。
FastMCTSは、ステップレベルの評価信号を提供するマルチステップ推論データに対して、より効率的なサンプリング方法を提供する。
英語と中国語の両方の推論データセットの実験では、FastMCTSが30%以上の正しい推論パスを生成することが示されている。
論文 参考訳（メタデータ） (2025-02-17T06:27:57Z) - How Low Can We Go? Minimizing Interaction Samples for Configurable Systems [2.569213261297365]
提案手法は, 必要サンプルサイズに対して, ほぼ最適解と証明可能な下限を結合する枠組みである。
我々のアルゴリズムであるSampLNSは,85%のケースにおいて,従来手法よりも小型のサンプルを確実に見つけることができる。
これにより、研究者や実践者によるサンプルの最小化という面倒な作業を避けることができる。
論文 参考訳（メタデータ） (2025-01-12T12:02:26Z) - Faster Stochastic Variance Reduction Methods for Compositional MiniMax
Optimization [50.10952609321302]
合成ミニマックス最適化は、さまざまな機械学習領域において重要な課題である。
構成最小最適化の現在の方法は、最適以下の複雑さや、大きなバッチサイズに大きく依存することによって悩まされている。
本稿では,Nested STOchastic Recursive Momentum (NSTORM)と呼ばれる新しい手法を提案する。
論文 参考訳（メタデータ） (2023-08-18T14:57:21Z) - Towards Automated Imbalanced Learning with Deep Hierarchical
Reinforcement Learning [57.163525407022966]
不均衡学習はデータマイニングにおいて基本的な課題であり、各クラスにトレーニングサンプルの不均等な比率が存在する。
オーバーサンプリングは、少数民族のための合成サンプルを生成することによって、不均衡な学習に取り組む効果的な手法である。
我々は,異なるレベルの意思決定を共同で最適化できる自動オーバーサンプリングアルゴリズムであるAutoSMOTEを提案する。
論文 参考訳（メタデータ） (2022-08-26T04:28:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。