PaperlayerView exact revision on arXiv

Source-linked AI summary

CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action

Lekai Chen, Alvaro Velasquez, Ashutosh Trivedi

arXiv:2608.27797v1cs.AIcs.CLcs.FL

TL;DR

Embodied agents must preserve user constraints as worlds change, but free-form programs are hard to inspect and safely compose. CEDAR represents skills and constraints as automata, and Minecraft experiments provide evidence of persistent constraint following and amortized skill reuse.

  • Problem

    Embodied agents must preserve temporal, spatial, and safety constraints, yet free-form skill programs are difficult to inspect formally, compose safely, or repair from failures.

    Source: §1 · p. 1

  • Method

    CEDAR grounds trajectories as symbolic event words and represents skills and natural-language specifications as DFAs that can be composed and refined using counterexample traces.

    Source: §1 · p. 1, §2 · p. 2

  • Results

    Minecraft experiments provide evidence that CEDAR maintains temporal and spatial constraints, including against assertion-augmented code baselines, and amortizes skill reuse.

    Source: §7 · p. 9

  • Takeaways & Limitations

    Within evaluated symbolic, event-driven settings, regular languages offer an explicit layer for composing learned skills with constraints.

    Source: §7 · p. 9

    Learned specification DFAs are not certified safety specifications and are insufficient for physical robots or other safety-critical systems without independent validation and fail-safe control.

    Source: Limitations · p. 10

Abstract

from arXiv · show

Natural-language tasking of embodied agents is rarely just goal specification: users also impose constraints that must persist while the world changes. Code-generating LLM agents can produce plausible behaviors for such instructions, but their free-form programs provide no stable object to verify, compose with new constraints, or repair from a failing trace. We present CEDAR, a counterexample-guided framework that grounds instructions as regular languages over environment event traces. CEDAR uses a language model for semantic judgments and execution traces for correction, then represents both skills and specifications as deterministic finite automata. This turns constraints into executable finite-state objects: a learned skill can be intersected with a learned sleep at night or stay in this biome specification, yielding a controller that enforces the learned constraint by construction rather than by repeated prompting. In Minecraft, with the same simulator/API observations available to a program-generating baseline, CEDAR maintains temporal and spatial constraints that the baseline fails to preserve and amortizes reuse of learned skills, reducing cumulative LLM queries. These results suggest that regular languages offer a practical verification layer between natural-language instructions and embodied-agent policies.

1 Introduction

Embodied-agent instructions often impose persistent temporal, spatial, and safety constraints, not just terminal goals; CEDAR grounds instructions as regular languages over event traces and represents skills and constraints with automata.

1 Introduction

  • Prior LLM-agent systems generate code, decompose goals, store skills, or interleave reasoning and action, but free-form programs are hard to inspect, compose safely, and repair from failures (Yao et al., 2023; Wang et al., 2023; Zhu et al., 2023; Liu et al., 2023; Wang et al., 2024).A generated program may satisfy a constraint once and later forget it.Source: §1 · p. 1
  • An LLM acts as a semantic teacher for alphabet selection and trace-membership queries, while a DFA learner and environment-backed equivalence oracle produce automata and counterexamples.The learned automaton is minimal up to isomorphism for the learned regular language, can be checked by replaying event traces, and supports operations including intersection and concatenation.Source: §1 · p. 1
  • CEDAR’s event predicates are read-only functions over simulator/API state, and the VOYAGER baseline has access to the same underlying state variables; the difference is representational and architectural.CEDAR exposes persistent finite-state objects that can be intersected, checked, reused, and repaired, unlike free-form code skills.Source: §1 · p. 2
  • CEDAR is, to the authors’ knowledge, the first embodied-agent framework to use regular languages as shared executable representations for learned skills and natural-language constraints.Skills and specifications are represented as DFAs that can be intersected, prerequisite and follow-up skills concatenated, and failing traces returned as counterexamples for repair; the contribution is not a new DFA-learning algorithm.Source: §1 · pp. 1–2
  • Minecraft experiments evaluate persistent constraint enforcement and amortized skill reuse, while the iTHOR study tests whether alphabet grounding and environment-backed counterexample repair transfer to another simulator.The iTHOR study evaluates only those instantiation capabilities.Source: §1 · p. 2

2 Task Formulation

