11institutetext:  Barnard College, Columbia University

# Enforcing Temporal Constraints on Generative Agent Behavior with Reactive
Synthesis

Raven Rothkopf 11 0000-0002-3926-683X Hannah Tongxin Zeng 11
0000-0003-2011-3072 Mark Santolucito 11 0000-0001-8646-4364

###### Abstract

The surge in popularity of Large Language Models (LLMs) has opened doors for
new approaches to the creation of interactive agents. However, managing the
temporal behavior of such agents over the course of an interaction remains
challenging. The stateful, long-term horizon and quantitative reasoning
required for coherent agent behavior does not fit well into the LLM paradigm.
We propose a combination of formal logic-based program synthesis and LLM
content generation to create generative agents that adhere to temporal
constraints. Our approach uses Temporal Stream Logic (TSL) to generate an
automaton that enforces a temporal structure on an agent and leaves the
details of each action for a moment in time to an LLM. By using TSL, we are
able to augment the generative agent where users have a higher level of
guarantees on behavior, better interpretability of the system, and more
ability to build agents in a modular way. We evaluate our approach on
different tasks involved in creating a coherent interactive agent specialized
for various application domains. We found that over all of the tasks, our
approach using TSL achieves at least 96% adherence, whereas the pure LLM-based
approach demonstrates as low as 14.67% adherence.

###### Keywords:

Program Synthesis, Reactive Synthesis, Temporal Stream Logic, Large Language
Models, Human-AI Co-creation

##  1 Introduction

Large Language Models (LLMs) excel at acting as generative agents that should
have some self-consistency in their behavior. One such example is the use of
LLMs to create video game agents [28, 14]. However, one limitation is in the
ability to manage long-horizon behavioral consistency of such agents. Often,
when relying solely on LLMs to control agent behavior, the agent will display
behavior that is out of line with its previously established patterns [6].
While a certain amount of agent evolution can increase the depth of player
experience [5], players also expect in-game agents to have some consistency
over time [21]. Prior work has attempted to address the issues of agent memory
by logging an input-response history which can be used in future calls to a
LLM for content (e.g. NPC script). While these approaches have been shown to
create more natural conversation flows, for example with chain-of-thought
frameworks [50], the core problem of enforcing temporal consistency remains
unaddressed.

Enforcing temporal consistency for our work means to give structure to the
long-horizon behavior of an LLM. As an example, we may want to ensure that an
LLM-based teaching assistant for a CS101 class does not give example code with
nested conditionals before explaining what a conditional is and how it
functions. In order to convey such constraints on an LLM-based agent, users
must compose extensive prompts, scrutinize responses for potential factual
inaccuracies, biases, or content misaligned with their intentions, adjust
their prompts accordingly, and repeat the process. This creates the “Gulf of
Execution” [24], representing the divide between users’ intentions and the
system’s ability to fulfill them, leading to excessive back-and-forth in
crafting prompts for users to guide LLMs toward desired outputs. In addition,
there is the “Gulf of Evaluation” between the system’s output and users’
comprehension of how well these outputs align with their intentions. This lack
of interpretability of the model necessitates additional effort from the user
to understand how and why the LLM-based agent came up with its responses.

To bridge these two gulfs and to enforce temporally consistent agent behavior
in LLMs, we turn to temporal logic and program synthesis. We combine LLMs with
logic-based program synthesis techniques to build a system for creating
generative agents that are guaranteed to obey particular temporal properties
of the generative content. In this system, users provide a specification of
the temporal behavior to which their agent should adhere, and we synthesize an
interpretable system that structures LLM queries of the agent.

The key design goal of our approach is to provide a system which has three
main features: 1) adherence, 2) interpretability and 3) modularity. First, we
want to make sure the system adheres to the provided specification. Second,
the user should be able to identify the root cause of decisions made by the
agent. Third, the user should be able to build upon their specification in
modular way, such that properties can be added to the system without needing
to explore an invisible trade-off space between the properties.

Recognizing these design priorities, and that generative agents are at their
core reactive systems that consume input and produce output while maintaining
some internal state, we turn to the world of reactive synthesis. Reactive
synthesis allows us to take a specification of the long-horizon behavior of an
agent and generate a state machine that gives instructions (as a prompt
modifier) to the LLM on each state transition of how to generate its response.
To make decisions on how to transition between states, the LLM makes queries
on its own output and the user’s prompts at each time step. Interestingly,
despite using a self-evaluative model, we are able to achieve significantly
better results than state-of-the-art approaches that only rely on an LLM.

The key contributions of this work are as follows:

  1. 1.

A formalization of our generative agent and its properties of adherence,
interpretability, and modularity

  2. 2.

A prototype system that uses Temporal Stream Logic to impose temporal
constraints on generative agents

  3. 3.

An evaluation of this framework measuring temporal consistency compared to
existing chain-of-thought memory models.

##  2 Motivating Example

To explore a more in-depth example of where temporal consistency of an LLM-
agent is required, consider a simple choose-your-own-adventure game. Ideally,
we could use LLMs to generate dynamic story passages for interactions with
players, but we also want to require that the player visits three different
locations along their journey: a town, a market, and a cave. We also want to
ensure that the player visits a town and a market before they can visit a
cave. To create such an agent, we will use a combination of LLM calls and
Temporal Stream Logic (TSL) [19]. TSL allows us to write properties about the
temporal behavior of an agent, and then automatically generate code that is
guaranteed to meet those properties. Although we have not yet formally
introduced TSL, the specification of the player’s adventure is straightforward
to understand, as shown in Fig 1.

ALWAYS ASSUME

//Once the LLM is queried for a story passage where the player visits a cave,
in the next step, the player should be in a cave.

$\displaystyle\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\left([\texttt{storyPassage}\leftarrow\texttt{toCave(storySummary)}]\operatorname{\leftrightarrow}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{inCave(storySummary)}\right)$

//Once the LLM is queried for a story passage where the player visits a
market, eventually the player should be in a market.

$\displaystyle\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\left([\texttt{storyPassage}\leftarrow\texttt{toMarket(storySummary)}]\operatorname{\rightarrow}\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{inMarket(storySummary)}\right)$

//Once the LLM is queried for a story passage where the player visits a town,
eventually the player should be in a town.

$\displaystyle\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\left([\texttt{storyPassage}\leftarrow\texttt{toTown(storySummary)}]\operatorname{\rightarrow}\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{inTown(storySummary)}\right)$

