Source-linked AI summary
CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action
Lekai Chen, Alvaro Velasquez, Ashutosh Trivedi
TL;DR
Embodied-agent instructions include persistent constraints that free-form code is difficult to verify, compose, or repair. CEDAR grounds instructions over event traces, uses LLM judgments and counterexamples to learn DFAs, and composes skills with specifications. In Minecraft, it maintains temporal and spatial constraints, supports amortized skill reuse, and reduces cumulative LLM queries relative to the described baseline setting.
Problem
Free-form programs generated for constrained embodied tasks provide no stable object for formal verification, composition with new constraints, or precise repair from failing traces.
Method
CEDAR learns goal and constraint regular languages from LLM membership judgments and execution counterexamples, then represents skills and specifications as deterministic finite automata.
Results
CEDAR maintains persistent temporal and spatial constraints in Minecraft, supports amortized skill reuse, and reduces cumulative LLM queries relative to the program-generating baseline.
Takeaways & Limitations
Regular languages provide a practical verification layer between natural-language instructions and embodied-agent policies within the evaluated symbolic, event-driven setting.
Takeaways & Limitations
Instruction fidelity depends on the selected alphabet and query feedback, while learned specification DFAs are not certified safety specifications for physical or safety-critical systems.
Abstract
from arXiv · showhide
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
CEDAR addresses the difficulty of preserving temporal, spatial, and safety constraints in changing environments by grounding instructions into explicit regular-language representations. It uses LLM semantic judgments, counterexamples, and automata composition to make learned skills and constraints inspectable, reusable, and repairable.
- Embodied-agent instructions often impose persistent temporal, spatial, and safety constraints beyond a terminal goal.
- Free-form programs and text memories are difficult to formally inspect, safely compose, or precisely repair from failure trajectories.
- CEDAR grounds natural-language instructions as regular languages over environment event traces and uses the LLM as a noisy semantic teacher.
- Skill and specification DFAs support product intersection, skill concatenation, counterexample-guided relearning, and template-based reuse.
2. CEDAR
CEDAR uses regular languages as a shared executable representation for learned skills and natural-language constraints. This representation supports composition, reuse, and counterexample-guided repair across the evaluated simulator settings.
- The shared representation distinguishes CEDAR from free-form code by exposing formal operations for intersecting, checking, reusing, and repairing learned behaviors.
- CEDAR represents both learned skills and natural-language specifications as deterministic finite automata.
- DFA composition combines skills with constraints through product intersection, while concatenation chains prerequisite and follow-up skills.
- Minecraft evaluates persistent constraint enforcement and amortized skill reuse, whereas iTHOR evaluates alphabet grounding and environment-backed counterexample repair.
2 Task Formulation
CEDAR formulates instruction following as grounding over symbolic event traces. It separates goal and constraint languages, learns their DFAs through semantic queries and counterexamples, and restricts predicates to implemented environment observations.
- CEDAR maps simulator/API observations to symbolic event words over a task-specific alphabet.
- The alphabet includes executable action-object symbols and logger-backed event predicates such as time=night and biome membership.
- The LLM selects among available predicates but does not create new sensors, because logger predicates require implemented environment queries.
- Each instruction induces a goal language and a constraint language, with DFA hypotheses learned for both.
- Membership queries ask whether traces should be accepted, while equivalence feedback supplies counterexamples from execution or human judgment.
3 CEDAR
CEDAR separates language-based semantic grounding from persistent DFA control, enabling learned skills and constraints to be composed, reused, and corrected through execution feedback. Its alphabet construction and constraint-enforcement design are evaluated in Minecraft, where the learned controller preserves the intended constraint representation.
- Core design: CEDAR uses the LLM for semantic judgments while DFAs provide persistent control structure for natural-language goals and constraints.The LLM selects symbols and answers membership queries; DFA learning and execution-backed counterexamples produce the controller.
- Alphabet construction: CEDAR constructs a task-specific alphabet from simulator/API state rather than assuming extra predefined observations.The global inventory contains 1,429 implemented Minecraft symbols, including action primitives, event predicates, and objects.
- Alphabet construction: Alphabet retrieval achieves absolute accuracy 0.9372±0.10 and overlap coefficient 0.9208 ± 0.10 against target alphabets from 44 validated skill DFAs.The LLM prunes retrieved verbs, objects, and event predicates into the finite alphabet used by the active learner.
- Alphabet construction: A missing global predicate prevents CEDAR from expressing the intended regular language, while an omitted retrieved predicate can leave the learned DFA semantically incomplete despite acceptance by the oracle.CEDAR may expand the alphabet and restart learning when execution exposes an omission, but this mechanism is not complete.
- Composition and reuse: Symbolic skill reuse is exact for matching verb-object queries and template-based for matching verbs with different objects, providing the main source of amortized efficiency.For a changed object, CEDAR substitutes noun-specific symbols and refines the adapted DFA through active learning.
- Composition and reuse: CEDAR stores skills and specifications as DFAs, supports product intersection for conjunction, concatenation for prerequisite and follow-up skills, and counterexample-guided relearning.The composed automaton accepts exactly the traces accepted by both component automata, although this guarantee does not certify that either learned DFA fully captures the original instruction.
- Constraint verification: In repeated three-day Minecraft trials aggregated over 24,000 ticks, CEDAR suppresses night-time work because its sleep constraint remains active throughout execution.Figure 3 reports action counts and average exact health for VOYAGER and CEDAR, with curves and error regions representing means and standard deviations.
4 Experiments
The experiments test whether CEDAR maintains natural-language constraints, reuses learned skills efficiently, grounds symbols and counterexamples reliably, and transfers its pipeline beyond Minecraft. Across Minecraft tasks, CEDAR persistently enforces temporal and spatial constraints while skill libraries reduce prompting overhead; iTHOR provides feasibility evidence without comparative benchmarking.
- Experimental Questions: The evaluation asks whether regular-language controllers preserve constraints, improve skill reuse and query cost, support reliable grounding and repair, and transfer beyond Minecraft.Minecraft compares CEDAR with VOYAGER and CODEACT under matched simulator/API access; iTHOR tests grounding and repair feasibility.
- Temporal Constraint Following: Runtime assertions improve local compliance, but none of the four code conditions achieves joint task-and-constraint success in five evaluated trials.Assertions can repair violations only when control returns to their boundary, whereas CEDAR carries specification state throughout execution.
- Temporal Constraint Following: CEDAR performs more total actions and collects more items by using daytime for exploration and nighttime for mineral extraction under a fixed 24,000-tick horizon.The experiment measures day-time mineral-mining action counts and reports object collection in Table 3 and temporal distributions in Figure 4.
- Spatial Constraint Following: For the windswept-forest instruction, CEDAR restricts activity to the target biome while the baseline traverses multiple biomes.Biome predicates are derived from simulator state available to both agents, making this a test of persistent non-temporal event predicates.
- Goal Completion and Skill Reuse: Among successful trajectories, CEDAR with a skill library uses fewer mean prompting iterations than VOYAGER with a skill library on four of five tasks.These means are conditioned on success and therefore are not unconditional efficiency estimates; cumulative-query accounting is reported separately.
- iTHOR Feasibility Study: Four of five iTHOR tasks succeed in a single pass, while a camera-perspective counterexample repairs COOK POTATO by inserting LOOKUP without additional LLM calls.The iTHOR study does not evaluate persistent constraint enforcement, skill reuse, or comparative performance outside Minecraft.
5 When Do Regular Languages Suffice?
CEDAR’s regular-language representation is suitable when tasks can be expressed with finite predicates and bounded event horizons, but it cannot represent unbounded memory or arbitrary recursion. The intended boundary is therefore finite-milestone, persistent temporal or spatial constraints backed by available environment predicates.
- Power and Boundary: DFAs recognize regular languages, so they cannot count indefinitely, store unbounded memory, or implement arbitrary recursion as general programs can.This limitation is also the source of CEDAR’s interpretability.
- Sufficiency Conditions: If numerical conditions become finite milestone predicates and subtasks finish within bounded horizon H, successful traces are regular.Under these assumptions, intersection preserves constraint enforcement and concatenation preserves skill chaining.
- Intended Use: CEDAR is appropriate for finite predicates and persistent temporal or spatial restrictions, but less appropriate for unbounded counting, arbitrary data structures, or uncaptured long-range memory.Richer models such as counter automata, visibly pushdown automata, or recursive state machines may be needed in those settings.
6 Related Work
CEDAR builds on prior automata learning, language-to-formal-specification, and program-verification work while changing the interface between language and embodied control. Its distinctive scope is learning both executable skill and constraint automata from API-grounded symbols, semantic judgments, and execution counterexamples.
- Natural-Language Formalization: NL-to-temporal-logic methods typically assume a proposition vocabulary, whereas CEDAR retrieves an API-backed alphabet and learns an executable DFA through active judgments and execution counterexamples.The supervision assumptions differ, and the paper does not empirically establish superiority over NL-to-LTL systems.
- Program Verification: Prior work verifies LLM-generated robot programs with automata and external safety specifications; CEDAR instead learns both the skill automaton and the natural-language constraint automaton.The broader use of automata for verification is not claimed as novel.
- Active Automata Learning: CEDAR inherits active DFA learning and LLM semantic-teacher ideas rather than introducing a new active automata-learning algorithm.Its contribution is applying these ideas within an embodied-agent architecture.
- Counterexample-Guided Learning: CEDAR uses execution inconsistencies as counterexamples in a task-specific simulator-API setting, differing from reward-machine relearning and related policy-learning approaches.Its grounding problem is finite-state specification learning from natural language and counterexamples.
- Scope of Claims: A learned CEDAR specification could in principle shield another controller, but the paper does not compare against independently validated formal specifications or claim certified safety.The learned DFAs are therefore not presented as independently certified safety specifications.
7 Conclusion
CEDAR uses regular languages as a shared executable representation for learned embodied skills and natural-language constraints. In the evaluated symbolic, event-driven setting, this supports composition, reuse, counterexample-guided relearning, and persistent temporal and spatial constraint following.
- Conclusion: CEDAR uses regular languages as a shared verifiable representation for learned embodied skills and natural-language constraints.The contribution is a common executable substrate rather than a new DFA-learning algorithm.
- Conclusion: Skill and specification automata support product intersection, skill chaining and reuse, and returning failing execution traces as counterexamples for relearning.Minecraft provides evidence for persistent temporal and spatial constraint following and amortized skill reuse; iTHOR demonstrates pipeline instantiation in another simulator.
- Conclusion: The results support regular languages as a practical common substrate when instructions can be represented through finite predicates.This conclusion is limited to the evaluated symbolic, event-driven setting.
Limitations
CEDAR’s guarantees are scoped by its symbolic representation, feedback quality, composition size, and evaluated environments. Its resource advantages are reported for specific protocols, while alphabet omissions and incorrect feedback can undermine instruction fidelity.
- Minecraft provides the main evidence for persistent constraint enforcement and amortized skill reuse; iTHOR evaluates only alphabet grounding and counterexample repair.
- The evaluated environments are discrete and symbol-rich, with no claimed advantage for continuous-control policies requiring unbounded memory, arbitrary data structures, or fine-grained continuous state.Learned specification DFAs are not certified safety specifications for physical robots or safety-critical systems without independently validated sensing, specifications, runtime enforcement, and fail-safe control.
- DFA intersection exactly enforces the learned automata’s languages, but instruction fidelity depends on alphabet selection and correct membership- and equivalence-query feedback.Missing predicates can silently omit intended clauses, and execution-backed alphabet expansion is incomplete and not systematically measured.
- Incorrect or conflicting human counterexamples can steer learning toward an incorrect specification DFA, but robustness to such feedback was not established.The reported specification feedback came from one human expert, so inter-annotator sensitivity was not measured.
- Product automata have worst-case multiplicative state growth, and the experiments do not guarantee general scalability beyond the tested small compositions.Retrieval was evaluated on a fixed 1,429-symbol inventory without controlled variation in inventory size or target-automaton complexity.
- 37 LLM queries versus 75 for VOYAGER at the final Find a Diamond milestone demonstrates amortized query savings under the reported protocol.CEDAR pays more queries at the first logging milestone, then uses fewer cumulative queries from the Cobblestone milestone onward.
C Additional Results
Additional analyses examine counterexample discovery, expert-designed DFA performance, human feedback, alphabet construction, and CAPAL’s learning and cache-update mechanisms. They clarify both how the system operates and where its feedback-driven repair can fail.
- Most observed counterexamples have length below seven, where simulation-based collection probability remains high.Rare long-horizon failures remain possible when an incorrect transition appears only after a long execution prefix.
- Expert-designed DFA skills achieved 10/10 success on four Minecraft tasks and 9/10 on Diamond Pickaxe, whose failure was caused by map initialization.This upper-bound diagnostic bypasses the language-grounding problem and is not a learning baseline.
- Human specification feedback used trajectory annotation, demonstration logs, or direct formal trace judgments, while it was not used for task-skill learning, code-baseline comparisons, or iTHOR.The reported specification demonstrations were supplied by one human expert.
- The RAG alphabet constructor retrieves environment-bound candidate symbols and asks the LLM to select a compact task-specific alphabet, combining verbs with appropriate nouns and leaving event predicates standalone.The selected predicates are symbolic recodings of existing simulator/API observations rather than additional perceptual inputs.
- A missing predicate such as has_3_cobblestone can make the DFA over-accept or fail to distinguish progress states; counterexample-triggered expansion may recover it but is not guaranteed.Recovery fails when the available oracle does not recognize the semantic mismatch.
- CAPAL integrates semantic membership judgments, cached evidence, hypothesis DFAs, and execution-backed counterexamples, rebuilding its state partition rather than directly patching transitions.Counterexamples may add structural discriminators, provide label-only gold overrides, or trigger alphabet-dependent learner restarts with compatible cached labels replayed.
- Persistent-noise reconciliation caches the first membership judgment for each word, while execution-supplied counterexample labels override cached judgments.Repeated queries for the same word are not resampled or aggregated.
- CAPAL’s statistical class query estimates disagreement over a capped suffix sample and declares prefixes equivalent only under the stated threshold condition.Only DIFFERENT outcomes are cached, with cache keys incorporating the prefix pair, suffix-set version, and decision threshold.
H Assertion-Baseline Statistics
The assertion-baseline statistics report exact binomial confidence intervals for task outcomes and clarify how success, constraint compliance, joint success, and product-automaton size are interpreted.
- Exact two-sided 95% binomial confidence intervals accompany the three binary outcomes in Table 2, but five trials per condition make them necessarily wide.The sleep-at-night comparison reports marginal binary outcomes and does not remove uncertainty from the small sample.
- Exact two-sided 95% binomial confidence intervals accompany the success counts in Table 4, covering task success rather than conditional prompting-iteration means.Table 4 spans 25 trials per method–task condition, and S.L. denotes a skill library.
- The skill–constraint product DFA has worst-case size |Qg||Qc|, while Table 13 reports reachable states after unreachable product states are removed.