CEDAR represents instructions as goal and constraint languages over symbolic event traces, then learns deterministic finite automata from language-model judgments and execution or human counterexamples. Its event symbols are grounded in implemented simulator/API queries rather than invented sensors.

2 Task Formulation

  • CEDAR converts simulator/API observations into finite event words using logger predicates for actions, objects, and observed conditions backed by implemented environment queries.The available observations include inventory, time, biome, and nearby objects; the LLM selects from available predicates but cannot create sensors.Source: §2 · pp. 2–3
  • Each instruction induces goal and constraint languages over traces, for which CEDAR learns separate DFA hypotheses to represent desired outcomes and prohibited behavior.For “collect diamonds but sleep at night,” the goal accepts diamond collection, while the constraint rejects continuing to work through night without sleeping.Source: §2 · p. 3
  • CAPAL learns the DFAs through membership judgments from an LLM and equivalence-query counterexamples from environment execution or human specification judgments.For skill DFAs, the environment returns counterexamples when accepted behavior fails to achieve the outcome or rejected behavior is feasible; humans may provide specification counterexamples through annotation, demonstration, or trace judgment.Source: §2 · p. 3

3 CEDAR

CEDAR separates LLM semantic judgments from DFA-based control, making learned skills and constraints persistent automata that can be composed rather than left as prompt context.

3.1 Alphabet Construction

  • CEDAR’s Minecraft inventory contains 1,429 implemented symbols; against target alphabets from 44 validated skill DFAs, it achieves absolute accuracy 0.9372±0.10 and overlap coefficient 0.9208 ± 0.10.Each candidate pairs a natural-language description with an executable binding to an environment query, action primitive, or logger predicate; the LLM retrieves and prunes candidates into the task alphabet.Source: §3.1 · p. 4
  • When required predicates are unavailable, CEDAR cannot express the intended language; omitted retrieved predicates may trigger alphabet expansion and relearning, but the approximate oracle can miss omissions.An omitted predicate can leave the learned DFA accepting despite failing to capture the full intended semantics.Source: §3.1 · p. 4

3.2 Active DFA Learning under Noise

  • CEDAR learns DFAs under noisy LLM membership answers by reconciling repeated queries in a cache and refining hypotheses with execution counterexamples from failed or goal-missing traces.For skills, it executes a shortest path to acceptance, disables unavailable or unsuccessful transitions, and terminates after successful execution without a counterexample within the interaction budget.Source: §3.2 · p. 4

3.3 Skill Storage, Retrieval, and Adaptation

  • For a new verb-object query, CEDAR reuses an exact-match skill DFA, adapts and refines a same-verb DFA for a new object, or learns anew for a different verb.Stored skill evidence comprises membership-query labels and equivalence counterexamples; symbolic reuse is the main source of amortized efficiency.Source: §3.3 · p. 4

3.4 Verifying Natural-Language Constraints

  • Intersecting learned skill and specification DFAs accepts exactly traces accepted by both, enforcing their conjunction with respect to those automata.This is not a certificate that either DFA fully captures the original instruction; specifications use the same learning procedure, with human counterexamples when constraints are ambiguous.Source: Figure 2 · p. 3, §3.4 · pp. 4–5
  • CEDAR chains skills by connecting prerequisite accepting states to the follow-up DFA, exposing whether the prerequisite succeeded before the next skill begins.In the sleep-at-night trials, CEDAR suppresses night-time work over three Minecraft days (24,000 ticks).Source: §3.4 · p. 5, Figure 3 · p. 5

4 Experiments

CEDAR is evaluated as a DFA-based approach to persistent temporal and spatial constraints, skill reuse, grounding reliability, and feasibility beyond Minecraft. The experiments compare agents with matched simulator/API information and treat iTHOR as a feasibility study, not a comparative benchmark.

4 Experiments

  • Minecraft baselines receive the same instruction and simulator/API state, and CEDAR’s predicates recode available state variables; human counterexamples are reserved for high-level specification demonstrations.They are not used for skill learning, code-baseline comparisons, or iTHOR experiments.Source: §4 · p. 5

