論文の概要: Engineering an Efficient Boolean Functional Synthesis Engine

• arxiv url: http://arxiv.org/abs/2108.05717v1
• Date: Thu, 12 Aug 2021 13:01:49 GMT
• ステータス: 処理完了
• システム内更新日: 2021-08-13 14:41:21.833688
• Title: Engineering an Efficient Boolean Functional Synthesis Engine
• Title（参考訳）: 効率的なブール機能合成エンジンの工学
• Authors: Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel
• Abstract要約: 入力と出力の集合間のブール仕様が与えられたとき、関数合成の問題は、各出力を仕様が満たされるような入力の関数として合成することである。 関数合成のためのデータ駆動型フレームワークに対して,4つのアルゴリズム改良を提案する。 Manthan2はManthanに比べて実行時のパフォーマンスが大幅に向上した。
• 参考スコア（独自算出の注目度）: 22.075107339383255
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reasoning to efficiently synthesise Boolean functions. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We implement these improvements in the state-of-the-art framework, called Manthan. The proposed framework is called Manthan2. Manthan2 shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan--- an increment of 153 instances over the state-of-the-art. To put this into perspective, Manthan improved on the prior state-of-the-art by only 76 instances.
• Abstract（参考訳）: 入力と出力の間のブール仕様が与えられた場合、ブール関数合成の問題は、各出力を仕様が満たされるような入力の関数として合成することである。 過去数年間、アルゴリズムの激しい開発が見られたが、スケーラビリティを達成することが聖杯のままである。 最先端のアプローチは、機械学習と自動推論を組み合わせて、ブール関数を効率的に合成する。 本稿では,関数合成のためのデータ駆動型フレームワークのアルゴリズム改良を4つ提案する:依存性駆動型多クラス化器を用いて候補関数を学習し,補間,変数保持,語彙的MaxSATを用いて一意に定義された関数を抽出し,候補を修復する。 manthanと呼ばれる最先端のフレームワークにこれらの改善を実装します。 提案されたフレームワークはManthan2と呼ばれる。 Manthan2はManthanに比べて実行時のパフォーマンスが大幅に向上した。 609ベンチマークに関する広範な実験的評価において、Manthan2は、Manthanによって解決された356インスタンスと比較して、509インスタンスのBoolean関数ベクトルを合成することができる。 これを考慮すると、Manthan氏は以前の最先端を76インスタンスで改善した。

関連論文リスト

• Preference Optimization for Reasoning with Pseudo Feedback [100.62603571434167]
  提案手法では,解のラベル付けを関連するテストケースに対する評価として行うことで,推論タスクに対する疑似フィードバックを生成する手法を提案する。 本研究では,擬似フィードバックを優先最適化に用いる数学的推論と符号化の両タスクについて実験を行い,両タスク間の改善を観察する。
  論文  参考訳（メタデータ） (2024-11-25T12:44:02Z)
• Enhancing Function Name Prediction using Votes-Based Name Tokenization and Multi-Task Learning [10.668991471782618]
  投票による名前のトークン化とマルチタスク学習を用いた関数名予測を行うフレームワークを提案する。 Epitomeは、事前訓練されたアセンブリ言語モデルとグラフニューラルネットワークにより、包括的な機能意味学を学ぶ。 エピトームは最先端の関数名予測ツールを44.34%、64.16%、54.44%の精度、リコール、F1スコアで上回っている。
  論文  参考訳（メタデータ） (2024-05-15T06:01:40Z)
• INR-Arch: A Dataflow Architecture and Compiler for Arbitrary-Order Gradient Computations in Implicit Neural Representation Processing [66.00729477511219]
  計算グラフとして表される関数を考えると、従来のアーキテクチャはn階勾配を効率的に計算する上で困難に直面している。 InR-Archは,n階勾配の計算グラフをハードウェア最適化データフローアーキテクチャに変換するフレームワークである。 1.8-4.8x と 1.5-3.6x の高速化を CPU と GPU のベースラインと比較した結果を示す。
  論文  参考訳（メタデータ） (2023-08-11T04:24:39Z)
• UNETR++: Delving into Efficient and Accurate 3D Medical Image Segmentation [93.88170217725805]
  本稿では,高画質なセグメンテーションマスクと,パラメータ,計算コスト,推論速度の両面での効率性を提供するUNETR++という3次元医用画像セグメンテーション手法を提案する。 我々の設計の核となるのは、空間的およびチャネル的な識別的特徴を効率的に学習する、新しい効率的な対注意ブロック(EPA)の導入である。 Synapse, BTCV, ACDC, BRaTs, Decathlon-Lungの5つのベンチマークで評価した結果, 効率と精度の両面で, コントリビューションの有効性が示された。
  論文  参考訳（メタデータ） (2022-12-08T18:59:57Z)
• A SAT Encoding for Optimal Clifford Circuit Synthesis [3.610459670994051]
  量子回路の重要なサブクラスであるクリフォード回路の最適合成を考える。 本稿では,タスクを満足度問題として符号化したクリフォード回路の最適合成法を提案する。 得られたツールは、最大26ドルキュービットの最適回路を合成する。
  論文  参考訳（メタデータ） (2022-08-24T18:00:03Z)
• Inducing Transformer's Compositional Generalization Ability via Auxiliary Sequence Prediction Tasks [86.10875837475783]
  体系的な構成性は人間の言語において必須のメカニズムであり、既知の部品の組換えによって新しい表現を作り出すことができる。 既存のニューラルモデルには、記号構造を学習する基本的な能力がないことが示されている。 本稿では,関数の進行と引数のセマンティクスを追跡する2つの補助シーケンス予測タスクを提案する。
  論文  参考訳（メタデータ） (2021-09-30T16:41:19Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Logic Synthesis Meets Machine Learning: Trading Exactness for Generalization [37.3380462457184]
  我々は,IWLS 2020で実施した競技結果に基づいて,不完全特定関数を学習する。 このベンチマークスイートを利用可能にし、学習に対するさまざまなアプローチの詳細な比較分析を提供しています。
  論文  参考訳（メタデータ） (2020-12-04T11:23:01Z)
• Programming by Rewards [20.626369097817715]
  我々は、性能、資源利用、あるいはベンチマーク上の正確性などの量的指標を最適化するための新しいアプローチである「報酬によるプログラミング」 (PBR) を定式化し、研究する。 PBR仕様は、(1)入力機能$x$と(2)報酬関数$r$で構成され、ブラックボックスコンポーネントとしてモデル化されている(実行しかできない)。 フレームワークは理論的に確立された -- 報酬が優れた特性を満たす場合において、合成されたコードは正確な意味で最適であることを示す。
  論文  参考訳（メタデータ） (2020-07-14T05:49:14Z)
• Manthan: A Data Driven Approach for Boolean Function Synthesis [35.159590750027]
  ブール関数合成に対する新しいデータ駆動型アプローチであるManthanを提案する。 マンサンは356のベンチマークを280と比較し、最先端の技術によって最も解決された。 Manthan氏は60のベンチマークを解決した。
  論文  参考訳（メタデータ） (2020-05-14T12:44:21Z)

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

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