ALWAYS GUARANTEE

//The player cannot go to cave until they have been in a market and a town.

$\displaystyle\neg\texttt{inCave(storySummary)}\operatorname{\mathcal{W}}\texttt{inMarket(storySummary)}\
\land$
$\displaystyle\neg\texttt{inCave(storySummary)}\operatorname{\mathcal{W}}\texttt{inTown(storySummary)}$

//Eventually, the player should visit the cave, the market, and the town.

$\displaystyle\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{toCave(storySummary)}\land\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{toMarket(storySummary)}\land\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\texttt{toTown(storySummary)})$

Figure 1: A specification written in Temporal Stream Logic that consistently
constrains the locations visited by the player along their journey through a
choose-your-own-adventure game.

There are no guarantees about the behavior of the component functions in this
specification, but by using TSL, we can construct an automaton that governs
the times when these functions are called. In this way, we allow the story to
change over time, and how the player navigates the story to change over time,
but the relationship between when these things happen will remain consistent.

##  3 Preliminaries

###  3.1 Limitations of LLMs in Co-creation

Based on user prompts, a form of text-based input, Large Language Models(LLMs)
excel at generating high-quality content for specific topics, tasks, or styles
[8, 27, 15]. Collaborating with an LLM, especially given its exceptional
generative capacity, requires users to relinquish partial control over the
generated content. Consequently, the creative results become a collaborative
effort through interactions between the individual (human) and the non-human
agent (LLM) [44], resulting in a form of human-AI co-creation [23]. A defining
feature of human-AI co-creation is the substantial contribution of non-human
input to the creative process, complementing the inputs from human users. Co-
creation occupies the space between pure computational creativity, where a
non-human agent creates without human involvement, and creative support tools,
software systems and interfaces assisting human users by enhancing their
abilities and offering new possibilities [22]. Aligning LLM output with user
intentions poses a critical challenge for both engineers designing and
developing the language model and users seeking improved results.

Due to its text-mediated interface and the black-box nature of artificial
neural nets, LLMs have several limitations in the context of human-LLM co-
creation.

  1. 1.

Adherence: Despite explicit instructions in prompts, the LLM might still
generate content that clearly violates the instructions–this challenge has
been termed loss of authorial control [36].

  2. 2.

Interpretability: Understanding why an LLM returns a particular block of text
can be difficult through the black-box internal workings of the model. When an
LLM produces an unexpected or undesired outcome, it can be hard to pinpoint
the cause from a series of interactions and correct accordingly.

  3. 3.

Modularity: LLMs fall short of representing a non-linear information structure
that involves more complex components such as conditionals and parallelism.
This is particularly an issue for enabling the iterative creation users
require for building complex systems.

###  3.2 Reactive Synthesis and Temporal Stream Logic

At the core of our work is the use of reactive synthesis [12]. Reactive
synthesis focuses on the temporally infinite interaction between the system
and its environment, and automatically constructs control strategies that
ensure that the system reacts to any possible move by the environment in a way
that adheres to the specification’s requirements. In the classical synthesis
setting, using specification languages such as Linear Temporal Logic [45],
time is discrete and inputs and outputs are given as vectors of Boolean
signals. _Temporal Stream Logic (TSL)_ [19] is a specification language that
provides an extra layer of abstraction that can be applied to input and output
values of arbitrary type (as opposed to only Boolean as in LTL). Specifically,
TSL introduces predicate terms, $\tau_{P}\in\mathcal{T}_{\\!P}$, which are
used to make observations on the environment, and function terms,
$\tau_{F}\in\mathcal{T}_{\\!F}$, which are used to construct output values.
Additionally, TSL introduces the notion of cell values - values which are
outputted by the system and piped back as input in the following timestep. The
grammar of a TSL formula, $\varphi$, is an extension to the grammar of LTL:

$\begin{array}[]{rl}\tau_{P}\
\;:=&\;\tau_{F}^{0}~{}\;\tau_{F}^{1}~{}\;\ldots~{}\;\tau_{F}^{n-1}\\\\[3.00003pt]
\tau_{F}\
\;:=&f~{}\;\tau_{F}^{0}~{}\;\tau_{F}^{1}~{}\;\cdots~{}\;\tau_{F}^{n-1}\\\\[3.00003pt]
\varphi\ \;:=&\;\tau_{P}\ \,|\ \,[\hskip 0.5pt\,\tau_{F}\hskip 0.5pt]\ \,|\
\,\neg\varphi\ \,|\ \,\varphi\wedge\varphi\ \,|\
\,\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\ \,|\
\,\varphi\operatorname{\mathcal{U}}\varphi\end{array}$

where $I\cup\mathbb{C}$ is an input stream or cell value, and
$O\cup\mathbb{C}$ is an output steam or cell value. Together, all the
available predicate names $andalltheavailablefunctionnames$form the set of
function symbols $\mathbb{F}$. A TSL formula describes a system that consumes
input $\mathcal{I}=\mathbb{I}\cup\mathbb{C}$ and produces output
$\mathcal{O}=\mathbb{O}\cup\mathbb{C}$.

The realizability problem of TSL is stated as: given a TSL formula $\varphi$,
is there a strategy $\sigma\in\mathcal{I}^{+}\to\mathcal{O}$ mapping a finite
input steam (since the beginning of time) to an output (at each particular
timestep), such that for any infinite input stream
$\iota\in\mathcal{I}^{\omega}$, and every possible interpretation of the
function symbols (some concrete implementation)
$\langle\cdot\rangle:\mathbb{F}\to\mathcal{F}$, the execution of that strategy
over the input $\sigma\\!\wr\iota$ satisfies $\varphi$, i.e.,

$\exists\sigma\in\mathcal{I}^{+}\to\mathcal{O}.\
\,\forall\iota\in\mathcal{I}^{\hskip 0.2pt\omega}.\
\,\forall\langle\cdot\rangle:\mathbb{F}\to\mathcal{F}.\
\,\sigma\\!\wr\iota,\iota\;\vDash_{\\!\langle\cdot\rangle}\varphi$

If such a strategy $\sigma$ exists, we say that $\sigma$ realizes $\varphi$.
The key insight here is that in TSL we specify a temporal relation of
predicate evaluations to function applications - abstracting away from what
these predicates and functions actually do to any underlying data. In TSL
synthesis, this model $\sigma$ can be turned into a block of program code that
describes a Mealy machine [34], where the transitions represent function and
predicate terms. For a full exposition of the formalism of TSL we refer the
reader to [19].

