# Programming-by-Demonstration for Long-Horizon Robot Tasks (Extended Version)

Noah Patton  Research AssistantDepartment of Computer ScienceThe University of
Texas at AustinAustinTexasUSA<EMAIL_ADDRESS>0009-0002-7028-518X ,  Kia
Rahmani  Postdoctoral FellowDepartment of Computer ScienceThe University of
Texas at AustinAustinTexasUSA<EMAIL_ADDRESS>0000-0001-9064-0797 ,  Meghana
Missula  Research AssistantDepartment of Computer ScienceThe University of
Texas at AustinAustinTexasUSA<EMAIL_ADDRESS>0000-0002-1610-6198 ,
Joydeep Biswas  Associate ProfessorDepartment of Computer ScienceThe
University of Texas at AustinAustinTexasUSA<EMAIL_ADDRESS>0000-0002-1211-1731 and  Işıl Dillig  ProfessorDepartment of Computer
ScienceThe University of Texas at AustinAustinTexasUSA<EMAIL_ADDRESS>0000-0001-8006-1230

(2024; 2023-07-11; 2023-11-07)

###### Abstract.

Abstract. The goal of _programmatic Learning from Demonstration (LfD)_ is to
learn a policy in a programming language that can be used to control a robot’s
behavior from a set of user demonstrations. This paper presents a new
programmatic LfD algorithm that targets _long-horizon robot tasks_ which
require synthesizing programs with complex control flow structures, including
nested loops with multiple conditionals. Our proposed method first learns a
program sketch that captures the target program’s control flow and then
completes this sketch using an LLM-guided search procedure that incorporates a
novel technique for proving unrealizability of programming-by-demonstration
problems. We have implemented our approach in a new tool called prolex and
present the results of a comprehensive experimental evaluation on 120
benchmarks involving complex tasks and environments. We show that, given a 120
second time limit, prolex can find a program consistent with the
demonstrations in 80% of the cases. Furthermore, for 81% of the tasks for
which a solution is returned, prolex is able to find the ground truth program
with just one demonstration. In comparison, CVC5, a syntax-guided synthesis
tool, is only able to solve 25% of the cases _even when given the ground truth
program sketch_ , and an LLM-based approach, GPT-Synth, is unable to solve any
of the tasks due to the environment complexity.

Abstract Interpretation, Program Synthesis, Learning from Demonstrations

††copyright: rightsretained††doi: 10.1145/3632860††journalyear:
2024††submissionid: popl24main-p83-p††journal: PACMPL††journalvolume:
8††journalnumber: POPL††article: 18††publicationmonth: 1††ccs: Computing
methodologies Robotic planning††ccs: Theory of computation Abstraction††ccs:
Theory of computation Grammars and context-free languages††ccs: Theory of
computation Action semantics††ccs: Theory of computation Program
analysis††ccs: Software and its engineering Automatic programming

##  1\. Introduction

Learning From Demonstration (LfD) is an attractive paradigm for teaching
robots how to perform novel tasks in end-user environments (Argall et al.,
2009). While most classical approaches to LfD are based on black-box behavior
cloning (Ly and Akhloufi, 2021; Ho and Ermon, 2016), recent work has argued
for treating LfD as a program synthesis problem (Holtz et al., 2020a; Xin et
al., 2023; Porfirio et al., 2023). In particular, _programmatic LfD_
represents the space of robot policies in a domain-specific language (DSL) and
learns a program that is consistent with the user’s demonstrations.

Although this programmatic approach has been shown to offer several advantages
over black-box behavior cloning in terms of data efficiency, generalizability,
and interpretability (Holtz et al., 2021; Lipton, 2018), existing work in this
space suffers from three key shortcomings: First, most prior techniques focus
on simple Markovian policies that select the _next_ action based only on the
current state. As a result, the target programs have a simple decision-list
structure, and the main difficulty lies in inferring suitable predicates for
each branch. Second, most existing techniques have only been applied to
restricted domains with limited object and interaction types, such as robot
soccer playing where the entities of interest are known a priori and comprise
a small set.

Our goal in this work is to develop a programmatic LfD approach for _long-
horizon_ tasks that commonly arise in service mobile robot settings — e.g.,
putting away groceries in a domestic setting, or proactively providing tools
and parts to a mechanic in assistive manufacturing. Long-horizon robotics
tasks are inherently more challenging, as the robot needs to reason about the
interactions between a long _sequence of actions_ (e.g., that the dishes must
be cleared from a table before it can be wiped down) and the _effect of
specific environmental states_ on sequences of actions (e.g., a robot tasked
with dusting a shelf must first remove all items from the shelf if it is not
empty vs. directly dusting it if there are no items on it). This is in stark
contrast to control tasks, such as motion control, where the policy just needs
to select the next action for a single time step.

Recognizing the importance of long horizon tasks, recent work (Porfirio et
al., 2023) has proposed a multi-modal user interface (combining natural
language with hand-drawn navigation paths) to facilitate programmatic LfD in
this setting. This paper makes another stride towards that goal, but in an
orthogonal direction, by learning more complex programs from demonstration
traces. In particular, the approach that we propose in this paper aims to (a)
handle tasks that require complex control flow (such as nested loops with
multiple conditionals) and (b) scale to demonstrations performed in complex
environments with hundreds of objects and a large number of relationships to
consider between those objects.

Figure 1. Overview of prolex

Our proposed approach tackles these two challenges using a novel program
synthesis algorithm that is illustrated schematically in Figure 1. First,
given a set of demonstration traces, our approach infers a control flow sketch
of the target program. To do so, our method abstracts each demo trace as a
string over a finite alphabet and then learns a set of simple regular
expressions that “unify” all of the demonstrations. As there is an obvious
correspondence between regex operators and control flow structures (e.g.,
loops as Kleene star; conditionals as disjunction), our method can quickly
infer the control flow structure of the target program from a small number of
demonstrations. Furthermore, because the sketch learner prefers small regular
expressions over complex ones, this application of the Occam’s razor principle
introduces inductive bias towards control structures that are more likely to
generalize to unseen traces.

Given a program sketch capturing the underlying control flow structure, the
second _sketch completion_ phase of our algorithm tries to find a complete
program that is consistent with the given traces. This algorithm is based on
top-down enumerative search, meaning that it starts by considering all DSL
programs as part of the search space and gradually refines it until it
contains a single program. However, because the size of the search space is
exponential with respect to the number of entities in the environment, such a
search strategy does not scale to complex environments. Our approach deals
with this challenge using two key ideas, namely (1) guiding the search
procedure using a large language model (LLM), and (2) proving unrealizability
of synthesis sub-problems.

LLM-guided refinement. As shown in Figure 1 (and as standard in the
literature), our sketch completion procedure represents the search space as a
_partial program_ (i.e., a program containing _holes_), so the refinement step
involves filling one of the holes in this partial program with a concrete
expression. In our setting, these holes need to be instantiated with objects
(or object types) in the environment, as well as properties of –and
relationships between– those objects. However, because the demonstration may
be performed in complex environments with many such objects and properties,
each hole typically has a very large number of possible completions. To
address this problem, our method consults an LLM to perform refinement;
intuitively, this serves two purposes: First, when the target program contains
object types that do not explicitly occur in the demonstrations (a very common
scenario), LLM guidance allows the synthesizer to propose new entities by
reasoning about commonalities between objects that do occur in the
demonstrations. Second, by conditioning the current prediction on previous
ones, the synthesizer can avoid generating programs that do not “make sense”
from a semantic perspective.

Proving unrealizability. However, even with LLM guidance, the search procedure
may end up constructing partial programs that have no valid completion with
respect to the demonstrations. Our approach tries to avoid such dead-ends in
the search space through a novel procedure for proving unrealizability. In
particular, given a partial program $P$, our approach performs _static
analysis_ to construct a suitable abstraction, in the form of a regex, that
represents _all_ possible traces of _all_ completions of $P$ for the
demonstration environment. Given such a regex $r$, proving unrealizability of
a synthesis problem boils down to proving that the demonstration trace cannot
possibly belong to the language of $r$.

We have implemented the proposed LfD technique in a tool called
prolex111Programming RObots with Language models and regular EXpressions and
evaluate it on a benchmark set containing 120 long-horizon robotics tasks
involving household activities. Given a 2 minute time limit, our approach can
complete 80% of the synthesis tasks and can handle tasks that require multiple
loops with several conditionals as well as environments with up to _thousands_
of objects and dozens of object types. Furthermore, for 81% learning tasks
that prolex is able to complete within the 2 minute time limit, prolex learns
a program that matches the ground truth from just a _single_ demonstration. To
put these results in context, we compare our approach against two relevant
baselines, including CVC5, a state-of-the-art SyGuS solver and GPT-Synth, a
neural program synthesizer, and experimentally demonstrate the advantages of
our approach over other alternatives. CVC5 is only able to solve 25% of the
tasks even when given the ground-truth sketch. GPT-Synth, on the other hand,
is unable to solve any of the tasks due to environment complexity, even when
the environment is simplified to include only a small fraction of the objects
in addition to the required ground truth entities. Furthermore, we report the
results of a series of ablation studies and show that our proposed ideas
contribute to successful synthesis.

In summary, this paper makes the following contributions:

  * •

We propose a novel programming-by-demonstration (PBD) technique targeting
long-horizon robot tasks. Our approach can learn programs with complex control
flow structures, including nested loops with conditionals, from a small number
of traces and in complex environments with thousands of objects.

  * •

We propose a new (reusable) method for proving unrealizability of synthesis
problems in the PBD setting.

  * •

We implement these ideas in a tool called prolex and evaluate its efficacy in
the context of 120 benchmarks involving 40 unique household chores in three
environments. prolex can complete the synthesis task within 2 minutes for 80%
of the benchmarks, and, for 81% of the completed tasks, prolex is able to
learn the ground truth program from just a _single_ demonstration.

##  2\. Motivating Example

(a) Trace of demonstrated actions (left) and the abstracted string using
function $\alpha$ (right)

(b) Regexes learned from the string abstracted from the demonstration. The
correct regex (bottom) is highlighted to show looping and conditional
structures.

(c) Inferred Sketch

(d) Synthesized Program

Figure 2. Motivating Example

In this section, we present a motivating example to illustrate our
programmatic LfD approach. Imagine a hotel worker who wants to instruct a
robot to collect dirty sheets from guest rooms and place them in a laundry bin
in the room. The goal of LfD is to teach this task through demonstrations
rather than explicitly programming the robot. We formalize user demonstrations
in a form that is amenable to be captured using smart hand-held devices,
similar to existing end-user robots like the iRobot Roomba (iRobot, 2023) and
Amazon Astro (Lee et al., 2023).

Loc | State
---|---
$r_{1}$ | ${Objs}$ | $bed\\!:\\![b_{1}],\;sheet\\!:\\![s_{1},s_{2}],\;bin\\!:\\![bn_{1}],\dots$
${Props}$ | $(s_{1},dirty),(bn_{1},closed),\;\dots$
${Rels}$ | $(s_{1},on\text{-}top\text{-}of,b_{1}),\;(s_{2},on\text{-}top\text{-}of,b_{1}),\;\dots$
$r_{2}$ | ${Objs}$ | $bed\\!:\\![b_{2}],\;sheet\\!:\\![s_{3},s_{4}],\;bin\\!:\\![bn_{2}],\dots$
${Props}$ | $(s_{3},dirty),(s_{4},dirty),(bn_{2},closed),\;\dots$
${Rels}$ | $(s_{3},on\text{-}top\text{-}of,b_{2}),\;(s_{4},on\text{-}top\text{-}of,b_{2}),\;\dots$
Figure 3. Partial representation of the initial environment.

