論文の概要: Co-Certificate Learning with SAT Modulo Symmetries
- arxiv url: http://arxiv.org/abs/2306.10427v2
- Date: Wed, 21 Jun 2023 09:41:35 GMT
- ステータス: 処理完了
- システム内更新日: 2023-06-22 10:35:52.514411
- Title: Co-Certificate Learning with SAT Modulo Symmetries
- Title(参考訳): SATモジュロ対称性を用いた共証明学習
- Authors: Markus Kirchweger, Tom\'a\v{s} Peitl, Stefan Szeider
- Abstract要約: 与えられたco-NP特性を満たす同型まで全てのグラフを生成するSATベースの新しい手法を提案する。
SMSが与えられたco-NPプロパティに違反する候補グラフを生成する場合、この違反の証明書を取得する。
我々は,SMSと共認証学習が,コチェン・スペクターベクトルシステムのサイズに最もよく知られた下位境界を改善する強力な手法であることを実証した。
- 参考スコア(独自算出の注目度): 22.49516188788183
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present a new SAT-based method for generating all graphs up to isomorphism
that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry
(SMS) framework with a technique that we call co-certificate learning. If SMS
generates a candidate graph that violates the given co-NP property, we obtain a
certificate for this violation, i.e., `co-certificate' for the co-NP property.
The co-certificate gives rise to a clause that the SAT solver, serving as SMS's
backend, learns as part of its CDCL procedure. We demonstrate that SMS plus
co-certificate learning is a powerful method that allows us to improve the
best-known lower bound on the size of Kochen-Specker vector systems, a problem
that is central to the foundations of quantum mechanics and has been studied
for over half a century. Our approach is orders of magnitude faster and scales
significantly better than a recently proposed SAT-based method.
- Abstract(参考訳): 与えられたco-NP特性を満たす同型まで全てのグラフを生成するSATベースの新しい手法を提案する。
本手法はSAT Modulo Symmetry (SMS) フレームワークを拡張し,協調学習(co-certificate learning)と呼ぶ手法を提案する。
SMSが与えられたco-NPプロパティに違反する候補グラフを生成する場合、この違反の証明書、すなわちco-NPプロパティの 'co-certificate' を得る。
SATソルバはSMSのバックエンドとして機能し、CDCL手順の一部として学習する。
我々は、SMSと共証明学習が、量子力学の基礎の中心であり、半世紀以上にわたって研究されてきたKochen-Speckerベクトルシステムのサイズに最もよく知られた下界を改善する強力な方法であることを示した。
我々のアプローチは、最近提案されたSATベースの方法よりも桁違いに高速でスケールできる。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳(メタデータ) (2024-10-18T22:25:54Z) - SAT and Lattice Reduction for Integer Factorization [5.035245337299788]
ランダムリークビット因数分解問題の解法として,新しいハイブリッドSATおよび計算機代数手法を提案する。
我々の実装は、純粋なSATや純粋計算機代数のアプローチよりもはるかに高速なランダムリークビット分解問題を解く。
論文 参考訳(メタデータ) (2024-06-28T17:30:20Z) - Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。
最新のUQベースラインの集合を実装した新しいベンチマークを導入する。
我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
論文 参考訳(メタデータ) (2024-06-21T20:06:31Z) - Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。
セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。
本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
論文 参考訳(メタデータ) (2024-02-13T11:59:43Z) - PQCMC: Post-Quantum Cryptography McEliece-Chen Implicit Certificate Scheme [0.0]
そこで本研究では,PQCMC(McEliece-Chen)を用いた量子後暗号手法を提案する。
本研究では,量子コンピューティングの脅威に対処する手段として,PQCに基づく暗黙的な証明スキームの実現可能性を示す。
論文 参考訳(メタデータ) (2024-01-03T13:34:20Z) - A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem [14.693394941317843]
本稿では,ブール充足可能性解法と計算機代数システムを組み合わせた検証可能な新しい証明生成法を提案する。
提案手法は、3次元のKS系が少なくとも24個のベクトルを含む必要があることを示す。
また, KS問題に対して, 順序23の40.3 TiBの低い値のコンピュータ検証証明を初めて提供した。
論文 参考訳(メタデータ) (2023-06-23T06:42:59Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。
そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
論文 参考訳(メタデータ) (2022-10-04T09:19:13Z) - Sound and Complete Verification of Polynomial Networks [55.9260539566555]
PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。
分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。
我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
論文 参考訳(メタデータ) (2022-09-15T11:50:43Z) - A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic
Locking [3.076761061950216]
本稿では,ニューラルネットワークを用いた unSAT 節変換器 SATConda を提案する。
SATCondaは最小限の領域と電力オーバーヘッドを発生させ、元の機能を不必要なセキュリティで保存する。
SATCondaをISCAS85およびISCAS89ベンチマークで評価した。
論文 参考訳(メタデータ) (2022-09-13T07:59:27Z) - Smooth-Reduce: Leveraging Patches for Improved Certified Robustness [100.28947222215463]
本研究では,Smooth-Reduce の学習自由な修正スムース化手法を提案する。
提案アルゴリズムは,入力画像から抽出した重なり合うパッチを分類し,予測ロジットを集約して,入力周辺の半径が大きいことを証明する。
我々は,このような証明書の理論的保証を提供し,他のランダムな平滑化手法に対する顕著な改善を実証的に示す。
論文 参考訳(メタデータ) (2022-05-12T15:26:20Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。