4.1 Constraint Following in Minecraft

  • None of four code conditions achieved joint task-and-constraint success in five trials; runtime assertions improved local compliance, while CEDAR keeps the learned specification state active throughout execution.Assertions can repair a violation only when control returns to their boundary, so a long-running or reused skill may continue after night begins.Source: Table 2 · p. 6, §4.1 · p. 6
  • Under 24,000 ticks per trial, CEDAR performs more actions and collects more underground and overground objects and total items, using daytime for exploration and nighttime for mineral extraction.The paper attributes the higher action count to this division of activity under the fixed horizon.Source: Table 3 · p. 6, §4.1 · p. 6, Figure 4 · p. 6
  • CEDAR stays in the requested windswept forest, whereas VOYAGER traverses multiple biomes, demonstrating persistent enforcement of a spatial predicate from shared simulator state.Figure 5 aggregates location visits over five trials.Source: §4.1 · p. 6, Figure 5 · p. 7

4.2 Goal Completion and Skill Reuse

  • Among successful trajectories, CEDAR with a skill library uses fewer mean prompting iterations than VOYAGER with one on four of five tasks; these success-conditioned means are not unconditional efficiency estimates.Without a skill library, CEDAR incurs additional interactions to learn and test a DFA; the paper points to separate cumulative-query accounting for the amortization claim.Source: Table 4 · p. 7, §4.2 · p. 7

4.3 Grounding Reliability

  • Retrieval achieves absolute accuracy 0.9372 ± 0.10 and overlap coefficient 0.9208 ± 0.10; environment-backed counterexample discovery averages 0.9358, while absent, rare, or noisy predicates remain failure modes.These analyses do not establish that every relevant predicate will be retrieved or that silent alphabet omissions will always be detected.Source: §4.3 · p. 7

4.4 iTHOR Feasibility Study

  • In iTHOR, four of five tasks succeed in one pass; a camera-perspective failure in COOK POTATO is repaired by adding LOOKUP without extra LLM calls, but the study is not a comparative benchmark.The five-task feasibility study does not evaluate persistent constraint enforcement, skill reuse, or amortized reuse outside Minecraft.Source: §4.4 · p. 8, Figure 6 · p. 8

5 When Do Regular Languages Suffice?

CEDAR’s DFA representation is interpretable but limited to regular languages. Finite milestone predicates and bounded event horizons make successful subtask traces regular, while tasks requiring unbounded memory may need richer models.

5 When Do Regular Languages Suffice?

  • DFAs recognize regular languages, so they cannot count indefinitely, store unbounded memory, or implement arbitrary recursion as JavaScript programs can.Source: §5 · p. 8
  • CEDAR’s task alphabet includes thresholded, temporal, and spatial predicates; with finite milestone predicates and bounded event horizon H, successful subtask traces are regular, and intersection and concatenation preserve regularity.Examples include has_3_cobblestone, time=night, and in_biome(x).Source: §5 · p. 8
  • CEDAR suits finite milestones and persistent temporal or spatial restrictions backed by environment predicates, but tasks requiring unbounded counting, arbitrary data structures, or uncaptured long-range memory may need richer formal models.Suggested extensions include counter automata, visibly pushdown automata, and recursive state machines; DFAs may still serve as learned constraints.Source: §5 · p. 8

6 Related Work

Related work positions CEDAR as an embodied-agent architecture that uses established automata-learning and counterexample-refinement ideas to learn executable skill and language-constraint automata and compose them. The paper distinguishes this interface from prior approaches and limits claims about comparative superiority and certified safety.

6 Related Work

  • Unlike NL-to-temporal-logic methods that typically assume a proposition vocabulary, CEDAR retrieves an API-backed alphabet and learns a DFA; the paper does not establish empirical superiority over those systems.An NL-to-LTL front end could initialize a specification DFA when its output is regular or compilable to a finite monitor, with counterexample-guided repair remaining complementary.Source: §6 · pp. 8–9
  • Yang et al. (2024) verify automaton representations of LLM-generated programs against supplied safety specifications; CEDAR instead learns skill and constraint automata from judgments and traces, then composes them.The paper explicitly does not claim automata-based verification of generated programs as novel.Source: §6 · p. 9
  • CEDAR inherits active DFA-learning ideas from Angluin (1987), Chen et al. (2026), and Vazquez-Chanlatte et al. (2024), contributing their use in an embodied architecture with a shared executable representation for skills and constraints.The paper does not claim a new active automata-learning algorithm.Source: §6 · p. 9
  • Xu et al. (2020) also use execution inconsistencies to refine automata, while safe-RL and shielding methods (Gu et al., 2024) generally assume an available constraint; CEDAR learns one from language and counterexamples.CEDAR task-specific alphabets come from simulator APIs, and LLM judgments assess trace membership. The paper neither compares against systems supplied with independently validated formal specifications nor claims its learned DFAs are certified safety specifications.Source: §6 · p. 9
  • CEDAR complements efficient-LLM-reasoning methods (Ye et al., 2026a; Guo et al., 2026; Ye et al., 2026b) by reducing the symbolic decision space through task-specific alphabet retrieval.The cited methods reduce effective reasoning space through relevance-based pruning, structured search, model routing, and cache reuse.Source: §6 · p. 9

