論文の概要: CounterExample Guided Neural Synthesis
- arxiv url: http://arxiv.org/abs/2001.09245v1
- Date: Sat, 25 Jan 2020 01:11:53 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-07 00:25:05.659821
- Title: CounterExample Guided Neural Synthesis
- Title(参考訳): 逆例 誘導神経合成
- Authors: Elizabeth Polgreen, Ralph Abboud, Daniel Kroening
- Abstract要約: プログラム合成は困難であり、形式的な保証を提供する方法はスケーラビリティの問題に悩まされる。
ニューラルネットワークとフォーマルな推論を組み合わせることで、論理的な仕様をニューラルネットワークを正しい解へと導く一連の例に変換する。
この結果から,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上することが示唆された。
- 参考スコア(独自算出の注目度): 12.742347465894586
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Program synthesis is the generation of a program from a specification.
Correct synthesis is difficult, and methods that provide formal guarantees
suffer from scalability issues. On the other hand, neural networks are able to
generate programs from examples quickly but are unable to guarantee that the
program they output actually meets the logical specification. In this work we
combine neural networks with formal reasoning: using the latter to convert a
logical specification into a sequence of examples that guides the neural
network towards a correct solution, and to guarantee that any solution returned
satisfies the formal specification. We apply our technique to synthesising loop
invariants and compare the performance to existing solvers that use SMT and
existing techniques that use neural networks. Our results show that the formal
reasoning based guidance improves the performance of the neural network
substantially, nearly doubling the number of benchmarks it can solve.
- Abstract(参考訳): プログラム合成は、仕様からプログラムを生成することである。
正しい合成は困難であり、形式的な保証を提供するメソッドはスケーラビリティの問題に苦しむ。
一方、ニューラルネットワークは、サンプルからすばやくプログラムを生成することができるが、彼らが出力するプログラムが論理的仕様を満たすことを保証できない。
この研究では、ニューラルネットワークと形式的推論を組み合わせる:後者を使用することで、論理仕様をニューラルネットワークを正しい解へと導く一連の例に変換し、返却された解が形式的仕様を満たすことを保証する。
本手法をループ不変量の合成に適用し,SMTを用いた既存の解法とニューラルネットワークを用いた既存の解法との比較を行う。
その結果,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上し,解決可能なベンチマークの数がほぼ倍増することが示された。
関連論文リスト
- Graph Neural Networks for Learning Equivariant Representations of Neural Networks [55.04145324152541]
本稿では,ニューラルネットワークをパラメータの計算グラフとして表現することを提案する。
我々のアプローチは、ニューラルネットワークグラフを多種多様なアーキテクチャでエンコードする単一モデルを可能にする。
本稿では,暗黙的ニューラル表現の分類や編集など,幅広いタスクにおける本手法の有効性を示す。
論文 参考訳(メタデータ) (2024-03-18T18:01:01Z) - NeuralFastLAS: Fast Logic-Based Learning from Raw Data [54.938128496934695]
シンボリック・ルール学習者は解釈可能な解を生成するが、入力を記号的に符号化する必要がある。
ニューロシンボリックアプローチは、ニューラルネットワークを使用して生データを潜在シンボリック概念にマッピングすることで、この問題を克服する。
我々は,ニューラルネットワークを記号学習者と共同でトレーニングする,スケーラブルで高速なエンドツーエンドアプローチであるNeuralFastLASを紹介する。
論文 参考訳(メタデータ) (2023-10-08T12:33:42Z) - Return of the RNN: Residual Recurrent Networks for Invertible Sentence
Embeddings [0.0]
本研究では、教師なし符号化タスクで訓練された残効再帰ネットワークを用いて、非可逆文埋め込みのための新しいモデルを提案する。
ニューラルネットワーク翻訳モデルに共通する確率的出力ではなく、回帰に基づく出力層を用いて入力シーケンスのワードベクトルを再構成する。
RNNはLSTMや2次最適化法などのメモリユニットを必要とすることを考えると、このモデルはADAMによる高精度かつ高速なトレーニングを実現している。
論文 参考訳(メタデータ) (2023-03-23T15:59:06Z) - Permutation Equivariant Neural Functionals [92.0667671999604]
この研究は、他のニューラルネットワークの重みや勾配を処理できるニューラルネットワークの設計を研究する。
隠れた層状ニューロンには固有の順序がないため, 深いフィードフォワードネットワークの重みに生じる置換対称性に着目する。
実験の結果, 置換同変ニューラル関数は多種多様なタスクに対して有効であることがわかった。
論文 参考訳(メタデータ) (2023-02-27T18:52:38Z) - Simple initialization and parametrization of sinusoidal networks via
their kernel bandwidth [92.25666446274188]
従来の活性化機能を持つネットワークの代替として、活性化を伴う正弦波ニューラルネットワークが提案されている。
まず,このような正弦波ニューラルネットワークの簡易版を提案する。
次に、ニューラルタンジェントカーネルの観点からこれらのネットワークの挙動を分析し、そのカーネルが調整可能な帯域幅を持つ低域フィルタを近似することを実証する。
論文 参考訳(メタデータ) (2022-11-26T07:41:48Z) - Neural Combinatorial Logic Circuit Synthesis from Input-Output Examples [10.482805367361818]
本稿では,入力出力の例から論理回路を合成するための,新しい完全説明可能なニューラルアプローチを提案する。
我々の方法は、ほぼ任意の原子の選択に利用できる。
論文 参考訳(メタデータ) (2022-10-29T14:06:42Z) - Lifted Bregman Training of Neural Networks [28.03724379169264]
本稿では,(潜在的に非滑らかな)近位写像を活性化関数として,フィードフォワードニューラルネットワークのトレーニングのための新しい数学的定式化を導入する。
この定式化はBregmanに基づいており、ネットワークのパラメータに関する偏微分がネットワークのアクティベーション関数の微分の計算を必要としないという利点がある。
ニューラルネットワークに基づく分類器のトレーニングや、スパースコーディングによる(デノーミング)オートエンコーダのトレーニングには、これらのトレーニングアプローチが等しく適しているか、さらに適していることを示す数値的な結果がいくつか提示される。
論文 参考訳(メタデータ) (2022-08-18T11:12:52Z) - Toward Neural-Network-Guided Program Synthesis and Verification [26.706421573322952]
ニューラルネットワーク誘導合成という,プログラムと不変合成の新しい枠組みを提案する。
まず、ニューラルネットワークの設計とトレーニングによって、訓練されたニューラルネットワークの重みとバイアスから整数上の論理式を抽出できることを示します。
この考え方に基づき、正負の例と含意制約から公式を合成するツールを実装した。
論文 参考訳(メタデータ) (2021-03-17T03:09:05Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。
我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。
提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文 参考訳(メタデータ) (2020-03-19T17:21:02Z) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳(メタデータ) (2019-12-31T17:09:49Z) - Synthetic Datasets for Neural Program Synthesis [66.20924952964117]
本稿では,プログラムと仕様の両方で合成データ分布のバイアスを制御し,評価するための新しい手法を提案する。
そこで我々は,Karel DSLと小さなCalculator DSLを用いて,これらの分布上でのディープネットワークのトレーニングにより,分散一般化性能が向上することが実証された。
論文 参考訳(メタデータ) (2019-12-27T21:28:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。