論文の概要: Bringing freedom in variable choice when searching counter-examples in
floating point programs
- arxiv url: http://arxiv.org/abs/2002.12447v1
- Date: Thu, 27 Feb 2020 21:20:38 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-28 08:51:01.029418
- Title: Bringing freedom in variable choice when searching counter-examples in
floating point programs
- Title(参考訳): 浮動小数点プログラムにおける反例探索における変数選択の自由度
- Authors: Heytem Zitoun, Claude Michel, Laurent Michel, Michel Rueher
- Abstract要約: 本稿では,浮動小数点数制約システムを用いたCSPの探索戦略に焦点を当てた。
最先端の戦略を上回り、世界規模の発生件数に基づく新しい検索を導入する。
- 参考スコア(独自算出の注目度): 0.5161531917413706
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Program verification techniques typically focus on finding counter-examples
that violate properties of a program. Constraint programming offers a
convenient way to verify programs by modeling their state transformations and
specifying searches that seek counter-examples. Floating-point computations
present additional challenges for verification given the semantic subtleties of
floating point arithmetic. % This paper focuses on search strategies for CSPs
using floating point numbers constraint systems and dedicated to program
verification. It introduces a new search heuristic based on the global number
of occurrences that outperforms state-of-the-art strategies. More importantly,
it demonstrates that a new technique that only branches on input variables of
the verified program improve performance. It composes with a diversification
technique that prevents the selection of the same variable within a fixed
horizon further improving performances and reduces disparities between various
variable choice heuristics. The result is a robust methodology that can tailor
the search strategy according to the sought properties of the counter example.
- Abstract(参考訳): プログラム検証技術は通常、プログラムの特性に反する反例を見つけることに焦点を当てる。
制約プログラミングは、状態変換をモデル化し、反例を求める検索を指定することで、プログラムを検証する便利な方法を提供する。
浮動小数点演算は浮動小数点演算の意味的な微妙な性質から検証のための追加の課題を与える。
本論文は,浮動小数点数制約システムを用いたCSPの探索戦略とプログラム検証に焦点をあてる。
最先端戦略を上回り、グローバルな発生回数に基づく新たな検索ヒューリスティックを導入する。
さらに重要なことは、検証されたプログラムの入力変数のみを分岐する新しい手法が性能を向上させることである。
これは、固定地平線内で同じ変数の選択を防止し、さらに性能を改善し、様々な変数選択ヒューリスティック間の格差を低減する、多様化技術で構成される。
その結果, 提案手法は, 探索戦略を, 対向例の検索特性に応じて調整できるロバストな手法である。
関連論文リスト
- Variable Substitution and Bilinear Programming for Aligning Partially Overlapping Point Sets [48.1015832267945]
本研究では,RPMアルゴリズムの最小化目的関数を用いて要求を満たす手法を提案する。
分岐とバウンド(BnB)アルゴリズムが考案され、パラメータのみに分岐し、収束率を高める。
実験による評価は,非剛性変形,位置雑音,外れ値に対する提案手法の高剛性を示す。
論文 参考訳(メタデータ) (2024-05-14T13:28:57Z) - Spurious Feature Eraser: Stabilizing Test-Time Adaptation for Vision-Language Foundation Model [86.9619638550683]
視覚言語基礎モデルは、画像とテキストのペアデータに拡張性があるため、多数の下流タスクで顕著な成功を収めている。
しかし、これらのモデルは、決定ショートカットの結果、きめ細かな画像分類などの下流タスクに適用した場合に重大な制限を呈する」。
論文 参考訳(メタデータ) (2024-03-01T09:01:53Z) - Weakly Supervised Semantic Parsing with Execution-based Spurious Program
Filtering [19.96076749160955]
本稿では,プログラムの実行結果に基づくドメインに依存しないフィルタリング機構を提案する。
私たちはこれらの表現に対して多数決を行い、他のプログラムと大きく異なる意味を持つプログラムを特定し、フィルタリングします。
論文 参考訳(メタデータ) (2023-11-02T11:45:40Z) - Randomized Adversarial Style Perturbations for Domain Generalization [49.888364462991234]
本稿では,RASP(Randomized Adversarial Style Perturbation)と呼ばれる新しい領域一般化手法を提案する。
提案アルゴリズムは, ランダムに選択されたクラスに対して, 対角方向の特徴のスタイルを乱し, 予期せぬ対象領域で観測される予期せぬスタイルに誤解されないよう, モデルを学習させる。
提案アルゴリズムは,様々なベンチマークによる広範な実験により評価され,特に大規模ベンチマークにおいて,領域一般化性能が向上することを示す。
論文 参考訳(メタデータ) (2023-04-04T17:07:06Z) - Budgeted Classification with Rejection: An Evolutionary Method with
Multiple Objectives [0.0]
予算付きシーケンシャル分類器(BSC)プロセスは、部分的特徴取得と評価ステップのシーケンスを通じて入力を行う。
これにより、不要な特徴取得を防止するための入力の効率的な評価が可能になる。
本稿では,信頼度に基づく拒否オプション付き逐次分類器を構築するための問題固有遺伝的アルゴリズムを提案する。
論文 参考訳(メタデータ) (2022-05-01T22:05:16Z) - Flipping the switch on local exploration: Genetic Algorithms with
Reversals [0.0]
著者らは、勾配のない探索手法が離散領域における最適解を提供するのに適していることを示した。
また、複数のローカル検索を使用することで、ローカル検索のパフォーマンスが向上することを示した。
提案したGA変種は,提案した問題を含む全てのベンチマークにおいて,最小平均コストであり,ICが構成成分よりも優れた性能を発揮することが観察された。
論文 参考訳(メタデータ) (2022-02-02T08:27:11Z) - Joint Contrastive Learning with Infinite Possibilities [114.45811348666898]
本稿では,新しい確率論的モデリングによるコントラスト学習における最近の発展の有用性について考察する。
コントラスト学習(Joint Contrastive Learning, JCL)という,コントラスト学習の特定の形態を導出する。
論文 参考訳(メタデータ) (2020-09-30T16:24:21Z) - Variance-Reduced Off-Policy Memory-Efficient Policy Search [61.23789485979057]
政治政策の最適化は強化学習において難しい問題である。
オフポリシーアルゴリズムはメモリ効率が高く、オフポリシーサンプルから学ぶことができる。
論文 参考訳(メタデータ) (2020-09-14T16:22:46Z) - Change Point Detection in Time Series Data using Autoencoders with a
Time-Invariant Representation [69.34035527763916]
変化点検出(CPD)は、時系列データにおける急激な特性変化を見つけることを目的としている。
近年のCDD法は、深層学習技術を用いる可能性を示したが、信号の自己相関統計学におけるより微妙な変化を識別する能力に欠けることが多い。
我々は、新しい損失関数を持つオートエンコーダに基づく手法を用い、使用済みオートエンコーダは、CDDに適した部分的な時間不変表現を学習する。
論文 参考訳(メタデータ) (2020-08-21T15:03:21Z) - Learning Differentiable Programs with Admissible Neural Heuristics [43.54820901841979]
ドメイン固有言語におけるプログラムとして表現される微分可能関数の学習問題について検討する。
我々は、この最適化問題を、プログラム構文のトップダウン導出を符号化した重み付きグラフの探索として構成する。
私たちの重要なイノベーションは、さまざまなニューラルネットワークのクラスを、プログラムの空間上の連続的な緩和と見なすことです。
論文 参考訳(メタデータ) (2020-07-23T16:07:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。