7 Conclusion

CEDAR uses regular languages as a verifiable representation for learned embodied skills and natural-language constraints. Its experiments support persistent constraint following and skill reuse in Minecraft, and show the pipeline can also be instantiated in iTHOR.

7 Conclusion

  • CEDAR is the first framework to use regular languages as a verifiable representation for learned embodied skills and natural-language constraints.The conclusion frames regular languages as a practical common substrate when instructions can be represented through finite predicates.Source: §7 · p. 9
  • Skill and specification automata can be combined by product intersection, skills chained and reused, and failing execution traces returned as counterexamples for relearning.This shared representation makes learned instruction semantics explicit within the evaluated symbolic, event-driven setting.Source: §7 · p. 9
  • Minecraft experiments provide evidence for persistent temporal and spatial constraint following relative to VOYAGER and CODEACT variants with the same runtime assertion-and-repair condition, and for amortized skill reuse.The iTHOR study demonstrates that the pipeline can also be instantiated in another simulator.Source: §7 · p. 9

Limitations · A LLM Query and Runtime Cost · B Alphabet Retrieval Details

CEDAR’s cost is front-loaded and amortized through DFA reuse, while the reported evidence is bounded by the evaluated environments, feedback assumptions, alphabet, and scalability tests. The alphabet retriever selects task-relevant symbols from existing simulator/API observations, but does not add perceptual inputs.

Limitations

  • Evidence for persistent constraint enforcement, skill composition, and amortized reuse comes from Minecraft; iTHOR tests only alphabet grounding, predicate binding, and counterexample repair.CAPAL assumes structured simulator/API observations and does not reliably extract predicates from raw visual input; the evaluated environments are discrete and symbol-rich, with no claimed advantage for policies requiring unbounded memory, arbitrary data structures, or fine-grained continuous state.Source: Limitations · pp. 9–10
  • DFA intersection exactly enforces represented languages, but instruction fidelity depends on the selected alphabet and correct membership- and equivalence-query feedback.Missing predicates can silently omit intended clauses while still permitting acceptance; execution-backed alphabet expansion may reveal some omissions but is incomplete, and their rate is not systematically measured.Source: Limitations · p. 10
  • Incorrect human counterexamples can steer CAPAL toward an incorrect automaton, and robustness to incorrect or conflicting feedback is not established.Where only one provider was used, inter-annotator sensitivity cannot be estimated.Source: Limitations · p. 10
  • Product automata have worst-case multiplicative state growth, and the small tested compositions do not establish general scalability.Retrieval was evaluated on the current 1,429-symbol inventory without controlled variation in inventory size or target-automaton complexity.Source: Limitations · p. 10
  • Learned specification DFAs are not certified safety specifications and are insufficient for physical robots or other safety-critical systems without independently validated sensing, specifications, runtime enforcement, and fail-safe control.Exact composition cannot correct incorrectly grounded semantics.Source: Limitations · p. 10

A LLM Query and Runtime Cost

  • 37 LLM queries versus 75 for VOYAGER at the final diamond milestone show CEDAR’s cumulative-query advantage after its early construction cost.CEDAR uses more queries at the first logging milestone but fewer cumulative queries from the Cobblestone milestone onward. Under the reported protocol, DFA construction adds time while skill-addition and total execution time are much lower.Source: Table 5 · p. 12, Figure 7 · p. 12, A LLM Query and Runtime Cost · p. 12

