論文の概要: 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でオープンソースライセンスで公開されている。
関連論文リスト
- LinSATNet: The Positive Linear Satisfiability Neural Networks [116.65291739666303]
本稿では,ニューラルネットワークに人気の高い正の線形満足度を導入する方法について検討する。
本稿では,古典的なシンクホーンアルゴリズムを拡張し,複数の辺分布の集合を共同で符号化する,最初の微分可能満足層を提案する。
論文 参考訳（メタデータ） (2024-07-18T22:05:21Z) - Freya PAGE: First Optimal Time Complexity for Large-Scale Nonconvex Finite-Sum Optimization with Heterogeneous Asynchronous Computations [92.1840862558718]
実用的な分散システムでは、労働者は概して均質ではなく、非常に多様な処理時間を持つ。
本稿では、任意に遅い計算を扱うための新しい並列手法Freyaを提案する。
Freyaは従来の手法と比較して,複雑性の保証が大幅に向上していることを示す。
論文 参考訳（メタデータ） (2024-05-24T13:33:30Z) - Light Schrödinger Bridge [72.88707358656869]
我々は,軽量でシミュレーション不要で理論的に正当化されたSchr"odinger Bridgesソルバを開発した。
我々の光解法は密度推定に広く用いられているガウス混合モデルに類似している。
この類似性に着想を得て、光解法が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) - 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) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳（メタデータ） (2019-12-31T17:09:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。