論文の概要: Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications

• arxiv url: http://arxiv.org/abs/1912.13430v1
• Date: Tue, 31 Dec 2019 17:09:49 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-16 20:15:47.038205
• Title: Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
• Title（参考訳）: 線形時間論理仕様のためのニューラルガイドプログラム合成に向けて
• Authors: Alberto Camacho, Sheila A. McIlraith
• Abstract要約: ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。 提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
• 参考スコア（独自算出の注目度）: 26.547133495699093
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Synthesizing a program that realizes a logical specification is a classical problem in computer science. We examine a particular type of program synthesis, where the objective is to synthesize a strategy that reacts to a potentially adversarial environment while ensuring that all executions satisfy a Linear Temporal Logic (LTL) specification. Unfortunately, exact methods to solve so-called LTL synthesis via logical inference do not scale. In this work, we cast LTL synthesis as an optimization problem. We employ a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize LTL synthesis. In our experiments the learned Q-function provides effective guidance for synthesis problems with relatively small specifications.
• Abstract（参考訳）: 論理仕様を実現するプログラムの合成は、コンピュータ科学における古典的な問題である。 そこで本研究では,すべての実行が線形時相論理(ltl)仕様を満たすことを保証しつつ,潜在的に敵対的な環境に反応する戦略を合成することを目的としている。 残念ながら、論理推論によるいわゆるLTL合成の正確な解法はスケールしない。 本研究では,LTL合成を最適化問題として用いた。 ニューラルネットワークを用いてQ-関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。 提案手法は,LTL合成を実現するために,検索とディープラーニングを組み合わせることに特有である。 我々の実験では、学習されたQ-関数は比較的小さな仕様で合成問題の効果的なガイダンスを提供する。

関連論文リスト

• Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
  本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。 また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
  論文  参考訳（メタデータ） (2024-07-12T15:23:27Z)
• Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
  本稿では,形式的合成ベンチマークを解くための大規模言語モデルの能力を評価する。 ワンショット合成が失敗すると,新しい列挙合成アルゴリズムを提案する。 形式的合成のためのスタンドアロンツールとしてGPT-3.5は,最先端の形式的合成アルゴリズムにより容易に性能が向上することがわかった。
  論文  参考訳（メタデータ） (2024-03-06T19:13:53Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。 本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
  論文  参考訳（メタデータ） (2023-07-26T01:07:52Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Neural Circuit Synthesis from Specification Patterns [5.7923858184309385]
  ハードウェア回路を高レベル論理仕様から直接合成するタスクにおいて階層変換器を訓練する。 機械学習を使った新しいアプローチは、この分野で多くの可能性を開くかもしれないが、十分な量のトレーニングデータが不足している。 この合成データに基づいて訓練された階層変換器は,合成競合による問題の大部分を解消することを示す。
  論文  参考訳（メタデータ） (2021-07-25T18:17:33Z)
• Synthesize, Execute and Debug: Learning to Repair for Neural Program Synthesis [81.54148730967394]
  本稿では,合成,実行,デバッグの段階を組み込んだニューラルネットワーク生成フレームワークであるSEDを提案する。 SEDはまず、神経プログラムシンセサイザーコンポーネントを使用して初期プログラムを生成し、その後、神経プログラムデバッガを使用して生成されたプログラムを反復的に修復する。 挑戦的な入出力プログラム合成ベンチマークであるKarelでは、SEDはニューラルプログラムシンセサイザー自体のエラー率をかなりのマージンで削減し、デコードのための標準ビームサーチより優れている。
  論文  参考訳（メタデータ） (2020-07-16T04:15:47Z)
• Physarum Powered Differentiable Linear Programming Layers and Applications [48.77235931652611]
  一般線形プログラミング問題に対する効率的かつ微分可能な解法を提案する。 本稿では,ビデオセグメンテーションタスクとメタラーニングにおける問題解決手法について述べる。
  論文  参考訳（メタデータ） (2020-04-30T01:50:37Z)
• CounterExample Guided Neural Synthesis [12.742347465894586]
  プログラム合成は困難であり、形式的な保証を提供する方法はスケーラビリティの問題に悩まされる。 ニューラルネットワークとフォーマルな推論を組み合わせることで、論理的な仕様をニューラルネットワークを正しい解へと導く一連の例に変換する。 この結果から,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上することが示唆された。
  論文  参考訳（メタデータ） (2020-01-25T01:11:53Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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