##  4 Generative Agents

The goal of this work is to build correct-by-construction generative agents.
To ground our notion of correctness, we need a formal definition of a
generative agent. We are specifically interested in generative agents that
take actions at discrete timesteps as a reaction to observations on their
environment and the history of prior environmental observations. In this work
we focus on a model where the environment and actions are all text-based,
though our approach is not specific to this (any datatype, such as JSON
objects, would also be fine).

This model of a generative agent matches closely with that of a reactive
system, and specifically a reactive system with a layer of data abstraction as
modeled by TSL. In our setting, a generative agent, $\mathcal{A}$, is a
reactive system which first consumes a stream of inputs $\mathcal{I}^{+}$ in
the form of environmental text inputs (inputs $\mathbb{I}$) and its own prior
outputs (cells $\mathbb{C}$). At each timestep, the generative agent may make
queries about these inputs (predicate terms . In our system, these predicates
are LLM queries (e.g. inCave(storySummary) \- cf. Sec. 5.1). After observing
the environment, the agent then should take an action. In our text-focused
model, this action is that of generating a new block of text - using the
terminology of TSL, the action would be framed as updating an output signal
with a function term. In particular, this function term is also a call to an
LLM, asking for the next passage of the story (e.g. toCave(storySummary) \-
cf. Sec. 5.1). Thus, for our work, a generative agent
$\mathcal{A}=(\sigma,\langle\cdot\rangle)$ is a tuple of a strategy $\sigma$
and an implementation $\langle\cdot\rangle$ of the function and predicate
terms ($\mathbb{F}$) provided in the specification. The implementation
$\langle\cdot\rangle$ in our case, corresponds to a particular version of an
LLM. We briefly note that we also need to fix a random seed [38] in the LLM to
ensure each generation is deterministic and is a pure function (the same input
gives the same output every time) to match the model of TSL [19].

Critically, a synthesized strategy realizing a TSL specification must be valid
for any implementation of the function and predicate terms. This universal
quantification of data manipulation is particularly well-suited for the
context of LLMs, where the LLM behavior is treated as a black-box. The
correctness of synthesis is in this way divorced from the inner-workings of
the LLM.

##  5 System Overview

Our proposed system combines reactive synthesis with an LLM, using reactive
synthesis to control the high-level temporal reasoning while leaving the low-
level details of each response to the LLM. In this way, the reactive synthesis
(and specifically the resulting automaton) controls the top level of the
system, while LLM calls make up the computations that should happen at each
transition step of the automaton.

We note that adhering to temporal properties (reactive synthesis) is in some
ways fundamentally the same problem as probabilistic token-by-token generation
(LLMs). In both cases, we care about the relation of generated values in
sequence. The key contribution of the automata as mediating systems for LLM
generation is that, with TSL, we can directly encode our desired long-horizon
temporal behavior. In contrast, when using an LLM we must use prompt
engineering to communicate our desired behavior in natural language - which is
an error-prone, time-consuming task that still gives unreliable results.
Conceptually we expect this strategy to work well, as the structure of an
automaton is relatively simple (even a few hundred states compares favorably
to billions of parameters), lightening the load on the LLM. By leveraging a
hybrid of formal methods and LLMs, we can drive content generation in a way
that allows the LLM to focus on a shorter context window.

Although the automaton is the key mediator of the LLM behavior, using
specifications to generate this automaton through reactive synthesis is a
critical part of the system and usability design. In particular, with the
temporal logic specification, we are able to deliver modularity to users. That
is, a user can add a new line of specification to their system and still be
guaranteed that the system will preserve the behavior of the prior system as
well as integrate the new behavior. This modularity is notoriously difficult
to achieve with natural language prompt engineering [10].

In Fig. 2, we provide an overview of our system in action on a choose-your-
own-adventure specification. The system first determines a content prompt for
generating new text content based off of an self-evaluation of previously
generated passages. These prompts are passed to the LLM. Second, the LLM
generates passages and player choices according to the given content prompt.
Third, the LLM proofreads its own output and judges its alignment with users’
intention based on the evaluation prompt. These self-evaluations are then used
in the next time step and the process is repeated indefinitely111An
implementation of our system in the context of a CYOA game can be found here:
https://barnard-pl-labs.github.io/CYOA-TSL/.

additions circular distance=4cm, font=, text width=4.5cm, module minimum
width=4.5cm, module minimum height=1.5cm, arrow tip=to, uniform arrow
color=true, border color=none, uniform color list=white for 4 items,
additions= additional item font=, additional item text width=4.5cm, additional
item width=0cm, additional item offset=9mm, additional item border color=gray,
additional item shape=rectangle,

[circular diagram] LLM generates point-in-time responses according to the
state machine output, LLM generates choices for the user, LLM queries
properties of user choices and its own response, A synthesized state machine
from $\phi$ makes high level decisions about the narrative structure above of
module2/R: You approach a dark hallway…, below of module2/R: 1) You run down
the hall.
2) You check for traps., below of module4/P: Was the action risky?
Is the user in a cave?, above of module4/P: Generate a passage in a cave

Figure 2: A diagram of the system, providing examples of prompts (P:) sent to
the LLM and responses (R:).

###  5.1 Predicates and function terms

In our system, function terms like toCave(), toMarket(), and toTown() from
Sec. 2 represent calls to the LLM. In this example, these functions take a
summary of previous storyPassages, and query the LLM for a new passage where
the player visits a cave, market, or town. An example function term prompt for
toCave(storySummary) is:

“Compose a passage where the reader encounters a cave on their journey.”

The storySummary is also determined by a call to the LLM asking for a new
summary based on the previous summary and the most recent storyPassage. An
example summarization prompt is:

“You are writing a book and need to recall important points of the story so
far. Summarize the provided passage from about the story so far in moderate
detail, including the main character description, the locations visited, items
acquired, and interactions with other characters.”

Our system determines predicates like inCave(), inMarket(), and inTown() from
Sec. 2 using a self-evaluation method. In this example, after receiving a new
storyPassage from the function terms, the LLM is queried to evaluate if, based
on that new passage, the player is in a cave, market, or town. An example
predicate evaluation prompt for inCave(storySummary) is:

“Read this passage in an adventure story. Is the main character actively in a
cave or not? Respond ’0’ if it is false, or ’1’ if it is true.”