_User Demonstration._ For the above task, suppose that the hotel worker
performs a demonstration consisting of the 12 actions shown in the left side
of Figure 2(a). The demonstration takes place in two rooms, $r_{1}$ and
$r_{2}$; Figure 3 shows the state of these two rooms before the demonstration
takes place. Each room contains a large number of objects, including a bed, a
laundry bin, and a few sheets on the bed. In particular, there is a clean
sheet ($s_{2}$) and a dirty sheet ($s_{1}$) on the bed in $r_{1}$, and there
are two dirty sheets ($s_{3}$ and $s_{4}$) on the bed in $r_{2}$. Note that
the complete representation of the rooms includes many more object types and
properties, which are omitted from the figure due to space constraints. The
first five steps of the demonstration sequence shown in Figure 2(a) (left)
correspond to the actions performed in $r_{1}$, and the remaining seven steps
indicate the actions performed in $r_{2}$. Specifically,
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto(l)}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
indicates going to the location $l$, and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,\overline{o})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
indicates performing a specific action $a$ on objects $\overline{o}$. Hence,
in our example demonstration, the user first visits room $r_{1}$, where they
open bin
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{bn_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
grab and place sheet
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
in that bin, and finally close the bin. Next, they go to the second room,
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{r_{2}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and repeat a similar sequence of actions with the bin
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{bn_{2}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and sheets
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{3}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{4}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$.

_Desired Output._ Since our goal is to perform _programmatic_ LfD, we wish to
learn a programmatic _robot execution policy_ from the provided demonstration.
Figure 2(d) shows the desired policy that generalizes from the user’s only
demonstration. Intuitively, this policy encodes that the robot should go to
each room (line 2), identify a bin and all beds present in that room, collect
all _dirty_ sheets from the top of each bed (lines 7-8), and place them in the
bin (line 9). The program also contains _perception_ primitives that enable
the robot to become aware of its environment (lines 1, 3, 5, and 6). In
particular, the function
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau)$
allows the robot to identify all objects of type $\tau$ that are visible from
its current location and reason about their properties and relations. Function
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau)$
is similar but returns all locations of type $\tau$. Synthesis of appropriate
perception primitives is crucial for effective LfD, since the robot must be
able to observe and reason about the state of objects in new and unseen
environments.

_Synthesis Challenges._ In this context, generating the desired policy from
the user’s demonstration is challenging for several reasons: (1) the desired
program has complex control flow, with three nested loops and an if statement
with multiple predicates, (2) the desired program requires performing
appropriate perception actions that have no correspondence in the given
demonstrations, and (3) the desired program requires reasoning about high-
level concepts that are also not indicated in the demonstrations, such as
being dirty or being on top of some other object. Additionally, observe that
the synthesized program needs to refer to object types (e.g., bed) that are
not involved in the demonstration. Hence, the synthesizer cannot _only_
consider those objects in the demonstration, as the desired program could
refer to any of the entities in the environment. This means that the
difficulty of the synthesis task is inherently sensitive to the complexity of
the environment.

_Our Approach._ Our algorithm first generates a set of _sketches_ of the
target program based on the demonstration. These sketches capture the control
flow structure of the target program but contain many missing expressions
(“holes”). The goal of the subsequent sketch completion step is to fill these
holes in a way that scales to complex environments.

_Sketch generation._ To generate a sketch, our method first abstracts the
user’s demonstrations as a set of strings: Figure 2(a) (right) shows the
string abstracted from the user’s sole demonstration using an abstraction
function $\alpha$, where $\mathcal{G}$ and $\mathcal{A}$ denote
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
in the demonstration, and the subscripts indicate the _type_ of their
arguments. For example, even though the demonstration specifies that the user
grabbed specific sheets (namely,
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{3}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{s_{4}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$),
the string abstraction omits such details and represents all three instances
of this action using $\mathcal{A}_{grab,sheet}$. Each character in the
abstract string is highlighted using a different color to visually aid the
reader. The idea of converting the demonstration to a more abstract form is a
crucial first step towards generalization.

Next, our approach utilizes existing techniques to synthesize a regex that
matches the string encoding of the demonstrations: Figure 2(b) presents three
regular expressions that all match the string abstraction of the given
demonstration. Note that there is an obvious parallel between regex operators
and the program’s control flow: Since Kleene star denotes repetition, it
naturally corresponds to a looping construct. Similarly, since the optional
operator (i.e., $(r)?$) denotes choice, it is naturally translated into an
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
statement. Thus, given a candidate regex $r$ for the demonstrations, our
approach translates it into a sketch in a syntax-directed way. For instance,
the third regular expression from Figure 2(b) is translated to the sketch
shown in Figure 2(c), where the three nested loops and the conditional block
are marked using the same colored dashed lines both in the regex and in the
sketch. Additionally, because the program should not manipulate any objects
before it perceives them, our sketch generation procedure also inserts any
necessary perception primitives to the sketch. For instance, the sketch in
Figure 2(c) contains an inferred let binding (labelled $\mathsf{P1}$), since
the object of type $bin$ at line 4 cannot be acted upon before it is first
perceived by the robot.

_Sketch completion._ For each sketch generated in the first step, our method
tries to find a completion that matches the user’s demonstration. In practice,
several of these sketches are unrealizable, meaning that there is no
completion that will match the user’s demonstrations. For example, consider
the first regex presented above in Figure 2(b) that matches the string
abstraction of the demonstration. This regex does not include the optional
operator $?$ used in the correct regex. Intuitively, sketches generated from
this regex will be infeasible because, without an if statement in the sketch,
the resulting programs would end up grabbing _both_ sheets in room $r_{1}$,
rather than only the single dirty sheet. Hence, the second phase of our
technique considers multiple sketches and tries to find a completion of _any_
sketch that is consistent with the given demonstrations.

Our sketch completion algorithm is based on top-down enumerative search but
(a) utilizes a novel unrealizability checking procedure to quickly detect
dead-ends and (b) leverages an LLM to guide exploration. In particular,
starting from a sketch, the synthesis algorithm maintains a worklist of
partial programs containing holes to be filled. When dequeuing a partial
program from the worklist, we consider its probability according to the LLM,
so more promising partial programs are prioritized over less likely ones.
Going back to our example, consider a partial program where we test the color
of a bedsheet before putting it in the bin. Because the concepts “laundry bin”
and “cleanliness” are much more related compared to “color” and “laundry bin”,
our technique prioritizes a program that includes the conditional
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(dirty,...)$
over one that is based on color.

Figure 4. An Unrealizable Partial Program

Our sketch completion method also leverages the demonstration to prove
unrealizability of a given synthesis problem. As an example, consider the
partial program shown in Figure 4. We can prove that there is no completion of
this partial program that will be consistent with the user’s demonstrations:
Because none of the actions in the partial program modify object locations and
because there are two sheets in each room, any completion of this partial
program would end up performing the
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{grab}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
action _at least four times_ but there are only three
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{grab}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
actions in the trace. Hence, this partial program is a dead end, and our
approach can detect unrealizability of such a synthesis sub-problem. To do so,
it statically analyzes the partial program to infer upper and lower bounds on
the number of loop executions. It then uses this information to construct a
regex, shown at the bottom of Figure 4, that summarizes all possible traces
that this partial program can generate. Since the demo trace from Figure 2(a)
is not accepted by the regular expression in Figure 4, our algorithm can prove
the unrealizability of this synthesis problem.

τ_l∈Location Type^*:={bedroom, kitchen, basement, mail room, …}τ_o∈Object
Type^*:={ plate, drawer, dishwasher, sink, …}p∈Property^*:={ empty, broken,
green, dry, …}r∈Relation^*:={ inside-of, next-to, on-top-of, belongs-to,
…}a∈Action^*:={grab, open, pour-into, scrub-with, put-in, …}ρ∈Item
List:=scanObj (τ_o) ∣ scanLoc (τ_l)ϕ∈Conditional:=checkProp (p,v) ∣ checkRel
(r,v_1, v_2) ∣ ϕ_1 ∧ϕ_2 ∣ ϕ_1 ∨ϕ_2 ∣ ¬ϕπ∈Program:=actUnary (a,v) ∣ actBinary
(a,v_1,v_2) ∣ goto (v) ∣ if (ϕ) {π} ∣ skip ∣foreach (v ∈ρ) {π} ∣ let v:=getNth
(ρ,n) ∣ π;π

Figure 5. DSL syntax where $v$ denotes variables and $n$ is a natural number.
Rules marked with ∗ domain-specific.

##  3\. Robot Execution Policies

In this section, we introduce a domain-specific language (DSL) for programming
robots and provide a formal definition of the robot learning from
demonstrations (LfD) problem.

###  3.1. Syntax

The syntax of the our DSL is presented in Figure 5. A robot program ($\pi$)
contains functions to perform various operations on a single object
($\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$)
or a pair of objects
($\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$).
The robot can move between locations using the
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
function. The robot becomes aware of its location by scanning the environment
using
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and it becomes aware of objects in its current location using the
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
function. The result of running a scan operation is an ordered list of
location or object instances (denoted by $\rho$) of the specified type $\tau$.
For example,
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(plate)$
yields all plates at the current location of the robots. Specific elements in
the scan result can be bound to variables using a restricted let binding of
the form ${\tt let}\
v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\rho,n)$.
This expression introduces a new variable $v$ and assigns the $n$’th element
of list $\rho$ to $v$. As standard, the DSL also contains typical conditional
and looping control structures. Conditional expressions check properties of
objects
($\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$),
relationships between them
($\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkRel}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$),
as well as their Boolean compositions. The abstractions for robot actions and
perception in our DSL is similar to widely used accepted symbolic abstractions
for classical planning (Aeronautiques et al., 1998; Fox and Long, 2003), and
more recently, symbolic robot policies (Liang et al., 2022).

Note that the DSL presented in Figure 5 is parametrized over a set of domain-
specific terminals, indicated by an asterisk. For example, location types
$\tau_{l}$ are not fixed and can vary based on the target application domain.
For example, for robot execution policies targeting household chores,
locations might be kitchen, living room, basement etc. Similarly, object
types, properties, relations, and actions are also domain-specific and can be
customized for a given family of tasks.

###  3.2. Operational Semantics

In this section, we present the operational semantics of our robot DSL using
the small-step reduction relation $\Rightarrow$ shown in Figure 6. This
relation formalizes how the robot interacts with its environment while
executing the program. Specifically, the relation $\Rightarrow$ is defined
between tuples of the form $(\pi,\mathcal{E},\sigma,t)$, where $\pi$ is a
program, $\mathcal{E}$ is the robot’s execution environment, $\sigma$ is a
valuation (mapping variables to their values), and $t$ is a program trace. In
more detail, the environment $\mathcal{E}$ is a quadruple
$(\mathcal{L},\mathcal{O},\ell,\mathcal{I})$ where $\mathcal{L}$ is a set of
typed location identifiers; $\mathcal{O}$ is a mapping from (typed) object
identifiers to their corresponding location; $\ell$ is the current location of
the robot; and $\mathcal{I}$ is an interpretation for all the relation
symbols. That is, for a relation $p$, $\mathcal{I}(p)$ yields the set of
tuples of objects for which $p$ evaluates to true. Given object type
$\tau_{o}$ and a location $l$, we write $\mathcal{E}.{\tt objs}(l,\tau_{o})$
to denote the list of all objects that are at location $l$ and that have type
$\tau_{o}$. Similarly, given a location type $\tau_{l}$, the list of locations
of this type is denoted by $\mathcal{E}.\mathtt{locs}(\tau_{l})$. Finally, a
trace is a sequence of actions performed by the robot. Robot actions are
denoted using
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,\bar{o})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto(l)}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
where $a$ is an action that was performed on objects $\bar{o}$, and $l$ is a
location that the robot visited. Note that robot execution policies are
effectful programs: for example, the location of the robot or some properties
of an object can change after executing $\pi$.

