論文の概要: CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses

• arxiv url: http://arxiv.org/abs/2510.26431v1
• Date: Thu, 30 Oct 2025 12:25:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-31 16:05:09.80582
• Title: CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
• Title（参考訳）: CHCVerif:拘束されたホーンクロースのためのポートフォリオベースのソルバー
• Authors: Mihály Dobos-Kovács, Levente Bajczi, András Vörös,
• Abstract要約: 制約付きホーンクロース(CHC)は、検証タスクの中間表現として広く採用されている。 本稿では,CHCを解くためのソフトウェア検証アプローチを採用するポートフォリオベースのCHCソルバを紹介する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interprocedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio.
• Abstract（参考訳）: 制約されたホーンクロース(CHC)は、安全性チェック、不変合成、相互解析など、様々な検証タスクの中間的表現として広く採用されている。 本稿では、ポートフォリオベースのCHCソルバであるCHCVERIFを紹介し、CHCを解くためのソフトウェア検証アプローチを採用する。 このアプローチにより、成熟したソフトウェア検証ツールを再利用してCHCベンチマーク、特にビットベクタや低レベルのセマンティクスに取り組みます。 評価の結果,線形整数算術では適度にしか成功しないが,ビットベクターベンチマークではわずかに成功していることがわかった。 さらに本結果は,CHC解決のバックエンドとしてソフトウェア検証ツールを使用する可能性,特に慎重に構築されたポートフォリオをサポートする場合の可能性を実証した。

関連論文リスト

• Theta as a Horn Solver [0.0]
  Thetaは、2023年からCHC-COMPコンペティションに参加している検証フレームワークである。 本稿では、Thetaが採用しているアルゴリズムの詳細な説明を行い、他のCHCソルバと区別するユニークな特徴を強調した。 また、CHC-COMPベンチマークの文脈でツールの長所と短所を分析する。
  論文  参考訳（メタデータ） (2025-10-30T12:24:52Z)
• On Continuous Optimization for Constraint Satisfaction Problems [33.35208489737497]
  制約満足度問題(Constraint satisfaction problem, CSP)は、数学、物理学、理論計算機科学において基本的な問題である。 近年の進歩により、最近の連続局所探索(CSP)解法は、SAT問題の特定のクラスにおいて高い競争力を発揮することが示されている。 本稿では,Walsh-Fourier変換をCSPに変換する連続最適化フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-06T04:30:07Z)
• Sample Efficient Certification of Discrete-Time Control Barrier Functions [2.4118840512344852]
  制御不変集合 (CI) は力学系の安全性を証明するための道具である。 制御バリア関数(CBF)は、CBFの零部分レベル集合がCI集合であるため、そのような集合を計算するのに有効なツールである。 CBFが実際にロバスト制約を満たすかどうかを検証するためのアプローチを提案する。
  論文  参考訳（メタデータ） (2025-09-04T05:47:24Z)
• Semi-supervised Semantic Segmentation with Multi-Constraint Consistency Learning [81.02648336552421]
  本稿では,エンコーダとデコーダの段階的拡張を容易にするためのマルチ制約一貫性学習手法を提案する。 自己適応型特徴マスキングとノイズ注入は、デコーダの堅牢な学習のための特徴を摂動させるために、インスタンス固有の方法で設計されている。 Pascal VOC2012およびCityscapesデータセットの実験結果から,提案したMCCLが新たな最先端性能を実現することを示す。
  論文  参考訳（メタデータ） (2025-03-23T03:21:33Z)
• Fast Context-Biasing for CTC and Transducer ASR models with CTC-based Word Spotter [57.64003871384959]
  この研究は、CTCベースのWord Spotterでコンテキストバイアスを高速化するための新しいアプローチを示す。 提案手法は,CTCログ確率をコンパクトなコンテキストグラフと比較し,潜在的なコンテキストバイアス候補を検出する。 その結果、FスコアとWERの同時改善により、文脈バイアス認識の大幅な高速化が示された。
  論文  参考訳（メタデータ） (2024-06-11T09:37:52Z)
• LLMC: Benchmarking Large Language Model Quantization with a Versatile Compression Toolkit [55.73370804397226]
  鍵圧縮技術である量子化は、大きな言語モデルを圧縮し、加速することにより、これらの要求を効果的に軽減することができる。 本稿では,プラグアンドプレイ圧縮ツールキットであるLLMCについて,量子化の影響を公平かつ体系的に検討する。 この汎用ツールキットによって、我々のベンチマークはキャリブレーションデータ、アルゴリズム(3つの戦略)、データフォーマットの3つの重要な側面をカバーしています。
  論文  参考訳（メタデータ） (2024-05-09T11:49:05Z)
• Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification [0.09786690381850355]
  制約付きホーンクロース(CHC)は、従来、形式的検証において低レベルな表現として用いられてきた。 線形CHCに対する別のボトムアップ手法を提案し、オープンソースのモデルチェックフレームワーク THETA における2つの選択肢を評価する。
  論文  参考訳（メタデータ） (2024-04-23T16:46:27Z)
• Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
  機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。 セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。 本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
  論文  参考訳（メタデータ） (2024-02-13T11:59:43Z)
• Multiple Query Satisfiability of Constrained Horn Clauses [0.0]
  本稿では,一組のクエリを含む一組のCHCを入力とし,一組のCHCを出力する手法を提案する。 変換されたCHCは、各新しいクエリに適した情報を他のクエリから取得し、CHC満足度アルゴリズムが全てのクエリ間の関係を活用できるようにする。
  論文  参考訳（メタデータ） (2022-11-28T10:30:04Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。 本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
  論文  参考訳（メタデータ） (2022-08-11T10:31:28Z)
• Using Representation Expressiveness and Learnability to Evaluate Self-Supervised Learning Methods [61.49061000562676]
  本稿では,学習可能性を評価するためにCluster Learnability (CL)を導入する。 CLは、K-meansで表現をクラスタリングすることによって得られたラベルを予測するために訓練されたKNNのパフォーマンスで測定される。 CLは、他の競合する評価手法よりも分布内モデルの性能と相関することがわかった。
  論文  参考訳（メタデータ） (2022-06-02T19:05:13Z)

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

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