論文の概要: Toward Neural-Network-Guided Program Synthesis and Verification

• arxiv url: http://arxiv.org/abs/2103.09414v1
• Date: Wed, 17 Mar 2021 03:09:05 GMT
• ステータス: 処理完了
• システム内更新日: 2021-03-18 12:52:33.172834
• Title: Toward Neural-Network-Guided Program Synthesis and Verification
• Title（参考訳）: ニューラルネットワークによるプログラム合成と検証
• Authors: Naoki Kobayashi, Taro Sekiyama, Issei Sato and Hiroshi Unno
• Abstract要約: ニューラルネットワーク誘導合成という,プログラムと不変合成の新しい枠組みを提案する。 まず、ニューラルネットワークの設計とトレーニングによって、訓練されたニューラルネットワークの重みとバイアスから整数上の論理式を抽出できることを示します。 この考え方に基づき、正負の例と含意制約から公式を合成するツールを実装した。
• 参考スコア（独自算出の注目度）: 26.706421573322952
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama's program synthesis by sketching.
• Abstract（参考訳）: 本稿では,ニューラルネットワーク誘導合成という,プログラムおよび不変合成の新しい枠組みを提案する。 まず、ニューラルネットワークを適切に設計し、トレーニングすることで、トレーニングされたニューラルネットワークの重みとバイアスから整数上の論理式を抽出できることを示します。 この考え方に基づき,正負の例と含意の制約から式を合成するツールを実装し,有望な実験結果を得た。 また,本手法の2つの応用についても論じる。 ひとつは、ICE学習に基づくCHC問題解決のフレームワークにおける修飾子発見のためのツールの使用であり、プログラム検証や帰納的不変合成に適用することができる。 もう1つの応用は、オラクルベースのプログラミングと呼ばれる新しいプログラム開発フレームワークであり、これは、スケッチによるSolar-Lezamaのプログラム合成の神経ネットワーク誘導のバリエーションである。

関連論文リスト

• Mechanistic Neural Networks for Scientific Machine Learning [58.99592521721158]
  我々は、科学における機械学習応用のためのニューラルネットワーク設計であるメカニスティックニューラルネットワークを提案する。 新しいメカニスティックブロックを標準アーキテクチャに組み込んで、微分方程式を表現として明示的に学習する。 我々のアプローチの中心は、線形プログラムを解くために線形ODEを解く技術に着想を得た、新しい線形計画解法(NeuRLP)である。
  論文  参考訳（メタデータ） (2024-02-20T15:23:24Z)
• Permutation Equivariant Neural Functionals [92.0667671999604]
  この研究は、他のニューラルネットワークの重みや勾配を処理できるニューラルネットワークの設計を研究する。 隠れた層状ニューロンには固有の順序がないため, 深いフィードフォワードネットワークの重みに生じる置換対称性に着目する。 実験の結果, 置換同変ニューラル関数は多種多様なタスクに対して有効であることがわかった。
  論文  参考訳（メタデータ） (2023-02-27T18:52:38Z)
• The Predictive Forward-Forward Algorithm [79.07468367923619]
  本稿では,ニューラルネットワークにおける信頼割当を行うための予測フォワード(PFF)アルゴリズムを提案する。 我々は,有向生成回路と表現回路を同時に同時に学習する,新しい動的リカレントニューラルネットワークを設計する。 PFFは効率よく学習し、学習信号を伝達し、フォワードパスのみでシナプスを更新する。
  論文  参考訳（メタデータ） (2023-01-04T05:34:48Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  入力出力の例からCプログラムを合成する第一歩を踏み出す。 特に,部分生成プログラムの実行を近似するために潜在表現を学習するLa Synthを提案する。 これらのプログラムのトレーニングにより,Karel と C のプログラム合成における予測性能がさらに向上することを示す。
  論文  参考訳（メタデータ） (2021-06-29T02:21:32Z)
• Geometry of Program Synthesis [4.83420384410068]
  チューリング機械の合成に基づく普遍計算の再評価を行う。 これはプログラムを解析多様体の特異点として、あるいは同値に合成問題のベイズ後方の位相として見ることに繋がる。
  論文  参考訳（メタデータ） (2021-03-30T05:14:15Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)
• Optimal Neural Program Synthesis from Multimodal Specifications [45.35689345004124]
  マルチモーダルプログラム合成は、プログラム合成を挑戦的な設定に拡張する魅力的な方法である。 本稿では,ユーザが提供する制約を満たすプログラムを見つけることを目的とした,最適なニューラルシンセサイザー手法を提案する。
  論文  参考訳（メタデータ） (2020-10-04T20:51:21Z)
• Type-driven Neural Programming by Example [0.0]
  我々は、与えられた入力を与えられた出力にマッピングするプログラムを見つけることを目的とした、例によるプログラミング(PBE)について考察する。 本稿では,プログラム型をPBEのためのニューラルプログラム合成手法に組み込む方法を提案する。
  論文  参考訳（メタデータ） (2020-08-28T12:30:05Z)
• Synthesize, Execute and Debug: Learning to Repair for Neural Program Synthesis [81.54148730967394]
  本稿では,合成,実行,デバッグの段階を組み込んだニューラルネットワーク生成フレームワークであるSEDを提案する。 SEDはまず、神経プログラムシンセサイザーコンポーネントを使用して初期プログラムを生成し、その後、神経プログラムデバッガを使用して生成されたプログラムを反復的に修復する。 挑戦的な入出力プログラム合成ベンチマークであるKarelでは、SEDはニューラルプログラムシンセサイザー自体のエラー率をかなりのマージンで削減し、デコードのための標準ビームサーチより優れている。
  論文  参考訳（メタデータ） (2020-07-16T04:15:47Z)
• CounterExample Guided Neural Synthesis [12.742347465894586]
  プログラム合成は困難であり、形式的な保証を提供する方法はスケーラビリティの問題に悩まされる。 ニューラルネットワークとフォーマルな推論を組み合わせることで、論理的な仕様をニューラルネットワークを正しい解へと導く一連の例に変換する。 この結果から,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上することが示唆された。
  論文  参考訳（メタデータ） (2020-01-25T01:11:53Z)

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

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