(sequence)

$\footnotesize\frac{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\pi^{\prime},\mathcal{E}^{\prime},\sigma^{\prime},t^{\prime}\end{array}}{\begin{array}[]{c}\pi;\pi^{\prime\prime},\mathcal{E},\sigma,t\Rightarrow\pi^{\prime};\pi^{\prime\prime},\mathcal{E}^{\prime},\sigma^{\prime},t^{\prime}\end{array}}$

(skip)

$\footnotesize\frac{\begin{array}[]{c}\\\
\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0};\pi,\mathcal{E},\sigma,t\Rightarrow\pi,\mathcal{E},\sigma,t\end{array}}$

(if-t)

$\footnotesize\frac{\begin{array}[]{c}\phi\Downarrow_{\mathcal{E},\sigma}\top\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\phi)\\{\pi\\},\mathcal{E},\sigma,t\Rightarrow\pi,\mathcal{E},\sigma,t\end{array}}$

(if-f)

$\footnotesize\frac{\begin{array}[]{c}\phi\Downarrow_{\mathcal{E},\sigma}\bot\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\phi)\\{\pi\\},\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E},\sigma,t\end{array}}$

(act-unary)

$\footnotesize\frac{\begin{array}[]{c}\pi=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,v)\\\
{o}=\sigma(v)\qquad\mathcal{E}\xrightarrow{a,{o}}\mathcal{E}^{\prime}\\\
t^{\prime}=\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,{o})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\end{array}}{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}^{\prime},\sigma,t;t^{\prime}\end{array}}$

(act-binary)

$\footnotesize\frac{\begin{array}[]{c}\pi=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,v_{1},v_{2})\\\
{o}_{1}=\sigma(v_{1})\qquad{o}_{2}=\sigma(v_{2})\\\
\mathcal{E}\xrightarrow{a,{o}_{1},{o}_{2}}\mathcal{E}^{\prime}\qquad
t^{\prime}=\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,{o}_{1},{o}_{2})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\end{array}}{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}^{\prime},\sigma,t;t^{\prime}\end{array}}$

(goto)

$\footnotesize\frac{\begin{array}[]{c}\pi=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v)\\\
{l}=\sigma(v)\qquad\mathcal{E}^{\prime}=\mathcal{E}[\ell\mapsto{l}]\\\
t^{\prime}=\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto({l})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\end{array}}{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}^{\prime},\sigma,t;t^{\prime}\end{array}}$

(let-obj)

$\footnotesize\frac{\begin{array}[]{c}\pi=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o}),n)\\\
\sigma^{\prime}=\sigma[v\mapsto\mathcal{E}.\mathtt{objs}(\ell,\tau_{o})[n]]\end{array}}{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E},\sigma^{\prime},t\end{array}}$

(foreach-obj)

$\footnotesize\frac{\begin{array}[]{c}n=|\mathcal{E}.\mathtt{objs}(\ell,\tau_{o})|\qquad\forall_{0\leq
i<n}.\;\sigma_{i}=\sigma[v\mapsto\mathcal{E}.\mathtt{objs}(\ell,\tau_{o})[i]]\\\
\mathcal{E}_{0}=\mathcal{E}\qquad t_{0}=t\qquad\forall_{0\leq
i<n}.\;\pi,\mathcal{E}_{i},\sigma_{i},t_{i}\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}_{i+1},\\_\,,t_{i+1}\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o}))\\{\pi\\},\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}_{n},\sigma,t_{n}\end{array}}$

(let-loc)

$\footnotesize\frac{\begin{array}[]{c}\pi=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{l}),n)\\\
\sigma^{\prime}=\sigma[v\mapsto\mathcal{E}.\mathtt{locs}(\tau_{l})[n]]\end{array}}{\begin{array}[]{c}\pi,\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E},\sigma^{\prime},t\end{array}}$

(foreach-loc)

$\footnotesize\frac{\begin{array}[]{c}n=|\mathcal{E}.\mathtt{locs}(\tau_{l})|\qquad\forall_{0\leq
i<n}.\;\sigma_{i}=\sigma[v\mapsto\mathcal{E}.\mathtt{locs}(\tau_{l})[i]]\\\
\mathcal{E}_{0}=\mathcal{E}\qquad t_{0}=t\qquad\forall_{0\leq
i<n}.\;\pi,\mathcal{E}_{i},\sigma_{i},t_{i}\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}_{i+1},\\_\,,t_{i+1}\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{l}))\\{\pi\\},\mathcal{E},\sigma,t\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\mathcal{E}_{n},\sigma,t_{n}\end{array}}$

Figure 6. Operational semantics. Relation $\Downarrow$ is defined in Figure 7,
and the definition of relation $\rightarrow$ can be found in Appendix A.1.

With the above notations in place, we now explain the operational semantics
from Figure 6 in more detail. The first rule, labeled (sequence), defines how
the robot takes a step by executing the first statement in the program. The
next rule (skip) defines the semantics of executing a
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
statement, which has no effect on the execution state. The rules (if-t) and
(if-f) describe the flow of the program when a conditional statement
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\phi)\\{\pi\\}$
is executed. First, the Boolean expression $\phi$ is evaluated to $\bot$ or
$\top$, depending on the result, the program either skips or executes $\pi$.
Boolean expressions are evaluated using the relation $\Downarrow$ defined in
Figure 7. This relation is parameterized by the execution environment
$\mathcal{E}$ and valuation $\sigma$.

(check_prop_t)

$\footnotesize\frac{\begin{array}[]{c}\textbf{o}\in\mathcal{I}(p)\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(p,v)\Downarrow_{\mathcal{E},\sigma}\top\end{array}}$

(check_prop_f)

$\footnotesize\frac{\begin{array}[]{c}\sigma(v)\not\in\mathcal{I}(p)\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(p,v)\Downarrow_{\mathcal{E},\sigma}\bot\end{array}}$

(check_rel_t)

$\footnotesize\frac{\begin{array}[]{c}(\sigma(v_{1}),\sigma(v_{2}))\in\mathcal{I}(r)\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkRel}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r,v_{1},v_{2})\Downarrow_{\mathcal{E},\sigma}\top\end{array}}$

(check_rel_f)

$\footnotesize\frac{\begin{array}[]{c}(\sigma(v_{1}),\sigma(v_{2}))\not\in\mathcal{I}(r)\end{array}}{\begin{array}[]{c}\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkRel}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r,v_{1},v_{2})\Downarrow_{\mathcal{E},\sigma}\bot\end{array}}$

(negation)

$\footnotesize\frac{\begin{array}[]{c}\phi\Downarrow_{\mathcal{E},\sigma}b\end{array}}{\begin{array}[]{c}\neg\phi\Downarrow_{\mathcal{E},\sigma}\neg
b\end{array}}$

(conjunction)

$\footnotesize\frac{\begin{array}[]{c}\phi_{1}\Downarrow_{\mathcal{E},\sigma}b_{1}\qquad\phi_{2}\Downarrow_{\mathcal{E},\sigma}b_{2}\end{array}}{\begin{array}[]{c}\phi_{1}\wedge\phi_{2}\Downarrow_{\mathcal{E},\sigma}b_{1}\wedge
b_{2}\end{array}}$

(disjunction)

$\footnotesize\frac{\begin{array}[]{c}\phi_{1}\Downarrow_{\mathcal{E},\sigma}b_{1}\qquad\phi_{2}\Downarrow_{\mathcal{E},\sigma}b_{2}\end{array}}{\begin{array}[]{c}\phi_{1}\vee\phi_{2}\Downarrow_{\mathcal{E},\sigma}b_{1}\vee
b_{2}\end{array}}$

Figure 7. Boolean expression evaluation.

The (act-unary) and (act-binary) rules specify the outcomes of executing a
unary and a binary action, respectively, using the auxiliary relation
$\rightarrow\,\subseteq\mathcal{E}\times\mathcal{E}$. Given an environment
$\mathcal{E}$, an action $a$ and affected object instance(s), the relation
$\rightarrow$ formalizes how the environment $\mathcal{E}$ is modified based
on the semantics of action $a$. Since our DSL is parameterized over the set of
actions, we do not discuss the $\rightarrow$ relation in detail in the main
body of the paper and refer the interested reader to Appendix A.1 for a
representative subset of actions used in our evaluation.

The goto rule defines the effect of executing a
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v)$
statement, where the environment is updated to reflect the robot’s new
location, and a new trace element
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto({l})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
is generated and appended to the existing trace, where $l$ is the location
stored in variable $v$. Next, the rules let-obj and let-loc, define the
semantics of the
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\rho,n)$
statement, which assigns to variable $v$ the $n^{th}$ element of list $\rho$
obtained via either
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
or
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$.
Specifically,
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o})$
yields all objects of type $\tau_{o}$ that are present at the robot’s current
location, and
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{l})$
yields all locations of type $\tau_{l}$. The rules (foreach-obj) and (foreach-
loc) describe the semantics of loops of the form
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\rho)\\{\pi\\}$,
where $\rho$ is the result of a scan operation. As expected, these rules
iteratively bind $v$ to each of the elements in $\rho$ and execute the loop
body $\pi$ under this new valuation.

Finally, we use the $\Rightarrow$ relation to define the semantics of
executing a policy $\pi$ on environment $\mathcal{E}$. Given $\mathcal{E}$ and
robot execution policy $\pi$, we write $\pi(\mathcal{E})=t$ iff
$\pi,\mathcal{E},\mathsf{Nil},\mathsf{Nil}\Rightarrow\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{skip}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\\_,\\_,t$
where $\mathsf{Nil}$ denotes an empty list/mapping.

###  3.3. Problem Statement

In this section, we formally define the LfD problem that we address in this
paper. Informally, given a set of demonstrations $\mathcal{D}$, the LfD
problem is to find a robot execution policy $\pi^{*}$ (in the DSL of Figure 5)
such that $\pi$ is consistent with $\mathcal{D}$. To make the notion of
consistency more precise, we represent a demonstration $\delta$ as a pair
$(\mathcal{E},t)$ where $\mathcal{E}$ is the initial environment and $t$ is a
trace of the user’s demonstration in this environment.

###### Definition 3.1.

(Consistency with demonstration) We say that a robot execution policy
$\pi^{*}$ is consistent with a demonstration $\delta=(\mathcal{E},t)$, denoted
$\pi\models\delta$, iff $\pi(\mathcal{E})=t$.

We also extend this notion of consistency to a set of demonstrations
$\mathcal{D}$, and we write $\pi\models\mathcal{D}$ iff $\pi\models\delta$ for
every demonstration $\delta$ in $\mathcal{D}$. We can now formalize our
problem statement as follows:

###### Definition 3.2.

(Programmatic LfD) Given a set of demonstrations $\mathcal{D}$, the
_programmatic LfD_ problem is to find a robot execution policy $\pi^{*}$ such
that $\pi^{*}\models\mathcal{D}$.

##  4\. Synthesis Algorithm

In this section, we present our synthesis technique for solving the
programmatic LfD problem defined in the previous section. We start by giving
an overview of the top-level algorithm and then describe each of its key
components in more detail.

