Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Program SynthesisSimilar Papers 제목 키워드 기반
idSTLPy: A Python Toolbox for Active Perception and Control
This paper describes a Python toolbox for active perception and control synthesis of probabilistic signal temporal logic (PrSTL) formulas of switched linear systems with additive Gaussian disturbances and measurement noi…
Motion PlanningLTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
We investigate the synthesis of policies for high-level agent programs expressed in Golog, a language based on situation calculus that incorporates nondeterministic programming constructs. Unlike traditional approaches f…
Direct data-driven control with signal temporal logic specifications
Most control synthesis methods under temporal logic properties require a model of the system, however, identifying such a model can be a challenging task. In this work, we develop a direct data-driven control synthesis m…
Toward Neural-Network-Guided Program Synthesis and Verification
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 integer…
Program SynthesisEvaluating Implicit Regulatory Compliance in LLM Tool Invocation via Logic-Guided Synthesis
The integration of large language models (LLMs) into autonomous agents has enabled complex tool use, yet in high-stakes domains, these systems must strictly adhere to regulatory standards beyond simple functional correct…