Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
This addresses the problem of scalable program synthesis for LTL specifications, which is incremental as it combines existing search and deep learning techniques.
The paper tackles the scalability issue of exact Linear Temporal Logic (LTL) synthesis by casting it as an optimization problem and using a neural network to learn a Q-function for guiding search, achieving effective guidance for small 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.