Input: _A set of demonstrations $\mathcal{D}$, a statistical completion model
$\theta$ _

Output: _A policy consistent with the demonstrations or $\bot$ if none exists_

1: $\mathsf{Synthesize}(\mathcal{D},\theta)$

2: $A:=\\{\alpha(t)\,\mid\,(\\_\,,t)\in\mathcal{D}\\}$ # get the abstraction
of given traces using function $\alpha$

3: while ($true$) {

4: $r:=\mathsf{GetNextRegex}(A)$ # get a regular expression that matches the
abstractions of all demos

5: if$(r=\bot)\ \ \mathbf{break}$

6: while ($true$) {

7: $s:=\mathsf{GetNextSketch}(r)$ # get the next lazily generated sketch from
$r$

8: if$(s=\bot)\ \ \mathbf{break}$

9: $\pi:=\mathsf{CompleteSketch}_{\theta}(s,\mathcal{D})$ # search for a
consistent completion of $s$ and return the result

10: if$(\pi\not\eq\bot)$ return $\pi$

11: }

12: $\\}$

13: return $\bot$

Algorithm 1 Top-level Synthesis Algorithm

###  4.1. Top-Level Algorithm

Our top-level learning procedure is presented in Algorithm 1. This algorithm
takes as input a set of demonstrations $\mathcal{D}$ and returns a policy
$\pi$ such that for all $\delta\in\mathcal{D}$, we have $\pi\models\delta$. If
there is no programmatic policy that is consistent with all demonstrations,
the algorithm returns $\bot$.

The synthesis procedure starts by constructing an _abstraction_ of each
demonstration $\delta\in\mathcal{D}$ as a string over the alphabet
$\Sigma=\\{\mathcal{G}_{\tau},\mathcal{A}_{a,\tau},\mathcal{A}_{a,\tau,\tau^{\prime}}\\}$
where $\tau,\tau^{\prime}$ indicate location and object types (e.g.,
${plate}$, ${kitchen}$) and $a$ denotes a specific type of action (e.g.,
${grab}$). This abstraction is performed at line 2 of Algorithm 1 using the
function $\alpha$, defined as follows:

$\begin{array}[]{lll}\alpha(\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{goto(l)}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}):={\mathcal{G}_{\tau_{l}}}&\alpha(\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,o)}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}):={\mathcal{A}_{a,\tau_{o}}}&\alpha(\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{act(a,o,o^{\prime})}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}):={\mathcal{A}_{a,\tau_{o},\tau_{o}^{\prime}}}\end{array}$

where $\tau_{l},\tau_{o}$ denote the type of location $l$ and object $o$
respectively. In other words, when abstracting a trace as a string, the
algorithm replaces specific object instances with their corresponding types.
Intuitively, this abstraction captures the commonality between different
actions in the trace, allowing generalization from a specific sequence of
actions to a more general program structure.

ρ_s∈Item List:=scanObj (??_τ_o) ∣ scanLoc (??_τ_l)s∈Sketch:=actUnary
(a,??_v:τ_o) ∣ actBinary (a,??_v:τ_o,??_v:τ’_o) ∣ goto (??_v) ∣ if (??_ϕ) {s}
∣foreach (v ∈ρ_s) {s} ∣ let v:=getNth (ρ_s,??_n) ∣ s;s

Figure 8. Syntax of Program Sketches. Domain specific definitions (i.e.,
$\tau_{o},\tau_{l},a$) are identical to Figure 5.

Next, given the string abstraction $A$ of the demonstrations $\mathcal{D}$,
the loop in lines 3–12 alternates between the following key steps:

  * •

Regex synthesis: The GetNextRegex procedure at line 4 finds a regular
expression $r$ matching all strings in $A$. Intuitively, this regex captures
the main control flow structure of the target program and can be used to
generate a set of program sketches.

  * •

Sketch generation: The inner loop in lines 6–10 translates a given regex to a
_set_ of program sketches. As shown in Figure 8, a sketch has almost the same
syntax as programs in our DSL except that the arguments of most constructs are
unknown, as indicated by question marks. In particular, note that (1) the
types of objects and locations being scanned are unknown, (2) predicates of
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
statements are yet to be determined, and (3) the specific objects and
locations being acted on are also unknown (although their _types_ are known).

  * •

Sketch completion: Given a candidate program sketch $s$, line 9 of the
algorithm invokes CompleteSketch to find a completion $\pi$ of $s$ that is
consistent with the demonstrations. If CompleteSketch does not return failure
($\bot$), the synthesized policy is guaranteed to satisfy all demonstrations;
hence, Synthesize returns $\pi$ as a solution at line 10.

In the remainder of this section, we describe sketch generation and sketch
completion in more detail. Because learning regexes from a set of positive
string examples is a well-understood problem, we do not describe it in this
paper, and our implementation uses an off-the-shelf tool customized to our
needs via some post-processing (see Section 5).

###  4.2. Sketch Inference

Given a regex $r$ over the alphabet
$\Sigma=\\{\mathcal{G}_{\tau_{l}},\mathcal{A}_{a,\tau_{o}},\mathcal{A}_{a,\tau_{o},\tau^{\prime}_{o}}\\}$,
the goal of sketch inference is to (lazily) generate a set of program
sketches. The inputs to the sketch inference procedure are regular expression
of the following form:

$\begin{array}[]{lcl}{r}&:=&{\mathcal{A}_{a,\tau_{o}}}\,\mid\,{\mathcal{A}_{a,\tau_{o},\tau_{o}^{\prime}}}\,\mid\,{\mathcal{G}_{\tau_{l}}}\,\mid\,{rr}\,\mid\,{(r)^{*}}\,\mid\,{(r)?}\end{array}$

Given such a regex, sketch inference consists of two steps:

  1. (1)

Syntax-directed translation: In the first step, sketch inference converts the
given regex to control flow operations using syntax-directed translation.
Intuitively, string concatenation is translated into to sequential
composition; Kleene star corresponds to loops; and, optional regexes translate
into conditionals.

  2. (2)

Perception inference: While the sketches generated in step (1) are
syntactically valid, they may lack essential perception operations (i.e.,
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
and
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$).
Hence, in the second step, our sketch inference procedure inserts these
perception operations such that the resulting sketch is _perception-complete_
, meaning that it contains at least the minimum number of required scan
operation. However, since the target program may require additional
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scan}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
operations, the second step of sketch inference yields a set of sketches that
only differ with respect to the placement of these perception operations.

$\footnotesize\frac{\begin{array}[]{c}\end{array}}{\begin{array}[]{c}{\mathcal{G}_{\tau_{l}}}\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{v}:\tau_{l})\end{array}}\qquad\footnotesize\frac{\begin{array}[]{c}\end{array}}{\begin{array}[]{c}{\mathcal{A}_{a,\tau_{o}}}\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,??_{v}:\tau_{o})\end{array}}\qquad\footnotesize\frac{\begin{array}[]{c}\end{array}}{\begin{array}[]{c}{\mathcal{A}_{a,\tau_{o},\tau^{\prime}_{o}}}\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,??_{v}:\tau_{o},??_{v}:\tau^{\prime}_{o})\end{array}}$

$\footnotesize\frac{\begin{array}[]{c}r\rhd
s\end{array}}{\begin{array}[]{c}(r)^{*}\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{\tau_{l}}))\\{s\\}\end{array}}\qquad\footnotesize\frac{\begin{array}[]{c}r\rhd
s\end{array}}{\begin{array}[]{c}(r)^{*}\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{\tau_{o}}))\\{s\\}\end{array}}\qquad\footnotesize\frac{\begin{array}[]{c}r_{1}\rhd
s_{1}\quad r_{2}\rhd s_{2}\end{array}}{\begin{array}[]{c}r_{1}r_{2}\rhd
s_{1};s_{2}\end{array}}$

$\footnotesize\frac{\begin{array}[]{c}r\rhd
s\end{array}}{\begin{array}[]{c}(r)?\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{\phi})\\{s\\}\end{array}}\qquad\frac{r\rhd
s}{r\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{\tau_{o}}),??_{n});s}\qquad\frac{r\rhd
s}{r\rhd\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{\tau_{l}}),??_{n});s}$

Figure 9. Regex to sketch inference rules.

Figure 9 presents our syntax-directed translation rules for converting regular
expressions to a syntactically valid sketch using judgments of the form
$r\triangleright s$, meaning that regex $r$ is translated to sketch $s$. As
expected, characters
$\mathcal{G}_{\tau},\mathcal{A}_{a,\tau},\mathcal{A}_{a,\tau,\tau^{\prime}}$
are translated to
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
constructs respectively. The Kleene star operator is translated into a looping
construct, but may iterate either over locations or objects. Finally, regex
concatanation is translated into sequential composition, and $(r)?$ is
translated into a conditional with an unknown predicate.

Recall that our DSL also allows
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings that assign a new variable to the result of a perception operation.
Since program traces (and, hence, the inferred regexes) do not contain these
perception operations, the last two rules in Figure 9 allow inserting
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings at arbitrary positions in the sketch. In particular, if $r$ can be
translated into a sketch $s$, then the last two rules of Figure 9 state that
$r$ can also be translated into a sketch of the form $l;s$ where $l$ is a new
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
binding which assigns a fresh variable $v$ to an entity that is obtained by
scanning objects or locations.

In general, observe that a regex can give rise to a large number of program
sketches, as we do not a priori know where to insert
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings. To tackle this problem, our lazy sketch inference procedure first
translates a regex into a sketch _without_ using the last two rules in Figure
9 for inserting
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings. In a second step, it infers where perception operations are needed
and inserts let bindings according to the results of this analysis.

This second step of our sketch inference procedure is formalized using the
notion of _perception completeness_. Intuitively, a sketch is _perception
complete_ if the program perceives (using
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scan}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
operations) all objects that it manipulates, before it manipulates them. If a
sketch is _not_ perception complete, it can never be realized into a valid
program; hence, it is wasteful to consider such sketches. We formalize the
notion of perception completeness using the following definition:

###### Definition 4.1.

(Perception Completeness) Let $\prec$ denote a standard partial order between
program points.222We refer the interested reader to the chapter 6 of
”Programming Language Pragmatics” by Michael L. Scott (2000) for a detailed
discussion on program orders and their usage in control flow analysis. A
sketch $s$ is said to be _perception complete_ if the following conditions are
satisfied:

  1. (1)

for all
$s_{1}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,??:\tau_{o})$
in $s$, there exists a
$s_{2}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o})$
such that $s_{2}\prec s_{1}$.

  2. (2)

for all
$s_{1}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a,??:\tau_{o},??:\tau^{\prime}_{o})$
in $s$, there exist
$s_{2}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o})$
and
$s_{3}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau^{\prime}_{o})$,
such that $s_{2}\prec s_{1}$ and $s_{3}\prec s_{1}$.

  3. (3)

for all
$s_{1}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??:\tau_{l})$
in $s$, there exists a statement
$s_{2}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{l})$
in $s$ such that $s_{2}\prec s_{1}$.

Our sketch inference algorithm leverages this notion of perception
completeness to lazily enumerate program sketches as follows: First, it
translates a given regex into a set of sketches using the inference rules
shown in Figure 9 but _without_ using the last two rules. It then infers a
minimal set of applications of the last two rules needed to make the sketch
perception complete and then augments the resulting sketches with the inferred
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings. Finally, because additional
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings may be needed, it lazily inserts more
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
bindings (up to a bound) if the current sketch does not produce a valid
completion.

###  4.3. Sketch Completion