The LLM’s responses become the new values of each of the predicates used in
the next time step.

##  6 Generative Agent Correctness

Our architecture aims to address the aforementioned limitations of LLMs from
Sec. 3.1–adherence, interpretability, and modularity. These properties are not
well-defined concepts for LLMs and their generated content [29]. We again
leverage the separation of data and control that TSL provides, and define
these metrics “up to” the data level - taking a correctness modulo models
approach. That is, we can provide a guarantee on the adherence,
interpretability, and modularity on the control level of the generative agents
we create using TSL synthesis, even if we we cannot guarantee these properties
on the underlying models that are used as subcomponents in TSL.

###  6.1 Adherence

To formalize adherence we introduce two complementary concepts of _procedural
adherence_ and _point-in-time adherence_. Point-in-time adherence captures the
goal of self-consistency over one time step. That is, given a request for
generative content, a self-reflection on the output of that request will match
the original intent. As an example, if our generative agent is prompted for a
passage where the user visits a cave, then when the agent assesses its
response, it will evaluate that the generated content is in a cave. Through
the framework of TSL, point-in-time adherence is a property of a generative
agent $\mathcal{A}=(\sigma,\langle\cdot\rangle)$ that focuses on the
implementation of the function and predicate terms $\langle\cdot\rangle$.
Specifically, it is that, given a some abstract property $a$ (e.g. in a cave),
and a function $f_{a}()$ that should generate content with that property, the
output of that function can be checked by a complementary predicate $p_{a}()$.
This is captured by the TSL formula $\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\left([cell\leftarrow
f_{a}(...)]\operatorname{\rightarrow}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}(cell)\right)$.
An agent $\mathcal{A}=(\sigma,\langle\cdot\rangle)$ has point-in-time
adherence if all function and predicate terms have point-in-time adherence.

In contrast to point-in-time adherence, procedural adherence is a property
relating the strategy $\sigma$ of an agent
$\mathcal{A}=(\sigma,\langle\cdot\rangle)$ to the specification $\varphi$ from
which it was synthesized. Intuitively, the idea of procedural adherence is
that given a history of self-reflections (i.e. predicate evaluations), the
generative agent will attempt to generate a response (i.e. select an update
term) that matches the specification. Again, through the framework of TSL,
procedural adherence corresponds directly to the correctness of the synthesis
automaton from some specification $\varphi$. As long as the synthesis
procedure used to generate a strategy $\sigma$ is sound, the resultant agent
$\mathcal{A}=(\sigma,\langle\cdot\rangle)$, will have procedural adherence
with respect to $\varphi$, regardless of the choice of $\langle\cdot\rangle$.

###  6.2 Interpretability

We also aim to improve the interpretability of a black box autonomous agent by
using TSL to provide a layer of abstraction between the long-horizon,
procedural control and the point-in-time decisions. Causality is commonly used
as a way to formalize one aspect of the interpretabilty of machine learning
models [7, 48, 4] \- a system is interpretable when causality of its output
can be identified. For our system, we refer to the recent work on temporal
causality for reactive systems by Coenen et al. [13], which builds upon the
formalization of causality from Halpern and Pearl [42] by extending the
definition of causality to reactive systems that run on infinite streams of
input. Core to the notion of causality is that “a cause is an event such that,
if it had not happened, the effect would not have happened either” [13]. We
remark that the definition of an event itself is critical to the understanding
of interpretability in our system. In our system, the strategy $\sigma$ of an
agent $\mathcal{A}=(\sigma,\langle\cdot\rangle)$ is interpretable because for
any given choice of an update term, we can identify a predicate evaluation (or
a set of) such that if the predicate evaluation had been different, we would
have made a different choice of the update term. We know that we can indeed
always identify such a cause for our system because Coenen et al. show that
causality for reactive systems is decidable [13]. This gives us a high-level
procedural interpretabilty. Related work seeks to address this lower level of
interpretability [31]

###  6.3 Modularity

The modularity of our system means that given two realizable TSL formulas
$\varphi$, and $\varphi^{\prime}$, with minimal effort, we can compose these
two formulas together to get a third realizable formula,
$\varphi^{\prime\prime}$, that satisfies both $\varphi$ and
$\varphi^{\prime}$.

$\varphi\wedge\varphi^{\prime}\rightarrow\varphi^{\prime\prime}$

To enable an iterative creation process, users can build upon existing
versions of their specifications by modifying or adding one component at a
time. This allows users to break their ultimate goal into smaller sub-goals in
making sure that each iteration produces a functional version of their desired
program. The modular design of TSL also supports re-using of specifications,
allowing the user to scale successful design patterns. We note that while we
could have adherence and interpretability with manual automata construction
(as opposed to using TSL synthesis), it is TSL as a specification language
that gives us modularity.

##  7 Evaluation

In this section, we present a preliminary evaluation on the efficacy of
imposing temporal constraints on generative agents with Temporal Stream Logic
(TSL). We expand upon our motivating example in Sec 2 by evaluating our system
architecture in the context of an agent that generates choose-your-own-
adventure games. This evaluation demonstrates the adherence and modularity of
our system as opposed to a pure LLM-based system.

###  7.1 Methods

We measured how well the choose-your-own-adventure agent satisfied three
story-building tasks given by specifications written in TSL and the natural
language equivalent. The three tasks that the agent had to follow are shown
below.

  1. 1.

_“The player must visit a town and a market before they can visit a cave.”_

  2. 2.

_“The initial story setting must be a forest.”_

  3. 3.

_“If the player makes three safe choices along their journey and they are in a
cave, they must visit a town.”_

The first and second tasks resemble the TSL specification from the motivating
example in Section 2 and serve as a baseline comparison between the two
systems. The third task evaluates how well the TSL and natural language-based
approaches adhere to their guarantees for more complicated systems. The
concrete TSL specifications and natural language prompts corresponding to each
task can be found in Appendix 0.A.

We played 75 games with each system using the GPT-4 API for 20 time steps. We
then analyzed the percentage of games that resulted in hallucinations and/or
arithmetic errors vs. games where all guarantees were consistently satisfied
for all time steps with each method of specification. If a system guarantee
was violated in one time step of a run, e.g., if the player visited a cave
before either a town or market, the whole game was marked as a violating game.
We chose 75 games due to budget constraints.

###  7.2 Results