B Alphabet Retrieval Details

  • The retriever achieves high absolute accuracy and overlap against target alphabets derived from 44 validated skill DFAs.It retrieves candidate symbols with implemented environment bindings for LLM pruning into a compact alphabet; these are symbolic recodings of existing simulator/API observations, not new sensors.Source: B Alphabet Retrieval Details · p. 12, Figure 8 · p. 12, Table 7 · p. 12

C Additional Results … G CEDAR Instantiation of CAPAL

The supplied additional material examines counterexample discovery and expert DFA performance, documents specification-feedback and alphabet-construction procedures, and details CAPAL’s learning mechanics and limitations. It shows that CEDAR’s guarantees depend on discoverable counterexamples and semantically sound feedback.

C.2 Counterexample Discovery by Item

  • Most simulated counterexamples are shorter than seven events, where collection probability remains high.Longer counterexamples are harder to surface during simulation.Source: Figure 9 · p. 13

C.3 Expert DFA Reference

  • Expert-designed DFAs achieved 10/10 success on four Minecraft tasks and 9/10 on Diamond Pickaxe, whose failure resulted from map initialization.This upper-bound diagnostic assumes expert construction and bypasses language grounding; it is not a learning baseline.Source: §C.3 · p. 13

D Human Counterexample Accounting

  • Human feedback was limited to high-level specification demonstrations, with interventions recorded across three modalities and reported annotation time.It was not used for Minecraft skill learning, code-baseline comparisons, or iTHOR experiments; the specification feedback came from one human expert, so the experiments do not assess disagreement or sensitivity to alternative interpretations.Source: D Human Counterexample Accounting · p. 13, Table 10 · p. 13, Figure 10 · p. 13

E Prompt Sketch for Alphabet Construction

  • The alphabet constructor retrieves candidate symbols with implemented environment bindings, then prompts an LLM to select relevant verb–noun combinations and standalone event predicates.The prompt gives examples such as pairing mine with blocks and smelt or place with items.Source: E Prompt Sketch for Alphabet… · p. 13

F Failure Modes

  • Without a predicate for a required milestone, a DFA may misrepresent progress; a counterexample can trigger alphabet expansion, but recovery is not guaranteed.If the oracle misses the semantic mismatch, the incomplete DFA may still accept; this is a logger/alphabet limitation, not an observation-advantage assumption.Source: F Failure Modes · pp. 13–14
  • Rare long-horizon errors are difficult to expose, and shared LLM–human misunderstandings can direct learning toward the wrong specification.Counterexamples help only when an oracle recognizes the mismatch; CEDAR does not claim robustness to systematically incorrect equivalence feedback.Source: F Failure Modes · p. 14

G CEDAR Instantiation of CAPAL

  • CEDAR caches each word’s first membership judgment, while counterexample labels override it; CAPAL uses sampled suffix disagreement to compare prefixes.Alphabet expansion restarts alphabet-dependent learner state but replays compatible cached judgments and gold labels, preserving prior semantic evidence without reusing an invalid state partition.Source: G CEDAR Instantiation of CAPAL · p. 15
  • CAPAL updates its state from labeled counterexamples, using Rivest–Schapire analysis to add structural discriminators or treating some examples as label-only corrections.Repeated label-only counterexamples can add suffixes to separate merged classes; consistency repairs use the discrimination tree, and CAPAL rebuilds the partition and DFA rather than directly patching a transition.Source: G CEDAR Instantiation of CAPAL · p. 15

H Assertion-Baseline Statistics

The section reports exact two-sided 95% binomial confidence intervals for three binary outcomes and cautions that five trials per condition leave the intervals wide.

H Assertion-Baseline Statistics

  • The intervals are necessarily wide because each condition contains only five trials.The section describes them as exact two-sided 95% binomial confidence intervals for the three binary outcomes in Table 2.Source: H Assertion-Baseline Statistics · p. 15, Table 11 · p. 16
  • Table 11 reports observed success counts and exact two-sided 95% Clopper–Pearson confidence intervals for the five-trial sleep-at-night comparison.The intervals describe marginal binary outcomes and do not eliminate uncertainty from the small sample.Source: Table 11 · p. 16

I Goal-Completion Success Intervals · J Automaton State Counts

The section specifies the scope of task-success confidence intervals and reports how skill–constraint automaton sizes are measured after unreachable product states are removed.

I Goal-Completion Success Intervals

J Automaton State Counts

Related papers

Loading 2608.27797v1…