Input: _A set of demonstrations $\mathcal{D}$, a sketch $s$_

Output: _A completion of $s$ consistent with $\mathcal{D}$ or $\bot$ if none
exists_

1: $\mathsf{CompleteSketch}_{\theta}(s,\mathcal{D})\\{$

2: $W:=[(s,{1.0})]$ # the given sketch $s$ is the only partial program
initially

3: while ($W\not\eq\emptyset$) {

4: $(\partial,p):=W.\mathsf{dequeue}()$ # get the partial program with the
highest probability

5: if $(\mathsf{IsComplete}(\partial))\\{$ # check if there is any holes left
to be filled

6: if $(\partial\models\mathcal{D})$ return $\partial$ # return the completed
program if it is consistent with the demos

7: else continue

8: if $\neg\mathsf{Compatible}(\partial,\mathcal{D})\;{\bf continue}$ # check
compatibility of the partial program and demos

9: $h:=\mathsf{GetNextHole}(\partial)$

10: foreach $(c\in\mathsf{Fill}(\partial,h,\mathcal{D}))\\{$

11: $\partial^{\prime}:=\partial[h\mapsto c]$; $p^{\prime}:=\theta(c\ |\
\partial,h,\mathcal{D})$ # fill the chosen hole and assign a probability to
the result

12: $W.\mathsf{enqueue}((\partial^{\prime},p^{\prime}))$ # add the new partial
program to the worklist

13: $\\}\\}\\}$

Algorithm 2 Sketch Completion Algorithm

We now turn our attention to the sketch completion procedure, shown in
Algorithm 2, for finding a sketch instantiation that satisfies the given
demonstrations. Given a sketch $s$ and demonstrations $\mathcal{D}$,
CompleteSketch either returns $\bot$ to indicate failure in finding a policy
$\pi$ that is consistent with all demonstrations. Note that the sketch
completion procedure is parameterized over a statistical model $\theta$ for
assigning probabilities to possible sketch completions.

CompleteSketch is a standard top-down search procedure that iteratively
expands partial programs until a solution is found.333Partial programs belong
to the grammar from Figure 5 augmented with productions $M\rightarrow??$ for
each non-terminal $M$. However, our sketch completion procedure has two novel
aspects: First, it assigns probabilities to partial programs using a large
language model, and second, it uses a novel _compatibility checking_ procedure
for proving unrealizability of synthesis problems.

In more detail, the sketch completion procedure initializes the worklist to a
singleton containing the input sketch $s$, with corresponding probability
$1.0$ (line 2). It then enters a loop (lines 3–14) where each iteration
processes the highest probability partial program $\partial$ in the worklist.
If the dequeued partial program $\partial$ is complete, meaning that it has no
holes (line 5), the algorithm checks whether all demonstrations are satisfied
(line 6). If so, $\partial$ is returned as a solution; otherwise, it is
discarded. If $\partial$ is incomplete, the algorithm performs a
_compatibility_ check at line 8 to avoid solving an unrealizable synthesis
problem. Next, if $\partial$ is a compatible with the demonstrations, the
algorithm considers one of the holes $h$ in $\partial$ and _all_ well-typed
grammar productions that can be used to fill that hole. In particular, given a
hole $?_{N}$, the procedure Fill yields a set of expressions
$c_{1},\ldots,c_{n}$ such that (1) $N\rightarrow c_{i}$ is a production in the
grammar, and (2) replacing $h$ with $c_{i}$ can result in a well-typed
program. Hence, for each such expression $c_{i}$, we obtain a new partial
program $\partial^{\prime}$ at line 11 by replacing hole $h$ in $\partial$
with expressions $c_{i}$.444When doing the replacement $\partial[h\mapsto c]$,
all non-terminals $N$ occurring in $c$ are replaced with a hole $?_{N}$.
However, since some completions are much more likely than others, our
algorithm assigns probabilities to completions using the statistical model
$\theta$. Hence, when dequeuing partial programs from the worklist, the
algorithm prioritizes programs that are assigned a higher probability.

####  4.3.1. Proving Unrealizability

Input: _A partial program $\partial$, a set of demonstrations $\mathcal{D}$_

Output: _True if the given partial program is compatible with $\mathcal{D}$
and otherwise false_

1: $\mathsf{Compatible}(\partial,\mathcal{D})$

2: foreach  $((\mathcal{E},t)\in\mathcal{D})\;$

3: $\partial^{*}:=\mathsf{PartialEval}(\partial,\mathcal{E})$ # Partially
evaluate the given partial program on the demonstration environment

4: $r:=\mathsf{ProgToRegex}(\partial^{*},\alpha(\mathcal{E}))$ # Find the
regex that over-approximates behaviors of $\partial^{*}$

5: if$(\alpha(t)\not\in r)\;$ return false # check if the trace is not
accepted by the over-approximating regex

6: return $true$

Algorithm 3 Checking compatibility between partial programs and demonstrations

A key component of our sketch completion procedure is a novel technique for
proving unrealizability of a programming-by-demonstration (PbD) problem. While
there has been significant prior work on proving unrealizability in the
context of programming-by-example (PbE) (Hu et al., 2019; Kim et al., 2023;
Feng et al., 2018a), such techniques only consider the input-output behavior
rather than the entire execution trace. In contrast, our goal is to prove
unrealizability of synthesis problems where the specification is a set of
demonstrations (i.e., traces).

Given a partial program $\partial$ (representing a hypothesis space), our key
idea is to generate a regex $r$ such that the language of $r$ includes all
possible traces of all programs in the hypothesis space. Hence, if there
exists some trace $t\in\mathcal{D}$ where $\alpha(t)$ is not accepted by $r$,
this constitutes a proof that the synthesis problem $(\partial,\mathcal{D})$
is unrealizable.

Our algorithm for checking compatibility between partial programs and traces
is presented in Algorithm 3. At a high level, this algorithm iterates over all
demonstrations (lines 2–5) and returns false if it can prove that $\partial$
is incompatible with some demonstration $(\mathcal{E},t)$ in $\mathcal{D}$. To
check compatibility with $(\mathcal{E},t)$, the algorithm first partially
evaluates $\partial$ on the initial environment $\mathcal{E}$ to obtain a
simplified program $\partial^{*}$, as done in existing work (Feng et al.,
2017). The novel part of our technique lies in constructing a regex
abstraction of the partial program $\partial$ under a given environment
$\mathcal{E}$. Specifically, our compatibility checking procedure constructs a
regex $r$ that over-approximates the possible behaviors of $\partial$ under
initial environment $\mathcal{E}$. In particular, the regex $r$ is constructed
at line 4 in such a way that if $\alpha(t)$ is not accepted by $r$, then no
completion of $\partial$ can be compatible with $(\mathcal{E},t)$ (see,
Theorem 4.2).

Hence, the crux of the compatibility checking algorithm is the ProgToRegex
procedure (formalized as inference rules shown in Figures 10 and 11) for
generating a regex that over-approximates the behavior of $\partial$ under
environment $\mathcal{E}$. These rules utilize the notion of an _abstract
environment_ which is a triple
$\hat{\mathcal{E}}:=(\mathsf{CurLoc},\mathsf{Locs},\mathsf{Objs})$ where (1)
CurLoc is a set containing all possible locations that the robot _could_
currently be at; (2) Locs is a mapping from location types to the set of
locations of that type; (3) Objs is a mapping from each location to the set of
objects of each type at that location (or $\top$ if unknown). Because
statements in our DSL can modify the environment, this notion of abstract
environment is used to conservatively capture (the possibly unknown) side
effects of partial programs on the environment. The inference rules shown in
Figures 10 and 11 formalize the ProgToRegex procedure using two types of
judgments:

  1. (1)

Scan rules (shown in Figure 10) are of the form
$\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scan}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(...):\Theta$,
indicating that the _cardinality_ of the set returned by
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scan}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
must be some element of $\Theta$. For example, if $\Theta=\\{1,4\\}$, this
means that the number of objects/locations returned by scan is either $1$ or
$4$. On the other hand, if $\Theta$ includes the special $\star$ element, then
the number of elements is unknown.

  2. (2)

Partial program rules (shown in Figure 11) are of the form
$\hat{\mathcal{E}}\vdash\pi:\hat{\mathcal{E}}^{\prime},r$, meaning that, under
initial abstract environment $\hat{\mathcal{E}}$, (a) the behavior of $\pi$ is
over-approximated by regex $r$, and (b) $\hat{\mathcal{E}}^{\prime}$ is a new
environment that captures all possible environment states after executing
$\pi$ on $\hat{\mathcal{E}}$.

Before we explain these rules in detail, we first describe the high level
idea, which is to encode (a) atomic actions using characters drawn from the
alphabet
$\\{\mathcal{G}_{\tau},\mathcal{A}_{a,\tau},\mathcal{A}_{a,\tau,\tau^{\prime}}\\}$,
(b)
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
statements using optional regexes, and (c) loops using regexes of the form
$r^{n}$ where $n$ denotes the number of times the loop will execute (or as
$r^{*}$ if the number of loop iterations is completely unknown). As mentioned
in earlier sections (and, as we demonstrate empirically in Section 6), static
reasoning about the number of loop iterations improves the effectiveness of
our unrealizability checking procedure. With this intuition in mind, we now
explain the rules shown in Figures 10 and 11.

##### Scan rules.

There are two sets of rules for scan operations, (loc-known) and (loc-unknown)
for scanning locations, and (obj-known) and (obj-unknown) for scanning
objects. For a
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
operation, if its argument is a known location type $\tau_{l}$, we simply look
up the number of locations of that type from the given abstract environment.
If it is unknown, we take the union over all possible location types. The
rules for
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
are similar: The (Obj-Known) rule handles the case where the argument is a
known object type $\tau_{o}$. In this case, we consider all the locations that
the robot could be currently at and take the union of the number of objects of
type $\tau_{o}$ for all of those locations. In the Obj-Unknown rule, we
additionally take the union over all possible object types, since the argument
of the
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
operation is unknown.

##### Atomic actions.

The rule labeled (atomic) in Figure 11 deals with
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
and
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
statements and serves two roles. First, it abstracts the performed action as a
letter in our regex alphabet using the abstraction function $\alpha$. Second,
it produces a new abstract environment $\hat{\mathcal{E}}^{\prime}$ by
considering all possible effects of the action on the input environment via
the UpdateAbsEnv function. Since the UpdateAbsEnv function is domain-specific
and depends on the types of actions of interest, we do not describe in detail
but provide a set of representative examples in Appendix A.4.

##### Sequence.

Sequential composition is abstracted using regex concatanation, and its final
effect on the environment is captured by threading the environment through the
two premises of the rule.

##### Conditionals.

As expected, if statements are abstracted using the optional operator
($(r)?$). Furthermore, since we do not know whether the predicate evaluates to
true or not555Recall that we apply partial evaluation before performing this
step. Hence, if the predicate of a conditional can be fully evaluated, it will
be simplified away and rewritten as conditional-free code., we take the _join_
of the two abstract environments. Intuitively, the join of abstract
environments $\hat{\mathcal{E}}$ and $\hat{\mathcal{E}}^{\prime}$, denoted by
$\hat{\mathcal{E}}\sqcup\hat{\mathcal{E}}^{\prime}$, is the smallest
environment that over-approximates both $\hat{\mathcal{E}}$ and
$\hat{\mathcal{E}}^{\prime}$. An abstract environment $\hat{\mathcal{E}}$ is
said to over-approximate an abstract environment $\hat{\mathcal{E}}^{\prime}$,
denoted by $\hat{\mathcal{E}}^{\prime}\sqsubseteq\hat{\mathcal{E}}$, if and
only if:

$\hat{\mathcal{E}}^{\prime}.\mathsf{Locs}\subseteq\hat{\mathcal{E}}.\mathsf{Locs}\wedge\forall_{l\in\hat{\mathcal{E}}^{\prime}.\mathsf{Locs}}\forall_{\tau\in\mathsf{ObjTypes}(\hat{\mathcal{E}}^{\prime})}.\;\hat{\mathcal{E}}^{\prime}.\mathsf{Objs}(l,\tau)\subseteq\hat{\mathcal{E}}.\mathsf{Objs}(l,\tau)$

Then, we can define a join operator on abstract environments as follows:

$\hat{\mathcal{E}}\sqcup\hat{\mathcal{E}}^{\prime}=\hat{\mathcal{E}}^{\prime\prime}\iff(\hat{\mathcal{E}}\sqsubseteq\hat{\mathcal{E}}^{\prime\prime})\wedge(\hat{\mathcal{E}}^{\prime}\sqsubseteq\hat{\mathcal{E}}^{\prime\prime})\wedge(\forall_{\hat{\mathcal{E}}^{\prime\prime\prime}}(\hat{\mathcal{E}}\sqsubseteq\hat{\mathcal{E}}^{\prime\prime\prime}\wedge\hat{\mathcal{E}}^{\prime}\sqsubseteq\hat{\mathcal{E}}^{\prime\prime\prime}\Rightarrow\hat{\mathcal{E}}^{\prime\prime}\sqsubseteq\hat{\mathcal{E}}^{\prime\prime\prime}))$

Intuitively, $\hat{\mathcal{E}}^{\prime\prime\prime}$ is the result of joining
$\hat{\mathcal{E}}$ and $\hat{\mathcal{E}}^{\prime}$ if it is the smallest
abstract environment that over-approximates both.

(loc-known)

$\footnotesize\frac{\begin{array}[]{c}\\\
\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{l}):\\{|\hat{\mathcal{E}}.\mathsf{Locs}(\tau_{l})|\\}\end{array}}$

(loc-unknown)

$\footnotesize\frac{\begin{array}[]{c}\mathsf{LocTypes}(\hat{\mathcal{E}})=\\{\tau_{1},\dots,\tau_{n}\\}\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??):\bigcup_{1\leq
i\leq n}\\{|\hat{\mathcal{E}}.\mathsf{Locs}(\tau_{i})|\\}\end{array}}$

(obj-known)

$\footnotesize\frac{\begin{array}[]{c}\hat{\mathcal{E}}.\mathsf{CurLocs}=\\{l_{1},\dots,l_{n}\\}\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\tau_{o}):\bigcup_{1\leq
i\leq n}\\{|\hat{\mathcal{E}}.\mathsf{Objs}(l_{i},\tau_{o})|\\}\end{array}}$

(obj-unknown)

$\footnotesize\frac{\begin{array}[]{c}\hat{\mathcal{E}}.\mathsf{CurLocs}=\\{l_{1},\dots,l_{n}\\}\qquad\mathsf{ObjTypes}(\hat{\mathcal{E}})=\\{\tau_{0},\dots,\tau_{k}\\}\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??):\bigcup_{1\leq
i\leq n}\bigcup_{1\leq j\leq
k}\\{|\mathcal{E}.\mathsf{Objs}(l_{i},\tau_{j})|\\}\end{array}}$

Figure 10. Over-approximation of robot perception used in ProgToRegex
function.

(atomic)

$\footnotesize\frac{\begin{array}[]{c}\mathsf{AtomicAction}(s)\qquad\hat{\mathcal{E}}^{\prime}=\mathsf{UpdateAbsEnv}(\hat{\mathcal{E}},s)\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash
s:\hat{\mathcal{E}}^{\prime},\alpha(s)\end{array}}$

(seq)

$\footnotesize\frac{\begin{array}[]{c}\hat{\mathcal{E}}\vdash
s_{1}:\hat{\mathcal{E}}_{1},r_{1}\qquad\hat{\mathcal{E}}_{1}\vdash
s_{2}:\hat{\mathcal{E}}_{2},r_{2}\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash
s_{1};s_{2}:\hat{\mathcal{E}}_{2},r_{1}r_{2}\end{array}}$

(if)

$\footnotesize\frac{\begin{array}[]{c}\hat{\mathcal{E}}\vdash
s:\hat{\mathcal{E}}^{\prime},r\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\\_)\,\\{s\\}:\hat{\mathcal{E}}\sqcup\hat{\mathcal{E}}^{\prime},(r)?\end{array}}$

(let)

$\footnotesize\frac{\begin{array}[]{c}\\\
\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v:=e:\hat{\mathcal{E}},\epsilon\end{array}}$

(loop)

$\footnotesize\frac{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\rho_{s}:\\{n_{1},\dots,n_{k}\\}\qquad\hat{\mathcal{E}}^{\prime}\vdash
s:\hat{\mathcal{E}}^{\prime},r\qquad\hat{\mathcal{E}}\sqsubseteq\hat{\mathcal{E}}^{\prime}\end{array}}{\begin{array}[]{c}\hat{\mathcal{E}}\vdash\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v\in\rho_{s})\\{s\\}:\hat{\mathcal{E}}^{\prime},r^{n_{1}}|r^{n_{2}}|\dots|r^{n_{k}}\end{array}}$

Figure 11.  Over-approximation of partial programs used in ProgToRegex
function.

##### Loops.

The last rule in Figure 11 summarizes the analysis of loops. First, since the
environment may be modified in the loop body, this rule first computes an
_inductive abstract environment_ , $\hat{\mathcal{E}}^{\prime}$, for the loop
(see Section 5 for further details). In particular, the premise
$\hat{\mathcal{E}}\sqsubseteq\hat{\mathcal{E}}^{\prime}$ ensures that
$\hat{\mathcal{E}}^{\prime}$ over-approximates the _initial_ environment,
thereby establishing our base case. Second, the premise
$\hat{\mathcal{E}}^{\prime}\vdash\pi:\hat{\mathcal{E}}^{\prime},r$ ensures
that $\hat{\mathcal{E}}^{\prime}$ is preserved in all iterations of the loop
body. Furthermore, because $\hat{\mathcal{E}}^{\prime}$ is an over-
approximation of the environment that the loop body $\pi$ operates in, the
regular expression $r$ also over-approximares the behavior of $\pi$. Finally,
to over-approximate the behavior of the entire loop, we determine the possible
number of loop executions using the rules from Figure 10 under the initial
environment $\hat{\mathcal{E}}$. If $\rho_{s}$ can yield $n$ different
objects, then the behavior of the loop is captured as $r^{n}$. However, since
we may not be able to compute the exact number of objects returned by a scan
operation, we consider all possible cardinalities $n_{1},\ldots,n_{k}$ of the
resulting set. Hence, the behavior of the loop is captured by the disjunction
of the regexes $r^{n_{1}},\ldots,r^{n_{k}}$.

The following theorem states that none of the completions of an unrealizable
partial program is consistent with all demonstrations (see Appendix A.5 for
the proof). An immediate corollary is the bounded completeness of our search
algorithm, i.e., that Algorithm 1 always finds a program consistent with the
demonstrations if it exists within the bounds of the search space.

###### Theorem 4.2.

Let $\partial$ be a partial program and let $\mathcal{D}$ be a set of
demonstrations. Then, for any complete program $P$ that is a completion of
$\partial$, we have:

$P\models\mathcal{D}\ \Longrightarrow\
\mathsf{Compatible}(\partial,\mathcal{D})$

####  4.3.2. Using LLM for Sketch Completion

We conclude this section with a discussion of how prolex infers a probability
distribution over partial programs by prompting a large language model. Our
prompting approach is inspired by the success of LLMs in addressing the “Fill
in the Middle (FIM)” challenges in NLP literature (Liu et al., 2023). We
reduce the sketch completion task to a FIM problem, as described below.

Given a partial program $\partial$ with a hole $h$ to fill, our approach
encodes the context of $h$ in $\partial$ as a natural language prompt with
unknown _masks_ (Devlin et al., 2019). The prompt includes the set of valid
completions for each mask, chosen by the $\mathsf{Fill}(.)$ procedure in
Algorithm 2, to ensure the resulting program is well-typed. The LLM is then
instructed to infer a probability distribution over the set of completions
(represented by $\theta$ in Algorithm 2). This procedure is repeated whenever
a partial program is expanded into a set of partial programs, to prioritize
the enumerative search towards the intended program.

To illustrate how prolex prompts the LLM, Figure 12(a) (top) shows a partial
program containing six unfilled holes, denoted as $??_{i}$. Figure 12(b) (top)
shows the prompt used for completing hole $??_{1}$, which essentially
corresponds to a natural description of the program.666Note that the
demonstration is implicitly encoded as part of the partial program using type
information for each hole. To generate such a prompt, our approach translates
control-flow constructs to natural language in a syntax-directed way and
replaces some of the holes ($??_{1}$ and $??_{2}$ in this example) with masks.
Because the remaining holes $??_{3}-??_{6}$ will be replaced with synthetic
variable names like $v_{1},v_{2}$, they are not meaningful to the LLM; so our
approach simply uses the types of these holes rather than masks when
translating the partial program to natural language. As we can see from the
LLM output in Figure 12(b), the highest likelihood completion of $??_{1}$ is
deemed to be _bed_ by the model, so the sketch completion algorithm
prioritizes this completion over other alternatives such as _chair_ or _mug_.

1:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{1}\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanLoc}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(room))\\{$
2:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{goto}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{1}:room)$;
3:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{let}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;v_{2}:=\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{getNth}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(bin),0)$;
4:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(open,v_{2}:bin);$
5:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{3}\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{1}))\\{$
6:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{4}\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(sheet))\\{$
7:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{2})\\{$
8:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(grab,??_{3}:sheet);$
9:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actBinary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(put\text{-}in,??_{4}:sheet,??_{5}:bin);$
10: $\\}$$\\}$$\\}$ 11:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{actUnary}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(close,??_{6}:bin);\\}$

4: … 5:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{3}\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(bed))\\{$
6:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(v_{4}\in\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scanObj}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(sheet))\\{$
7:
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{if}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{2a},v_{4})\wedge\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkRel}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{2b},v_{4},v_{3}))\\{$
…

(a) Partial programs $\partial$ (top) and $\partial^{\prime}$ (bottom)

Prompt for $??_{1}$: For each room; Go to room; Look for bins; Open a bin; For
each $[M]_{1}$ do; For each sheet do; If $[M]_{2}$, grab sheet and put sheet
in bin; Close bin.
LLM Output for $[M]_{1}$: {Bed: 0.8, Chair: 0.1, Mug: 0.05, …}

Prompt for $??_{2a}$: For each room; Go to room; Look for bins; Open a bin;
For each bed do; For each sheet do; If sheet is $[M]_{2a}$ and sheet is
$[M]_{2b}$ bed, grab sheet and put sheet in bin; Close bin.
LLM Output for $[M]_{2a}$: {Dirty: 0.75, Folded: 0.2, White: 0.02, …}

Prompt for $??_{2b}$: For each room; Go to room; Look for bins; Open a bin;
For each bed do; For each sheet do; If sheet is dirty and sheet is $[M]_{2b}$
bed, grab sheet and put sheet in bin. Close bin.
LLM Output for $[M]_{2b}$: {On-top-of: 0.9, Under: 0.05, …}

(b) LLM prompts for $??_{1}$, $??_{2a}$ and $??_{2b}$

Figure 12. Partial programs during synthesis and the generated LLM prompts to
choose the next completion

As another example, consider the process of filling hole $??_{2}$, and suppose
that the algorithm has already refined $??_{2}$ to the conjunct
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkProp}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{2a},v_{4})\wedge\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{checkRel}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(??_{2b},v_{4},v_{3})$
as shown in the bottom part of Figure 12(a). When generating the prompt for
$??_{2a}$, both holes $??_{2a}$ and $??_{2b}$ are filled with masks, and the
LLM outputs _dirty_ as the most likely completion for $??_{2a}$. When querying
the remaining hole ($??_{2b}$), $??_{2a}$ has already been filled with _dirty_
, so the prompt only contains a single mask, and the LLM outputs _on-top-of_
as the most likely completion. As illustrated by these examples, the LLM-
guided search strategy allows the sketch completion engine to quickly home in
on the right concepts (such as _bed_ , _dirty_ , and _on-top-of_ in this
example) and therefore allows the search procedure to focus on the most
promising sketch completions.