Table 1: Results of four different tasks constraining generative agent behavior, evaluated over 75 runs. Task |  Method |  States | Adherence (%) | Violations (%)
---|---|---|---|---
1 |  adventure.tsl |  8 | 96.00% | 4.00%
|  pure LLM |  - | 86.60% | 13.40%
2 |  adventure.tsl $\land$
forest.tsl |  9 | 96.00% | 4.00%
|  pure LLM |  - | 89.33% | 10.67%
3 |  adventure.tsl $\land$
choices.tsl |  16 | 98.67% | 1.33%
|  pure LLM |  - | 14.67% | 85.33%
4 |  adventure.tsl $\land$
choices.tsl $\land$
forest.tsl |  17 | 97.33% | 2.77%
|  pure LLM |  - | 16.00% | 84.00%
Table 2: Breakdown of specification violations by hallucination and arithmetic error over total violations across all runs and tasks. Method | Violating Runs | Total Runs
---|---|---
| Hallucinations | Arithmetic Errors |
TSL | 9 (3.00%) | 0 | 300
LLM | 43 (14.33%) | 101 (33.67%) | 300

In Table 1, we provide an evaluation of our system on the storytelling agent
described in Sec. 7.1. For each task, the TSL-based system achieved high
adherence, meaning that the game agent generated passages that consistently
behaved according to its tasks. While the TSL-based system is still at risk of
hallucinations, it is generally more reliable than the alternative. For Task 1
and 2, the agent also did fairly well at adhering to its pure LLM-based
specification and only hallucinated a cave or failed to generate a forest on
the first passage 13.4% and 10.67% of the time.

The benefits of TSL’s modularity are demonstrated in Tasks 3 and 4. Task 3
involves the combination of two distinct specifications, which regulate the
locations the player visits during the game and the impact of their choices on
gameplay. Task 4 is the combination of all three specifications outlined in
Sec 7.1. Combining two TSL specifications that impact different aspects of the
gameplay had no observable effect on how well the agent satisfied the system’s
guarantees.

In contrast, the pure LLM-based agent encountered challenges when tasked with
managing multiple objectives. In Task 3, the agent demonstrated an increased
tendency to hallucinate a cave in approximately 21% of the games, compared to
13% in Task 1. This 8% rise in cave hallucinations illustrates that as the
pure natural language prompts become more verbose, the consistency of the
generated output diminishes.

Table 2 highlights another significant finding: the pure LLM-based agent
exhibited simple arithmetic errors more than twice as often as hallucinations.
These errors involved inaccurately updating the count of safe choices the
player had made during their game, either by inconsistently increasing the
count or doing so when the player was not in a town. It is worth noting that
large language models often encounter challenges when generating responses to
numerical and mathematical queries, and this weakness has been deemed an
research area of critical importance [52]. As an alternative, TSL and reactive
synthesis offer a formally correct approach.

One clear limitation of this evaluation is the quality of the natural language
prompt we gave the pure LLM-based agent and its equivalency to the TSL
specification. However, it is worth noting that it took us less time to
engineer all TSL specifications than it took to engineer satisfactory natural
language prompts that ensured semi-consistent behavior from the pure LLM-based
agent for each task.

Overall, our preliminary evaluation suggests that the TSL-based approach
offers an adherent, modular, and interpretable solution for constraining
generative agent behavior in complex scenarios, outperforming pure LLM-based
agent specifications especially when dealing with computations.

###  7.3 Generalizability

Our system’s properties of adherence, interpretability, and modularity are
critical for domains other than choose-your-own-adventure games. More
generally, imposing temporal constraints on an autonomous agent could be used
to improve performance in any domain where an LLM-based chatbot must
continuously respond to input while keeping track of many variables
influencing the conversation, or when interacting with other autonomous
agents.

####  7.3.1 Educational Chatbot

The same design can be used on an educational chatbot that assists students as
they learn from a math textbook. There are many different ways to solve a
problem, and it is important that the chatbot does not give a student an
answer that contains material that is covered in a chapter that the student
has not covered yet. This property could be written as a TSL constraint like
so:

⬇

guarantee {

chapter1content(response) W chapter1complete;

(! (chapter2content(response))) W chapter1complete;

}

The chatbot should only respond using material covered in Chapter 1 of the
textbook until the student completes that chapter. The chatbot should not
respond using material from Chapter 2 until the student completes Chapter 1.
These constraints must extend to every chapter in the textbook, resulting in
many complex interactions that would be difficult for an LLM to manage without
help from formal methods.

At the same time, the chatbot may need to keep track of how many hints to a
sample problem it gives the student before it reveals the answer. For example,
using TSL, we can impose a threshold of three hints:

⬇

