Encoding formulas as deep networks: Reinforcement learning for zero-shot execution of LTL formulas

TL;DR

This paper presents a reinforcement learning approach using a compositional neural network that can zero-shot generalize to satisfy unseen LTL formulas in symbolic and simulated environments, enabling complex task execution without additional training.

Contribution

It introduces a neural network architecture capable of zero-shot generalization to new LTL formulas, advancing multi-task reinforcement learning and formal logic encoding.

Findings

Network successfully generalizes to unseen formulas in symbolic domain

Agent finds action sequences conforming to formulas in a Minecraft-like environment

Demonstrates encoding of all formulas reliably for zero-shot execution

Abstract

We demonstrate a reinforcement learning agent which uses a compositional recurrent neural network that takes as input an LTL formula and determines satisfying actions. The input LTL formulas have never been seen before, yet the network performs zero-shot generalization to satisfy them. This is a novel form of multi-task learning for RL agents where agents learn from one diverse set of tasks and generalize to a new set of diverse tasks. The formulation of the network enables this capacity to generalize. We demonstrate this ability in two domains. In a symbolic domain, the agent finds a sequence of letters that is accepted. In a Minecraft-like environment, the agent finds a sequence of actions that conform to the formula. While prior work could learn to execute one formula reliably given examples of that formula, we demonstrate how to encode all formulas reliably. This could form the basis of new multitask agents that discover sub-tasks and execute them without any additional training, as well as the agents which follow more complex linguistic commands. The structures required for this generalization are specific to LTL formulas, which opens up an interesting theoretical question: what structures are required in neural networks for zero-shot generalization to different logics?