##  5\. Implementation

We implemented the proposed approach in a tool called prolex written in
Python. In this section, we discuss salient aspects of prolex that are not
covered in the technical sections.

_Regex Learner._ Our implementation leverages an open-source library to learn
regular expressions from positive samples (Nordmann, 2014). However, since our
sketch generation procedure does not allow arbitrary regex operators, our
implementation post-processes the synthesized regexes by applying a set of
rewrite rules. For instance, because our sketch generation procedure does not
allow arbitrary disjunction, one of the rewrite rules
($(x|y)\rightarrow(xy?)$) replaces disjunction with an optional operator. The
full list of our rewrite rules can be found in Appendix A.3.

_Large Language Model._ Our sketch completion module utilizes the BERT large
language model (Devlin et al., 2019), with pre-trained weights obtained from
the HuggingFace library (Wolf et al., 2020). Since our algorithm generates
masked language modeling (MLM) queries, we chose to use the bert-base-uncased
model. This model is primarily fine-tuned for tasks that make use of the whole
sentence, potentially with masked words, to make decisions. It is a
lightweight model, and in our experiments, it consistently returns responses
in less than $70\,ms$ on average.

_Parallel Sketch Completion._ The inherent independence of program sketches
naturally lends itself to parallelization of the search process. To take
advantage of this, prolex spawns a new process to execute sketch completion
(Algorithm 2) for each generated sketch.

_Computing Loop Invariants._ Recall that our procedure for proving
unrealizability relies on an _inductive abstract environment_ for translating
loops to regular expressions. Our implementation conservatively models the
effect of any statement with holes by assuming that the hole could be filled
with any value, and it performs standard least fixed point computation under
these conservative semantics.

##  6\. Evaluation

In this section, we present experiments designed to answer the following
research questions:

  1. (RQ1)

How effective is prolex at learning policies from human demonstrations?

  2. (RQ2)

What is the relative significance of each of the key components in our
synthesis algorithm?

  3. (RQ3)

How does prolex compare against relevant baselines in terms of learning
policies that match the user’s intention?

(a) Complexity of the Tasks

Env | # Obj. | # Obj. | # Props.
---|---|---|---
Types | Instances
Easy | 40 | 140 | 609
Medium | 60 | 295 | 2455
Hard | 80 | 1109 | 13944
(b) Complexity of the Environments

Figure 13. Overview of the Benchmark

###  6.1. Benchmarks and Experimental Set-up

_Tasks._ We evaluate prolex on a set of 40 programmatic LfD problems involving
long-horizon service tasks in typical household environments. We gathered
these tasks from two sources, which we describe below.

First, we use 25 tasks from the Behavior Project (Srivastava et al., 2022).
This project is an interactive platform designed for a virtual embodied AI
agent operating within simulated household environments. The Behavior Project
offers simulation videos of the agent carrying out a range of long-horizon
tasks. These demonstrations are produced by human users who use a joystick to
control the agent’s movements and actions in the simulation environment. Out
of 100 tasks provided in the Behavior project, we observed that 75 required
precise low-level motion control of the robot’s arms, like detailed cleaning
of a car’s surfaces. As our DSL can trivially execute these tasks without any
conditionals or loops, we excluded them from our evaluation. The demonstration
videos for the remaining 25 tasks were transcribed using our action alphabet
by an expert annotator —one of the authors— who is knowledgeable about the
skill abstractions used by the robot.777Note that, in principle, this step
could be performed by an off-the-shelf vision-to-action detection (V2A)
algorithm (Ashutosh et al., 2023; Nazarczuk and Mikolajczyk, 2020). However,
since this perception inference is orthogonal to our main problem, we opt to
directly use the expert annotations.

Next, to broaden the scope of our evaluation and include more realistic tasks,
we surveyed students at our institution and collected 15 additional tasks to
evaluate prolex on. We did not impose any requirements regarding the users’
technical expertise, as our aim was to gather a list of household tasks that a
typical end-user would consider beneficial to have automated

A full list of the above 40 tasks and their ground-truth programs is provided
in Appendix A.6. Figure 13(a) presents an overview of the ground-truth
programs for these tasks, ordered by program size. In more detail, the right
y-axis represents program size (measured in terms of the number of nodes in
the abstract syntax tree) and the left y-axis represents the number of loops,
conditionals and perception primitives in the program. Tasks from the Behavior
project are labeled as $\mathtt{B1}\dots\mathtt{B25}$, and surveyed tasks are
labeled as $\mathtt{S1}\dots\mathtt{S15}$.

Figure 14. Length of Demonstrations

_Environments._ All of our benchmarks are defined in three household
environments, summarized in Figure 13(b). Because the difficulty of the
synthesis task depends crucially on the number of object types and objects in
the environment, we classify the three environments as Easy, Medium, and Hard
based on these numbers. As we can see from Figure 13(b), these environments
contain up to thousands of objects and over ten thousand properties.

_Full benchmark set._ Overall, we evaluate prolex on a total of 120
benchmarks, with 40 unique tasks and 3 different environments. For each of the
40 tasks, we manually write the ground truth program in our DSL and obtain a
demonstration by running the ground truth program. Figure 14 presents
statistics regarding the length of these demonstrations. On average,
demonstrations in the easy, medium, and hard environments consist of 11, 13,
and 24 actions, respectively. Some demonstrations in the hard environment
exceed 100 actions due to the large number of object instances that need to be
handled.

_Experimental set-up._ Our experiments were conducted on a server with 64
available Intel Xeon Gold 5218 CPUs @2.30GHz, 264GB of available memory, and
running Ubuntu 22.04.2. We use a time limit of 120 seconds per task in all of
our experiments.

###  6.2. Main Results for Prolex

Our main results are presented in Figure 15, with Figure 15(a) showing the
percentage of completed tasks against synthesis time. We consider a task to be
_completed_ if prolex is able to synthesize a policy within the time limit,
and _solved_ if the learned program also matches the user’s intent. We
determine if a task is solved by comparing it against the ground truth program
(written manually) and checking if the learned program is semantically
equivalent. Since the manually written policy is intended to work in all
environments, tasks classified as “solved” generalize to unseen environments.

_Running time._ In Figure 15(a), the three lines indicate the percentage of
benchmarks (y-axis) completed with a given time limit (x-axis) for each of the
three environments (Easy, Medium, Hard). Across all environments, prolex is
able to complete 36% of the tasks within the first 5 seconds, 28% of the tasks
within 6-30 seconds, and 16% of the tasks within 31-120 seconds. Overall,
prolex is able to complete 80% of the tasks within the 2 minute time limit.

Figure 15 also provides a more detailed look at these statistics by showing
the percentage of completed tasks with respect to task complexity. In
particular, Figure 15(b) shows the rate of completion according to the size of
the ground truth program. As expected, the learning problem becomes harder as
the complexity of target policy increases. However, even for the most complex
programs, prolex is still able to complete the learning task for 68% of the
benchmarks.

(a) Success Rate per Environment

(b) Success by AST Size

(c) Generalizability

Figure 15. Experimental Results

_Generalizability._ As mentioned earlier, completing a task is not the same as
“solving” it, since the synthesized policy may not match user intent despite
being consistent with the demonstrations. We manually inspected all programs
synthesized by prolex and found that it is equivalent to the ground truth
program in 81% of the completed cases. Interestingly, as shown in Figure
15(c), we found that prolex’s generalization power improves as environment
complexity increases. Intuitively, the more complex the environment, the more
objects there are with different properties, so it becomes harder to find
multiple programs that “touch” exactly the same objects as the demonstration.

_Search Statistics._ As explained in Section 4, sketches in prolex are
enumerated based on increasing order of complexity. In each iteration, a
finite number of completions are considered for the current sketch. If none of
these completions aligns with the demonstrations, the algorithm advances to
the next sketch. This process continues until either a successful match is
found or the time limit is reached. Figure 16 presents the average number of
sketches encountered before finding the solution or timing out for each task
in all three environments. For almost all tasks, prolex considers fewer than
50 sketches before termination. One task ($\mathtt{S5}$) is exceptionally
challenging and requires 143 sketches before a solution is found.

Figure 16. Number of Sketches Considered

_Failure analysis._ As discussed above, there are two reasons why prolex may
fail to solve a task: (1) it fails to find a policy consistent with the
demonstrations within the time limit, or (2) the synthesized policy does not
adequately capture the user intent. We have manually inspected both classes of
failure cases and report on our findings.

The main cause of prolex’s timeouts is due to perception operations. Many of
our environments contain a large number of object types, all of which can be
arguments of
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{scan}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
operations. Our approach tries to overcome this issue by using an LLM to guide
search, but in some cases, the LLM proposes the wrong object type to scan for.
This causes the synthesizer to go down a rabbit hole, particularly in cases
when the proposed object type has many properties associated with it. We
believe more advanced LLMs that can reason about finer-grained properties
between the environment and the context of the task can potentially mitigate
this issue.