guarantee {

(! (giveAnswer(response)) W (hintCount = 3);

G (hint(response) <-> [hintCount <- hintCount + 1]);

}

####  7.3.2 Conversational generative agents

Generative agents powered by LLMs have had impressive performance of
improvising conversations based on their environment and previous
conversations [40]. TSL can be fused with such a system to offer guarantees in
the temporal priority of topics being mentioned in a conversation by different
speakers. Conceive a conversation between Alice and Bob. We use speakA to
represent Alice, and speakB for Bob. For example, the following specification
expresses that Alice always eventually talks about work:

⬇

always guarantee {

F ([speakA <- workTopic(summary)]);

}

To impose a constraint on the selection of topics, various expressions can be
used to prescribe the arrangement of one topic over another. For example, we
can use the $\operatorname{\mathcal{W}}$ (weak until) temporal operator to
offer a conditional preference, such as “Alice talks only about personal
topics after the conversation topic is about cats”.

⬇

always guarantee {

(! [speakA <- personalTopic(summary)] W isCatTopic(summary));

}

The following specification provides a more detailed example conversation.

⬇

always guarantee {

// Alice always eventually talks about work

F ([speakA <- workTopic(summary)]);

// Alice talks only about personal topics

// after the conversation topic is about cats

(! [speakA <- personalTopic(summary)] W isCatTopic(summary));

// Alice will eventually talk about future plans

// after talking about work

(isWorkTopic(summary) -> F ([speakA <- futurePlans(summary)]));

// Bob always follows with a joke when talking about future plan

isFuturePlanTopic(summary) -> [speakB <- joke(summary)];

}

##  8 Threats to validity

The threats to the internal validity of our evaluation correspond to the lack
of more complex prompt engineering techniques, a limited budget, and the
general complexity of LLMs. Each task could have been evaluated over more
games to allow for broader assertions about LLM behavior and hallucinations.
Conceivably, we could have improved our prompt engineering and paired the LLM
with a monitor to check each response before outputting it to the user. This
would have enabled us to regenerate the response if it failed to adhere to its
specifications. To partially mitigate these threats, we chose to use GPT-4 to
compare against the state-of-the-art. We could have implemented and evaluated
adherence for each of the domains described in 7.3 if the cost of GPT-4
queries were not a concern. Additionally, prior work has shown that it is also
difficult to evaluate LLM performance due to the lack of transparency and
complexity of the model [39].

One threat to the external validity of our work is the well-studied problem of
program synthesis and temporal logic usability [26, 47, 16, 51]. There is
still a barrier to writing TSL and other specification languages for program
synthesis, as they do not share syntax with common programming languages and
are semantically complex. One way to solve this is to provide better tools for
writing specifications. Prior work proposed a visual scripting tool to make it
more usable and approachable for programmers of all skill levels [47]. The
next phase of our work involves the seamless integration of tools to enhance
TSL usability within the current architecture.

Furthermore, the efficacy of our framework is contingent upon its design,
rendering it more suited for certain tasks than others. Since TSL introduces
temporal logic, users must articulate their intentions within the framework of
TSL semantics. Consequently, tasks involving temporal operations or possessing
sequential properties stand to gain greater advantages from the incorporation
of temporal logic.

A threat to the construct validity of our work is the indeterminacy of point-
in-time adherence and interpretability. For our purposes, we formalize
_procedural_ adherence and interpretability in Secs 6.1 and 6.2 as they
pertain to our definition of generative agents, but their complementary point-
in-time concepts remain undefined in the NLP field.

Despite these limitations, our results serve as a targeted case study and
proof of concept for the combination of formal methods and LLM generation.
Even with tweaked prompt engineering to improve the adherence of LLM generated
responses, the problems of interpretability and modularity still remain.
Further research and experimentation will be essential for a comprehensive
understanding of the strengths and limitations of our approach.

##  9 Related Work

####  9.0.1 Program synthesis and LLMs.

One current research direction in the intersection between program synthesis
and Large Language Models is to generate formal language specifications, such
as Linear Temporal Logic (LTL) formulae, using LLMs. These language models are
able to translate natural language into executable robot plans for tasks
including navigation [30], carrying out cooking recipes [33] and arranging
objects [49]. They are verified to achieve near–or equal–accuracy when
compared to human-generated specifications. This body of work is primarily
motivated by automating the formalism so that humans are not required in the
synthesis process, which is distinct from our goal to facilitate co-creation
between humans and LLMs. Because the measure of success in this line of work
is often the accuracy of LTL formulae, some of these approaches [41] trained
specialized language models to acquire significant knowledge about LTL.

Another active area of work is text-to-code generation, using LLMs to
synthesize programs from natural language descriptions, in a sense in place of
specification languages [37, 25, 11]. Despite generating functionally correct
programs after few-shot learning, these models fall short of understanding the
semantics, as measured by successfully predicting program output given
specific inputs, of the programs they generated. While this approach lowers
the barrier of entry to program synthesis by allowing users to input natural
language only, the similar issue of the evaluation gulf in directly
interacting with LLMs persists.

Our work is distinct from existing lines of research in the intersection of
program synthesis and LLMs in the aspects of system design and design goals.

####  9.0.2 Increasing adherence in LLMs.

Hallucinations in LLM outputs–namely, the plausible yet ungrounded information
[17]–can lead to inconsistency and factual errors in conversations and
generated explanations [9, 3, 1]. Verification methods, whether executed and
planned internally by the LLM (referred to as self-critique) [46, 32, 17],
coordinated among different LLMs to find agreement [18], or completed outside
the LLM framework entirely [35], contribute diverse approaches to addressing
hallucinations. Enhancing the reasoning capacity of LLMs, including
arithmetic, symbolic, and commonsense reasoning, is another way to reduce
hallucinations. In this context, our work can be understood as adding a
reasoning component to LLMs for verifying temporal consistency in its outputs.
Compared to previous work that enhances reasoning ability in specific domains,
such as reading comprehension [2] and mathematics [20, 43], our work aims to
facilitate reasoning of LLMs in the temporal domain, irrespective of the
nature of tasks.

##  10 Conclusion

This paper presents a working system that combines formal logic-based program
synthesis with Large Language Model (LLM) content generation. Supported by
Temporal Stream Logic (TSL), this system allows for the imposition of temporal
constraints on LLM generated content, extending the application of reactive
synthesis. In the evaluation of our system, we demonstrated its efficacy in
constraining the behavior of a choose-your-own-adventure game agent through a
set of predefined tasks. The benefits of TSL’s modular nature were highlighted
in the successful simultaneous adherence to a combination of tasks.

Furthermore, our proposed system addresses the challenges and limitations
associated with human-AI co-creation, particularly in the context of LLMs.
Through a cyclical process, our architecture provides users with guaranteed
control over coherency in LLM generation, ensuring that user intentions are
effectively translated into the final outputs. The introduction of procedural
interpretabiliity in the system architecture allows users to comprehend and
explain decision-making processes at both high and low levels. Furthermore,
the iterative creation process facilitated by our architecture empowers users
to refine and experiment with their specifications incrementally.

### Acknowledgements

This material is based upon work supported by the National Science Foundation
under Grant No. CCF-2105208.

## References

  * [1] Daniel Adiwardana et al.  “Towards a human-like open-domain chatbot”  In _arXiv preprint arXiv:2001.09977_ , 2020
  * [2] Daniel Andor, Luheng He, Kenton Lee and Emily Pitler  “Giving BERT a calculator: Finding operations and arguments with reading comprehension”  In _arXiv preprint arXiv:1909.00109_ , 2019
  * [3] Jacob Austin et al.  “Program synthesis with large language models”  In _arXiv preprint arXiv:2108.07732_ , 2021
  * [4] Christel Baier et al.  “From verification to causality-based explications”  In _arXiv preprint arXiv:2105.09533_ , 2021
  * [5] Russell Beale and Chris Creed  “Affective interaction: How emotional agents affect users”  In _International journal of human-computer studies_ 67.9 Elsevier, 2009, pp. 755–776
  * [6] Marcel Binz and Eric Schulz  “Using cognitive psychology to understand GPT-3”  In _Proceedings of the National Academy of Sciences_ 120.6 National Acad Sciences, 2023, pp. e2218523120
  * [7] Emily Black, Zifan Wang, Matt Fredrikson and Anupam Datta  “Consistent counterfactuals for deep models”  In _arXiv preprint arXiv:2110.03109_ , 2021
  * [8] Tom Brown et al.  “Language models are few-shot learners”  In _Advances in neural information processing systems_ 33, 2020, pp. 1877–1901
  * [9] Oana-Maria Camburu et al.  “Make up your mind! adversarial generation of inconsistent natural language explanations”  In _arXiv preprint arXiv:1910.03065_ , 2019
  * [10] Yu Cheng et al.  “Prompt Sapper: A LLM-Empowered Production Tool for Building AI Chains”  In _arXiv preprint arXiv:2306.12028_ , 2023
  * [11] Fenia Christopoulou et al.  “Pangu-coder: Program synthesis with function-level language modeling”  In _arXiv preprint arXiv:2207.11280_ , 2022
  * [12] Alonzo Church  “Applications of recursive arithmetic to the problem of circuit synthesis” 1, Summaries of the Summer Institute of Symbolic Logic at Cornell University, 1957
  * [13] Norine Coenen et al.  “Temporal causality in reactive systems”  In _International Symposium on Automated Technology for Verification and Analysis_ , 2022, pp. 208–224  Springer
  * [14] Maximilian Croissant, Madeleine Frister, Guy Schofield and Cade McCall  “An Appraisal-Based Chain-Of-Emotion Architecture for Affective Language Model Game Agents”  In _arXiv preprint arXiv:2309.05076_ , 2023
  * [15] Sumanth Dathathri et al.  “Plug and play language models: A simple approach to controlled text generation”  In _arXiv preprint arXiv:1912.02164_ , 2019
  * [16] Nicoletta De Francesco, Antonella Santone and Gigliola Vaglini  “A user-friendly interface to specify temporal properties of concurrent systems”  In _Information Sciences_ 177.1 Elsevier, 2007, pp. 299–311
  * [17] Shehzaad Dhuliawala et al.  “Chain-of-Verification Reduces Hallucination in Large Language Models”, 2023  arXiv:2309.11495 [cs.CL]
  * [18] Yilun Du et al.  “Improving Factuality and Reasoning in Language Models through Multiagent Debate”  In _arXiv preprint arXiv:2305.14325_ , 2023
  * [19] Bernd Finkbeiner, Felix Klein, Ruzica Piskac and Mark Santolucito  “Temporal stream logic: Synthesis beyond the bools”  In _International Conference on Computer Aided Verification_ , 2019  Springer
  * [20] Mor Geva, Ankit Gupta and Jonathan Berant  “Injecting numerical reasoning skills into language models”  In _arXiv preprint arXiv:2004.04487_ , 2020
  * [21] Kiel Gilleade, Alan Dix and Jen Allanson  “Affective videogames and modes of affective gaming: assist me, challenge me, emote me”  In _DiGRA 2005: Changing Views–Worlds in Play._ , 2005
  * [22] Ning Gu and Peiman Amini Behbahani  “A critical review of computational creativity in built environment design”  In _Buildings_ 11.1 MDPI, 2021, pp. 29
  * [23] Oliver Hoffmann  “On modeling human-computer co-creativity”  In _Knowledge, Information and Creativity Support Systems: Selected Papers from KICSS’2014-9th International Conference, held in Limassol, Cyprus, on November 6-8, 2014_ , 2016, pp. 37–48  Springer
  * [24] Edwin L Hutchins, James D Hollan and Donald A Norman  “Direct manipulation interfaces”  In _Human–computer interaction_ 1.4 Taylor & Francis, 1985, pp. 311–338
  * [25] Naman Jain et al.  “Jigsaw: Large language models meet program synthesis”  In _Proceedings of the 44th International Conference on Software Engineering_ , 2022, pp. 1219–1231
  * [26] Dhanya Jayagopal, Justin Lubin and Sarah E Chasins  “Exploring the learnability of program synthesizers by novice programmers”  In _Proceedings of the 35th Annual ACM Symposium on User Interface Software and Technology_ , 2022, pp. 1–15
  * [27] Nitish Shirish Keskar et al.  “Ctrl: A conditional transformer language model for controllable generation”  In _arXiv preprint arXiv:1909.05858_ , 2019
  * [28] Gaetan Lopez Latouche, Laurence Marcotte and Ben Swanson  “Generating Video Game Scripts with Style”  In _Proceedings of the 5th Workshop on NLP for Conversational AI (NLP4ConvAI 2023)_ , 2023, pp. 129–139
  * [29] Zachary C Lipton  “The mythos of model interpretability: In machine learning, the concept of interpretability is both important and slippery.”  In _Queue_ 16.3 ACM New York, NY, USA, 2018, pp. 31–57
  * [30] Jason Xinyu Liu et al.  “Lang2ltl: Translating natural language commands to temporal specification with large language models”  In _Workshop on Language and Robotics at CoRL 2022_ , 2022
  * [31] Linhao Luo, Yuan-Fang Li, Gholamreza Haffari and Shirui Pan  “Reasoning on graphs: Faithful and interpretable large language model reasoning”  In _arXiv preprint arXiv:2310.01061_ , 2023
  * [32] Potsawee Manakul, Adian Liusie and Mark JF Gales  “Selfcheckgpt: Zero-resource black-box hallucination detection for generative large language models”  In _arXiv preprint arXiv:2303.08896_ , 2023
  * [33] Angelos Mavrogiannis, Christoforos Mavrogiannis and Yiannis Aloimonos  “Cook2LTL: Translating Cooking Recipes to LTL Formulae using Large Language Models”  In _arXiv preprint arXiv:2310.00163_ , 2023
  * [34] George H Mealy  “A method for synthesizing sequential circuits”  In _The Bell System Technical Journal_ 34.5 Nokia Bell Labs, 1955, pp. 1045–1079
  * [35] Sewon Min et al.  “FActScore: Fine-grained Atomic Evaluation of Factual Precision in Long Form Text Generation”  In _arXiv preprint arXiv:2305.14251_ , 2023
  * [36] Norman Mu et al.  “Can LLMs Follow Simple Rules?”  In _arXiv preprint arXiv:2311.04235_ , 2023
  * [37] Erik Nijkamp et al.  “Codegen: An open large language model for code with multi-turn program synthesis”  In _arXiv preprint arXiv:2203.13474_ , 2022
  * [38] OpenAI  “OpenAI Documentation: Reproducable Outputs” https://platform.openai.com/docs/guides/text-generation/reproducible-outputs, 2023
  * [39] Shuyin Ouyang, Jie M Zhang, Mark Harman and Meng Wang  “LLM is Like a Box of Chocolates: the Non-determinism of ChatGPT in Code Generation”  In _arXiv preprint arXiv:2308.02828_ , 2023
  * [40] Joon Sung Park et al.  “Generative agents: Interactive simulacra of human behavior”  In _Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology_ , 2023, pp. 1–22
  * [41] Roma Patel, Roma Pavlick and Stefanie Tellex  “Learning to ground language to temporal logical form”  In _Conference of the North American Chapter of the Association for Computational Linguistics (NAACL)_ , 2019
  * [42] Judea Pearl  “Causes and Explanations: A Structural-Model Approach. Part Ii: Explanations”  In _British Journal for the Philosophy of Science_ 56.4 University of Chicago Press, 2005, pp. 889–911  DOI: 10.1093/bjps/axi148
  * [43] Piotr Piekos, Henryk Michalewski and Mateusz Malinowski  “Measuring and Improving BERT’s Mathematical Abilities by Predicting the Order of Reasoning”  In _arXiv preprint arXiv:2106.03921_ , 2021
  * [44] Jonathan A Plucker, Ronald A Beghetto and Gayle T Dow  “Why isn’t creativity more important to educational psychologists? Potentials, pitfalls, and future directions in creativity research”  In _Educational psychologist_ 39.2 Taylor & Francis, 2004, pp. 83–96
  * [45] Amir Pnueli  “The temporal logic of programs”  In _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_ , 1977, pp. 46–57  ieee
  * [46] Ofir Press et al.  “Measuring and narrowing the compositionality gap in language models”  In _arXiv preprint arXiv:2210.03350_ , 2022
  * [47] Raven Rothkopf et al.  “Towards the Usability of Reactive Synthesis: Building Blocks of Temporal Logic”, 2023  Plateau Workshop
  * [48] Sahil Verma et al.  “Counterfactual explanations and algorithmic recourses for machine learning: A review”  In _arXiv preprint arXiv:2010.10596_ , 2020
  * [49] Christopher Wang et al.  “Learning a natural-language to LTL executable semantic parser for grounded robotics”  In _Proceedings of the 2020 Conference on Robot Learning_ 155, Proceedings of Machine Learning Research  PMLR, 2021, pp. 1706–1718  URL: https://proceedings.mlr.press/v155/wang21g.html
  * [50] Jason Wei et al.  “Chain-of-thought prompting elicits reasoning in large language models”  In _Advances in Neural Information Processing Systems_ 35, 2022, pp. 24824–24837
  * [51] Seiji Yamashita, Masateru Tsunoda and Tomoyuki Yokogawa  “Visual programming language for model checkers based on google blockly”  In _Product-Focused Software Process Improvement: 18th International Conference, PROFES 2017, Innsbruck, Austria, November 29–December 1, 2017, Proceedings 18_ , 2017, pp. 597–601  Springer
  * [52] An-Zi Yen and Wei-Ling Hsu  “Three questions concerning the use of large language models to facilitate mathematics learning”  In _arXiv preprint arXiv:2310.13615_ , 2023

##  Appendix 0.A Appendix A

###  0.A.1 Task 1 specs

adventure.tsl

⬇

initially assume {

! getCave;

! getMarket;

! getTown;

}

always assume {

[passageTarget <- toCave] <-> X getCave;

[passageTarget <- toMarket] -> F getMarket;

[passageTarget <- toTown] -> F getTown;

}

guarantee {

(! (getCave)) W (getMarket);

(! (getCave)) W (getTown);

}

always guarantee {

F getCave;

F getMarket;

F getTown;

}

Natural language prompt example:  ”You are writing a choose your own adventure
book. Compose a one paragraph-long passage of the story of at most 100 words.
The paragraph should end just before a critical choice. Do not specify
choices. Write in the present tense. The player cannot visit a cave until they
visit a town. The player cannot visit a cave until they visit a market. The
player will eventually visit a town. The player will eventually visit a
market. The player will eventually visit a cave. After the player visits a
town and a market, they must visit a cave. The player may visit these
locations in a later passage.”

###  0.A.2 Task 2 Specs

forest.tsl

⬇

initially guarantee {

[passageTarget <- toForest]

}

Natural language prompt example:  ”If this is the first passage of the story,
you should write an introductory passage of the story starting which describes
the character and the setting. The initial setting must be a forest, not a
market, town or cave.”

###  0.A.3 Task 3 Specs

adventure.tsl && choices.tsl

⬇

initially assume {

! safeThreshold;

! getCave;

! getTown;

! getMarket;

}

always assume {

[safeCount <- safeCount + 1] -> F safeThreshold;

[passageTarget <- toCave] <-> X getCave;

[passageTarget <- toTown] -> F getTown;

[passageTarget <- toMarket] -> F getMarket;

}

guarantee {

(safeThreshold && getCave) -> F getTown;

(! (getCave)) W (getTown);

(! (getCave)) W (getMarket);

}

always guarantee {

(safe && getTown) <-> [safeCount <- safeCount + 1];

F getCave;

F getTown;

F getMarket;

}

Natural language prompt example:  ”You are writing a choose your own adventure
book. Compose a one paragraph-long passage of the story of at most 100 words.
The paragraph should end just before a critical choice. Do not specify
choices. Write in the present tense. The player cannot visit a cave until they
visit a town. The player cannot visit a cave until they visit a market. The
player will eventually visit a town. The player will eventually visit a
market. The player will eventually visit a cave. After the player visits a
town and a market, they must visit a cave. The player may visit these
locations in a later passage. If the player is in the town and makes a safe
choice, the ‘safeCount‘ count variable should be incremented by 1. The current
amount of safe choices made is: 0. The the player just made a neutral choice.
Once the player has made 3 safe choices and they are in a cave, they should go
to a town. Make sure to output the current amount of safe choices made in the
form: ‘safeCount=x‘ at the beginning of each story passage and then include
the story, but remember that this variable can only be updated if the player
is in a town, which right now, is false.”