論文の概要: Data-driven Verification of Procedural Programs with Integer Arrays

• arxiv url: http://arxiv.org/abs/2505.15958v1
• Date: Wed, 21 May 2025 19:19:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-23 17:12:47.880654
• Title: Data-driven Verification of Procedural Programs with Integer Arrays
• Title（参考訳）: 整数アレーを用いた手続き型プログラムのデータ駆動検証
• Authors: Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl,
• Abstract要約: 整数のパラメトリックサイズ配列を操作する手続きプログラムを自動検証する問題に対処する。 本稿では,ループ不変量と手続き前/後条件を合成するアルゴリズムを提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a powerful learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers. The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.
• Abstract（参考訳）: 本稿では,制約付きホーン節解決問題として符号化された整数のパラメトリックサイズ配列を操作する手続きプログラムの自動検証の問題に対処する。 配列要素とプログラム変数を制約する一階述語論理式として表現されたループ不変量と手続き前/後条件を合成するアルゴリズムを提案する。 私たちは、配列を処理するために決定ツリーHhorn-ICEフレームワークを拡張するデータ駆動アプローチを採用しています。 整数列のベクトルの複雑な分類問題を、整数列のベクトルのより単純な分類問題に還元する強力な学習手法を提案する。 得られた分類器は、普遍的に定量化された不変量と手続き前/後条件を得るように一般化される。 我々は,本手法を実装し,その効率性と競争性について,有意なベンチマークで検証した。

関連論文リスト

• Accelerating Cutting-Plane Algorithms via Reinforcement Learning Surrogates [49.84541884653309]
  凸離散最適化問題に対する現在の標準的なアプローチは、カットプレーンアルゴリズムを使うことである。 多くの汎用カット生成アルゴリズムが存在するにもかかわらず、大規模な離散最適化問題は、難易度に悩まされ続けている。 そこで本研究では,強化学習による切削平面アルゴリズムの高速化手法を提案する。
  論文  参考訳（メタデータ） (2023-07-17T20:11:56Z)
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes [0.0]
  数値不変合成と検証のためのデータ駆動アルゴリズムを提案する。 このアルゴリズムは、正および負の状態のサンプルから決定木を学習するためのICE-DTスキーマに基づいている。
  論文  参考訳（メタデータ） (2022-05-30T09:18:37Z)
• Structural Analysis of Branch-and-Cut and the Learnability of Gomory Mixed Integer Cuts [88.94020638263467]
  ブランチ・アンド・カット(ブランチ・アンド・カット)として知られる分岐・アンド・バウンドアルゴリズムにおける切断平面の組み入れは、現代の整数計画解法のバックボーンを形成する。 入力整数プログラムに付加される切断平面を定義するパラメータの変化により、アルゴリズムの各ステップがどのように影響を受けるかをピン留めする、分岐切断の新たな構造解析を行う。 この分析の主な応用は、機械学習を用いてブランチ・アンド・カット時にどの切断面を適用するかを決定するためのサンプルの複雑性保証を導出することである。
  論文  参考訳（メタデータ） (2022-04-15T03:32:40Z)
• Accelerating ERM for data-driven algorithm design using output-sensitive techniques [26.32088674030797]
  データ駆動型アルゴリズム設計のための効率的な学習アルゴリズムを開発するための技術について研究する。 提案手法は,超平面の集合によって誘導されるポリトープを列挙する出力感受性アルゴリズムである。 本稿では、価格問題、リンクベースのクラスタリング、動的プログラミングに基づくシーケンスアライメントのアルゴリズムを提供することにより、我々の技術を説明する。
  論文  参考訳（メタデータ） (2022-04-07T17:27:18Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。 エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。 言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
  論文  参考訳（メタデータ） (2021-10-27T16:08:09Z)
• Accelerated Message Passing for Entropy-Regularized MAP Inference [89.15658822319928]
  離散値のランダムフィールドにおけるMAP推論の最大化は、機械学習の基本的な問題である。 この問題の難しさから、特殊メッセージパッシングアルゴリズムの導出には線形プログラミング(LP)緩和が一般的である。 古典的加速勾配の根底にある手法を活用することにより,これらのアルゴリズムを高速化するランダム化手法を提案する。
  論文  参考訳（メタデータ） (2020-07-01T18:43:32Z)
• Solution Path Algorithm for Twin Multi-class Support Vector Machine [6.97711662470035]
  本論文は, ツインマルチクラスサポートベクトルマシンの高速正規化パラメータチューニングアルゴリズムについて述べる。 新たなサンプルデータセット分割法を採用し,ラグランジアン乗算器は分数線形であることが証明された。 提案手法は,グリッド探索手法の計算コストを指数レベルから定数レベルに削減し,優れた分類性能を実現する。
  論文  参考訳（メタデータ） (2020-05-30T14:05:46Z)
• Optimal Randomized First-Order Methods for Least-Squares Problems [56.05635751529922]
  このアルゴリズムのクラスは、最小二乗問題に対する最も高速な解法のうち、いくつかのランダム化手法を含んでいる。 我々は2つの古典的埋め込み、すなわちガウス射影とアダマール変換のサブサンプリングに焦点を当てる。 得られたアルゴリズムは条件数に依存しない最小二乗問題の解法として最も複雑である。
  論文  参考訳（メタデータ） (2020-02-21T17:45:32Z)
• Optimal Clustering from Noisy Binary Feedback [75.17453757892152]
  本稿では,二元的ユーザフィードバックから一組のアイテムをクラスタリングする問題について検討する。 最小クラスタ回復誤差率のアルゴリズムを考案する。 適応選択のために,情報理論的誤差下界の導出にインスパイアされたアルゴリズムを開発する。
  論文  参考訳（メタデータ） (2019-10-14T09:18:26Z)

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

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