We also inspected the cases where prolex finds _a_ robot execution policy
consistent with the demonstrations, but the synthesized policy does not
generalize to different environments (i.e., it completes the task but fails to
solve it). There are two main reasons for this, both due to the inadequacy of
the demonstrations with respect to the desired task. Specifically, if there is
only one instance of a particular object type in the environment, the
synthesizer may not return a program with a
$\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{\mathtt{foreach}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
loop over that object type, even though the ground truth program contains such
a loop. Likewise, prolex is capable of inferring conditional blocks only if
the demonstrations are _branch complete_. This means that, in the
demonstration environment, some instances of a manipulated object type must
satisfy the intended property, while others must not. If all (or none) of the
object instances of that type are acted upon, the synthesizer cannot learn the
conditional block for such manipulations. As noted earlier, this
generalizability issue becomes less of a problem in more complex environments
with many instances of an object type.

RQ1 Summary.  Given a 2 minute time limit, prolex is able to find a policy
consistent with the demonstations for 80% of the benchmarks. Furthermore 81%
of the synthesized programs correspond to the ground truth, meaning that they
can generalize to any unseen environment.

###  6.3. Ablation Studies

As mentioned throughout the paper, there are three key components underlying
our approach, namely (1) learning control flow structures (i.e., sketches),
(2) use of LLMs to guide sketch completion, and (3) new technique for proving
unrealizability. To better understand the relative importance of each
component, we present the results of an ablation study where we disable each
component or combinations of components. Specifically, for our ablation study,
we consider the following variants of prolex:

  * •

prolex-NoSketch: This is a variant of prolex that does not generate program
sketches using regex learning.

  * •

prolex-NoLLM: This is a variant of prolex that does not utilize LLMs for
sketch completion.

  * •

prolex-NoPrune: This is a variant of prolex that does not utilize the
unrealizability checking procedure (Algorithm 2) for pruning the search space
during sketch completion.

  * •

prolex-SketchOnly: This is a variant of prolex that infers control flow
sketches (through regex learning) but neither utilizes LLM nor unrealizability
checking during sketch completion.

  * •

prolex-NoLoopBound: This is a variant of prolex summarizes loops using the
Kleene star operator during the unrealizability checking procedure. That is,
it does not reason about the number of loop iterations; however, it is the
same as the full prolex tool otherwise.

Figure 17(a) shows the results of our ablation study in the form of a
Cumulative Distribution Function (CDF). The x-axis represents the cumulative
running time, while the y-axis shows the percentage of benchmarks solved in
all environments. The results indicate a significant gap between the number of
the tasks solved by prolex and its variants defined above. In particular,
prolex is able to solve 8% more tasks than NoLLM, 19% more tasks than NoPrune,
24% more tasks than SketchOnly, and 8% more tasks than NoLoopBound variants.
However, the results for the NoSketch variant are particularly poor, with none
of the tasks solved.

(a) Ablation results over all environments.

(b) prolex vs. CVC5 in Easy environments. CVC5 is provided the ground truth
sketch but prolex is not

Figure 17. Experimental Results

RQ2 Summary.  All of the key components of our proposed synthesis algorithm
contribute to the practicality of our learning approach. The most important
component is regex-based sketch generation, without which none of the tasks
can be solved. The unrealizability checking procedure helps solve an
additional 18% of the tasks, and LLM guidance increases success rate by
another 8%.

###  6.4. Comparison with Alternative Approaches

In this section, we report on our experience comparing prolex against
alternative approaches. While there is no existing off-the-shelf LfD approach
that targets our problem domain (see Section 6.1), we compare prolex against
the following two baselines:

  * •

CVC5: We formulate our learning problem as an instance of syntax-guided
synthesis and use a leading SyGuS solver, CVC5 (Barbosa et al., 2022), as a
programmatic policy synthesizer.

  * •

GPT-Synth: We use an LLM as a _neural program synthesizer_ in our domain. To
this end, we consider a baseline called “GPT-Synth” that synthesizes programs
in our DSL from demonstrations.

##### Case Study with CVC5.

Our programmatic LfD task can be reduced to an instance of the syntax-guided
synthesis (SyGuS) problem (Alur et al., 2015a), which is the standard
formulation for synthesis problems. To compare prolex against state-of-the-art
SyGuS solvers, we encoded our tasks as instances of SyGuS and leveraged an
off-the-shelf solver, namely, CVC5 (Barbosa et al., 2022), which is the winner
of the most recent SyGuS competition.

To perform this comparison, we defined our DSL using the syntactic constraints
in SyGuS, and we incorporated semantic constraints based on the _initial and
final environment states_ in the demonstrations. Note that SyGuS solvers are
unable to perform synthesis from demonstrations, as demonstrations correspond
to intermediate program states, which are not expressible in the SyGuS
formulation. Hence, when comparing against CVC5, we only use the initial and
final environments and consider a task to be completed if the solver returns a
policy that produces the desired environment. Furthermore, we only compare the
performance of prolex and CVC5 on the “easy” environment as encoding the
environments in SyGuS requires significant manual labor.

When we tried to use CVC5 to perform synthesis from scratch (i.e., without a
sketch), it was not able to complete any task within a reasonable time limit.
Hence, for this evaluation, we manually provided CVC5 with the _ground truth_
sketch for the specific task. The results of this comparison are presented in
Figure 17(b). As in Figure 17(a), this figure plots the cumulative
distribution of the percentage of synthesized programs against solver time.
Overall, CVC5 only solves $25\%$ of the tasks, compared to $88\%$ solved by
prolex.

##### Case Study with GPT-Synth.

For this experiment, we use the GPT 3.5 LLM888We specifically use the text-
davinci-003 model, which is the most capable publicly available LLM from
OpenAI finetuned for completion, including natural language and code. to
generate programmatic policies from demonstrations. This study aims to
evaluate the effectiveness of LLMs as an end-to-end program synthesizer,
henceforth referred to as GPT-Synth.

The prompts used in this study were developed using the ”template” pattern as
described by White et al. (2023). This pattern has been shown to be highly
effective in situations where the generated output must conform to a specific
format that may not be part of the LLM’s training data. In particular, for
each benchmark task, we created a prompt that includes a description of our
DSL, and a set of example demonstrations and the environment states, along
with the correct programs for the desired task. For a novel task, we provide
the language model with the prompt, the demonstrations and environment states
for the novel task, and ask it to generate a corresponding program.

To use GPT 3.5 as an end-to-end synthesizer, we adopt the following
methodology, as done in prior work (Chen et al., 2021b). If the first program
returned by the LLM is consistent with the demonstration, GPT-Synth returns
that program as the solution. Otherwise, it asks the model to produce another
program, for up to 10 iterations. Unfortunately, we found that GPT-Synth is
unable to solve any of the benchmarks when we provide both the demonstrations
and the environment. This behavior seems to be caused by the large number of
entities and relations in the environment – prior work has reported similar
results in other domains (e.g., planning (Mahowald et al., 2023)) where LLMs
were used to perform tasks in non-trivial environments.

(a) GPT-Synth with environment

(b) GPT-Synth without environment

Figure 18. LLM Experiments

To gain more intuition about how the language model scales with the
environment size, we report on our experience with using GPT-Synth on five
representative tasks involving toy environments. We construct these toy
environments by incorporating _only_ the objects (and their properties)
required for that task plus some additional objects and properties. Figure
18(a) shows how the success rate of GPT-Synth scales with respect to
environment size. Here, the x-axis shows the number of additional objects (and
their properties) in the environment and the y-axis shows the success rate. As
we can see from Figure 18(a) , GPT-Synth works well if it is given _only_ the
relevant objects (which is not a realistic usage scenario), but, as
environment size increases, its success rate drops dramatically. In fact, when
the environment contains only 10 additional objects — a tiny fraction of our
“Easy” environment — the success rate of GPT-Synth already drops to zero.

The reader may wonder if the environment is actually necessary for GPT-Synth
to learn the correct program. To answer this question, we perform an
additional experiment where we provide GPT-Synth with only the demonstration,
but not the environment. The results of this evaluation are presented in
Figure 18(b), where we classify tasks into two categories as “Forall” and
“Conditional”. The former class of tasks does not involve branching, whereas
the latter does. Here, “Completed” shows the percentage of tasks for which
GPT-Synth finds a program consistent with the demonstration, and “Solved”
shows the percentage of tasks for which GPT-Synth returns a program that
_also_ matches the ground truth. As we can see, GPT-Synth returns a program
consistent with the demonstration for 45% of all tasks, but it is only able to
identify the ground truth program in 25% of the cases. Furthermore, as one
might expect, GPT-Synth is much more effective at the much simpler “Forall”
category of tasks that involve acting on all instances of a particular type.
In contrast, the “Conditional” category is much more challenging without
having access to the environment, and the success rate of GPT-Synth is only
11% for this category. Intuitively, without knowing which objects have what
properties, GPT-Synth has little chance of knowing that there should be a
conditional and what its corresponding predicate should be. We came across a
few cases where GPT-Synth is able to “hallucinate” the right predicates after
several rounds of interaction; but, in general, guessing the user’s intent
without knowing the environment, is at best a matter of sheer luck.

RQ3 Summary. prolex performs significantly better than the CVC5 and GPT-Synth
baselines. Even when given the ground truth sketches, CVC5 is only able to
return a program consistent with the final environment in 25% of the cases. On
the other hand, the GPT-based synthesizer cannot solve any tasks when provided
with both the demonstration _and_ the full environment, but it is able to
solve 25% of the tasks when it is given _only_ the demonstration.

##  7\. Related Work

_Robot Learning from Demonstrations._ Our approach builds upon a substantial
body of literature on the use of Learning from Demonstration (LfD) techniques
to learn robot execution policies (Argall et al., 2009; Sosa-Ceron et al.,
2022; Argall et al., 2008). This literature can be broadly categorized into
two approaches: (1) learning neural models to represent robot behaviors (Ly
and Akhloufi, 2021; Sünderhauf et al., 2018; Ziebart et al., 2008; Kober et
al., 2013; Ho and Ermon, 2016; Xiao et al., 2021; Taylor and Stone, 2009; Rusu
et al., 2017), and (2) synthesizing programmatic representations of execution
policies (Holtz et al., 2020a, 2021; Niekum et al., 2015; French et al.,
2019). The most well-established techniques for learning neural models from
demonstrations include behavior cloning within the framework of imitation
learning (Ly and Akhloufi, 2021; Ho and Ermon, 2016) and (deep) reinforcement
learning (RL) methods (Sünderhauf et al., 2018; Ziebart et al., 2008; Kober et
al., 2013). Empirical studies have demonstrated the efficacy of these neural
policies in perception tasks and their ability to perform well in unknown or
ill-defined environments. However, such neural models lack robust
interpretability and generalization capabilities — as a testament to this,
there exist no neural LfD algorithms to date capable of leveraging the user
demonstrations in the Behavior benchmarks (Srivastava et al., 2022). The field
of transfer learning (Pan and Yang, 2010; Taylor and Stone, 2009; Rusu et al.,
2017) aims to resolve generalization problems to some degree and also enhance
data efficiency. A related setting to our work is applying reinforcement
learning (RL) by specifying the task via formal specification of the goal
conditions; in fact, the Behavior benchmark set (Srivastava et al., 2022)
reports the results of such an approach. However, even in the simplest 12
activities, the RL algorithms are unable to complete the tasks even when
initiated close to the goal states. Further, even when the actions are
abstracted into symbols in Behavior-1K (Li et al., 2023), RL approaches
demonstrate very poor performance. These results mainly highlight the
complexity of the tasks that we tackle in this paper.

Recently, there has also been growing interest in developing techniques to
enhance the transparency and reliability of RL systems through formal
explanations (Topin and Veloso, 2019; Glanois et al., 2021; Krajna et al.,
2022; Li et al., 2019). These techniques aim to explain different aspects of
the learned models, such as inputs and transitions, by finding interpretable
representations of neural policies, such as Abstracted Policy Graphs (Topin
and Veloso, 2019) or structures in a high-level DSL (Verma et al., 2018). More
recently, there has also been interest in utilizing program synthesis methods
(Xin et al., 2023; Holtz et al., 2020b) to learn robot execution policies from
demonstrations as an alternative to neural model learning (Holtz et al.,
2020a, 2021). These approaches provide improved interpretability,
generalizability (Holtz et al., 2018), and data efficiency. prolex falls into
the same class of techniques as these approaches but broadens their
applicability in several ways: First, it can learn policies to handle long-
horizon tasks; second, it can synthesize programs with complex control flow,
such as loops with nested conditionals and loops; and, third, it can handle
environments with a large number of objects and properties.

Lastly, recent work proposes a methodology for automated learning of robotic
programs for long-horizon human-robot interaction policies from multi-modal
inputs, including demonstrations and natural language (Porfirio et al., 2019,
2023). The contributions of this work are largely complementary to ours: their
main focus is an interface for allowing end-users to draw the navigation path
of a robot on a 2D map of the environment and inferring symbolic traces from
this raw path representation. Similar to our regex-learning-based sketch
inference algorithm, the synthesizer in this work utilizes an automata