Multimodal Pretrained Models for Verifiable Sequential Decision-Making: Planning, Grounding, and Perception

TL;DR

This paper introduces an algorithm that leverages multimodal pretrained models to construct, verify, and ground automaton-based controllers for sequential decision-making, providing formal guarantees and handling perceptual uncertainties in real-world tasks.

Contribution

It develops a novel method to integrate pretrained models into decision-making controllers with formal verification and grounding capabilities in visual environments.

Findings

Successfully constructs automaton-based controllers from pretrained models.

Provides probabilistic guarantees on controller correctness under perceptual uncertainties.

Demonstrates effectiveness on real-world daily life and robot manipulation tasks.

Abstract

Recently developed pretrained models can encode rich world knowledge expressed in multiple modalities, such as text and images. However, the outputs of these models cannot be integrated into algorithms to solve sequential decision-making tasks. We develop an algorithm that utilizes the knowledge from pretrained models to construct and verify controllers for sequential decision-making tasks, and to ground these controllers to task environments through visual observations with formal guarantees. In particular, the algorithm queries a pretrained model with a user-provided, text-based task description and uses the model's output to construct an automaton-based controller that encodes the model's task-relevant knowledge. It allows formal verification of whether the knowledge encoded in the controller is consistent with other independently available knowledge, which may include abstract information on the environment or user-provided specifications. Next, the algorithm leverages the vision and language capabilities of pretrained models to link the observations from the task environment to the text-based control logic from the controller (e.g., actions and conditions that trigger the actions). We propose a mechanism to provide probabilistic guarantees on whether the controller satisfies the user-provided specifications under perceptual uncertainties. We demonstrate the algorithm's ability to construct, verify, and ground automaton-based controllers through a suite of real-world tasks, including daily life and robot manipulation tasks.