論文の概要: Formally Certified Approximate Model Counting
- arxiv url: http://arxiv.org/abs/2406.11414v1
- Date: Mon, 17 Jun 2024 11:02:04 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-18 15:11:33.154668
- Title: Formally Certified Approximate Model Counting
- Title（参考訳）: 形式的に認証された近似モデルカウント
- Authors: Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel,
- Abstract要約: 本稿では、その出力近似の品質に関する保証を正式に保証した、近似モデルカウントのための最初の認証フレームワークを提案する。
i)Isabelle/HOL証明アシスタントにおけるアルゴリズムのPAC保証の静的かつ1回限りの公式な証明、(ii)証明証明書を用いた外部CNF-XORソルバに対するApproxMCの呼び出しの動的かつ1回実行による検証。
- 参考スコア（独自算出の注目度）: 25.20597060311209
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of ApproxMC's approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter's stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints. We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both ApproxMC and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify $84.7\%$ of instances with generated certificates when given the same time and memory limits as the counter.
- Abstract（参考訳）: 近似モデルカウント(英: Approximate model counting)は、入力ブール式に対する解の数を近似するタスクである。
共役正規形(CNF)の公式に対する最先端の近似モデルカウンタであるApproxMCは、ほぼ正しい(PAC)スタイルの保証でモデルカウントを得るスケーラブルな手段を提供する。
それでも、ApproxMCの近似の妥当性は、そのランダム化アルゴリズムの慎重な理論的解析と高度に最適化された実装の正しさ、特に、パリティ(XOR)制約をネイティブに処理できる漸進的なCNF満足度解決器とのステートフルな相互作用に依存している。
本稿では、その出力近似の品質に関する保証を正式に保証した、近似モデルカウントのための最初の認証フレームワークを提案する。
私たちのアプローチは次の2つを組み合わせています。
i)Isabelle/HOL証明アシスタントにおけるアルゴリズムのPAC保証の静的で1回限りの形式的証明。
(ii) 証明証明書を用いた外部CNF-XORソルバに対するApproxMCの呼び出しの動的かつ実行単位の検証。
検証の2つの部分間の厳密な接続を確立するための我々の一般的なアプローチについて詳述し、形式化されたランダム化アルゴリズムを証明チェッカーに変換する青写真と、ApproxMCとその内部CNF-XOR解決ステップの証明証明書の設計について述べる。
実験により,証明書生成は近似カウンタの実装にオーバーヘッドをほとんど与えず,また,カウンタと同じ時間とメモリ制限が与えられた場合,証明書チェッカーが生成した証明書に対して,84.7\%のインスタンスを完全認証できることがわかった。
関連論文リスト
- Rigorous Probabilistic Guarantees for Robust Counterfactual Explanations [80.86128012438834]
モデルシフトに対する反ファクトの堅牢性を計算することはNP完全であることを示す。
本稿では,頑健性の厳密な推定を高い保証で実現する新しい確率論的手法を提案する。
論文 参考訳（メタデータ） (2024-07-10T09:13:11Z) - ConU: Conformal Uncertainty in Large Language Models with Correctness Coverage Guarantees [68.33498595506941]
自然言語生成(NLG)タスクの不確実性定量化は、依然としてオープンな課題である。
本研究では、不確実性の指標を厳密な理論的保証に変換することができる適合型予測(CP)について検討する。
本稿では,自己整合性を利用したサンプリングに基づく不確実性評価手法を提案する。
論文 参考訳（メタデータ） (2024-06-29T17:33:07Z) - Smart Casual Verification of CCF's Distributed Consensus and Consistency Protocols [2.160395257762205]
Confidential Consortium Framework(CCF)は、信頼できる信頼性のあるクラウドアプリケーションを開発するためのオープンソースプラットフォームである。
CCFはMicrosoftのAzure Confidential Ledgerサービスを動かしている。
本稿では、CCFの新しい分散プロトコルの正当性を検証するために、スマートカジュアル検証を適用した経験を報告する。
論文 参考訳（メタデータ） (2024-06-25T10:49:54Z) - Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。
セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。
本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
論文 参考訳（メタデータ） (2024-02-13T11:59:43Z) - Fast Entropy-Based Methods of Word-Level Confidence Estimation for
End-To-End Automatic Speech Recognition [86.21889574126878]
本研究では,フレーム単位のエントロピー値を正規化して集約し,単位単位当たりの信頼度と単語毎の信頼度を求める方法を示す。
提案手法をLibriSpeechテストセット上で評価した結果,最大フレーム当たりの信頼度推定値の最大値から,信頼度推定値の最大値の最大値の最大値の最大値の最大値の2倍,4倍の精度を示した。
論文 参考訳（メタデータ） (2022-12-16T20:27:40Z) - Accelerating Certifiable Estimation with Preconditioned Eigensolvers [2.1701691499017812]
多くの最先端 (Burer-Monteiro 因数分解に基づく) 推定手法における主要なコストは、解の検証である。
本稿では,この検証ステップを著しく高速化する方法を示し,検証手法の全体的な高速化について述べる。
事前条件付き固有解法を用いてこの問題に対処する方法を示す。
論文 参考訳（メタデータ） (2022-07-12T02:00:08Z) - Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。
まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。
次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
論文 参考訳（メタデータ） (2021-11-18T23:21:00Z) - Improved, Deterministic Smoothing for L1 Certified Robustness [119.86676998327864]
分割雑音を伴う非加法的決定論的平滑化法(dssn)を提案する。
一様加法平滑化とは対照的に、ssn認証は無作為なノイズコンポーネントを独立に必要としない。
これは、規範ベースの敵対的脅威モデルに対して決定論的「ランダム化平滑化」を提供する最初の仕事である。
論文 参考訳（メタデータ） (2021-03-17T21:49:53Z) - Incremental Verification of Fixed-Point Implementations of Neural
Networks [0.19573380763700707]
インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
論文 参考訳（メタデータ） (2020-12-21T10:03:44Z) - Adversarial Robustness of Supervised Sparse Coding [34.94566482399662]
表現を学習すると同時に、正確な一般化境界と堅牢性証明を与えるモデルを考える。
線形エンコーダと組み合わされたスパーシティプロモーティングエンコーダを組み合わせた仮説クラスに着目した。
エンドツーエンドの分類のための堅牢性証明を提供する。
論文 参考訳（メタデータ） (2020-10-22T22:05:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。