論文の概要: BNSynth: Bounded Boolean Functional Synthesis
- arxiv url: http://arxiv.org/abs/2212.08170v1
- Date: Thu, 15 Dec 2022 22:10:11 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-19 14:54:13.718512
- Title: BNSynth: Bounded Boolean Functional Synthesis
- Title(参考訳): bnsynth: 有界ブール汎関数合成
- Authors: Ravi Raja (1), Stanly Samuel (1), Chiranjib Bhattacharyya (1), Deepak
D'Souza (1), Aditya Kanade (2) ((1) Indian Institute of Science, Bangalore,
(2) Microsoft Research, Bangalore)
- Abstract要約: 本稿では,BFS問題を解空間上の与えられた境界の下で最初に解くツールを紹介する。
BN Synthは、境界付きBFS問題を解決するために、反例付き神経アプローチを使用している。
我々は,少なくとも textbf3.2X (および textbf24X まで) の改善を観測し,ソリューションサイズを平均で削減した。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The automated synthesis of correct-by-construction Boolean functions from
logical specifications is known as the Boolean Functional Synthesis (BFS)
problem. BFS has many application areas that range from software engineering to
circuit design. In this paper, we introduce a tool BNSynth, that is the first
to solve the BFS problem under a given bound on the solution space. Bounding
the solution space induces the synthesis of smaller functions that benefit
resource constrained areas such as circuit design. BNSynth uses a
counter-example guided, neural approach to solve the bounded BFS problem.
Initial results show promise in synthesizing smaller solutions; we observe at
least \textbf{3.2X} (and up to \textbf{24X}) improvement in the reduction of
solution size on average, as compared to state of the art tools on our
benchmarks. BNSynth is available on GitHub under an open source license.
- Abstract(参考訳): 論理仕様から正しいブール関数の自動合成はブール汎関数合成(bfs)問題として知られている。
BFSには、ソフトウェア工学から回路設計まで、多くの応用分野がある。
本稿では,BFS問題を解空間上の与えられた境界の下で最初に解くツールであるBNSynthを紹介する。
解空間の境界は、回路設計のような資源制約された領域に役立つ小さな関数の合成を誘導する。
BNSynthは、境界付きBFS問題を解決するために、反例付きニューラルネットワークを使用する。
我々は、ベンチマークにおけるアートツールの状態と比較して、ソリューションサイズが平均で減少するのに対して、少なくとも \textbf{3.2x}(および \textbf{24x}まで)の改善を観察した。
BNSynthはGitHubでオープンソースライセンスで公開されている。
関連論文リスト
- Light Schr\"odinger Bridge [79.62389172166125]
高速かつ簡易なシュロディンガーブリッジ (SB) ソルバを提案する。
私たちの開発は、最近この分野に登場した2つのアイデアの賢い組み合わせです。
これらのアイデアを組み合わせることで、軽量でシミュレーション不要で理論上正当化されたSBソルバが得られることを示す。
論文 参考訳(メタデータ) (2023-10-02T13:06:45Z) - Depth-Optimal Synthesis of Clifford Circuits with SAT Solvers [4.208975913508643]
最適合成は、量子および古典的ハードウェア設計において中心的な問題である。
エンタングリング入力刺激と安定化ホルマリズムを用いて、クリフォード合成問題をポリサイズ満足度問題の族に還元する。
実験的な評価により、最適合成手法は、ランダムなクリフォード回路とグロバー探索のためのクリフォード+T回路に対して実質的な深さ改善をもたらすことが示された。
論文 参考訳(メタデータ) (2023-05-02T18:00:00Z) - Decentralized Riemannian Algorithm for Nonconvex Minimax Problems [82.50374560598493]
ニューラルネットワークのためのミニマックスアルゴリズムは、多くの問題を解決するために開発された。
本稿では,2種類のミニマックスアルゴリズムを提案する。
そこで我々は, DRSGDAを提案し, 本手法が勾配を達成することを証明した。
論文 参考訳(メタデータ) (2023-02-08T01:42:45Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。
これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。
本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
論文 参考訳(メタデータ) (2022-11-16T18:59:54Z) - OpenABC-D: A Large-Scale Dataset For Machine Learning Guided Integrated
Circuit Synthesis [10.338357262730863]
OpenABC-Dは、オープンソースの論理合成ツールを備えたプロトタイプなオープンソース設計によって作成された、大規模でラベル付きデータセットである。
このデータセット上で一般的な学習問題を定義し、既存のソリューションをベンチマークする。
論文 参考訳(メタデータ) (2021-10-21T17:19:19Z) - Satisfiability and Synthesis Modulo Oracles [7.246701762489972]
多くの合成アルゴリズムは、満足度変調理論(SMT)に基づくホワイトボックスオラクルを用いて反例を提供する。
本稿では,分子誘導合成問題の一般クラスを解くための枠組みについて述べる。
また、満足度モジュロ理論やオラクルの問題を定式化し、この問題を解くアルゴリズムを提案する。
論文 参考訳(メタデータ) (2021-07-28T16:36:26Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳(メタデータ) (2021-04-14T09:22:42Z) - Scalable Combinatorial Bayesian Optimization with Tractable Statistical
models [44.25245545568633]
緩和空間上のブラックボックス関数(集合、列、木、グラフなど)を最適化する問題について検討する。
サブモジュール緩和の最近の進歩に基づき,BOCSモデルにおけるAFO問題のスケーラビリティと精度向上を目標として,Parametrized Submodular (PSR) のアプローチを検討する。
多様なベンチマーク問題に対する実験では、BOCSモデルに対するPSRによる大幅な改善が示されている。
論文 参考訳(メタデータ) (2020-08-18T22:56:46Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳(メタデータ) (2020-02-24T17:55:10Z) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳(メタデータ) (2019-12-31T17:09:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。