CEDAR: A Counter-Example Driven Agent with Regular Restriction

We thank the reviewer for the constructive and thoughtful feedback. Below, we address your concerns regarding runtime efficiency, skill retention, expressivity, and technical questions.

W1: Runtime Budget Comparison.

Thank you for raising this important concern. CEDAR is designed to minimize LLM interaction costs during DFA learning. Unlike systems that depend on repeated prompting or iterative code refinement, CEDAR requires a single LLM query per learning mode: in active learning, the LLM generates a hypothesis program to answer membership queries using the LAPR algorithm; in passive learning, one query suffices to produce both positive and negative examples (see Section 3.1). To provide a comparable perspective under a fixed verifier budget (as in Voyager Figure 1), we include the table below. While figures are not supported in rebuttals, we will include the corresponding chart in the next revision.

This table reports the cumulative number of LLM queries issued during task completion for “Find a Diamond.” While CEDAR incurs slightly higher query counts early on (due to recursive alphabet construction), it learns and reuses skills without repeated LLM queries, leading to greater long-term efficiency.

W2: Automatic Skill Retention.

We would like to clarify that CEDAR does not require manual specification of which skills to retain. Skills are automatically stored in the Skill Manager once successfully learned (i.e., when no further counterexamples are found). From that point onward, skill reuse and adaptation are fully autonomous: starting from an empty skill library, CEDAR retrieves and updates skills using LLM-based specification matching and alphabet adaptation.

W3: Expressivity of DFA-based Skills.

We fully acknowledge that DFAs, as regular languages, are less expressive than Turing-complete programming languages like JavaScript. However, our design deliberately prioritizes verifiability, canonical representation, minimization, and learnability over expressivity. This tradeoff enables symbolic reasoning and formal guarantees, which are often lacking in free-form programmatic approaches.

To address common “counting” tasks (e.g., crafting a stone pickaxe), we introduce symbolic environmental events into the DFA alphabet—such as has_3_cobblestone and has_2_stick—extracted from the agent’s logs. This enables DFAs to encode milestone-based progress checks without requiring internal counters or memory.

Although DFAs cannot represent general looping or recursion, we observe that many Minecraft tasks decompose naturally into bounded sequences of actions. These can be modularly composed through skill chaining and DFA composition, allowing us to scale to more complex behaviors while maintaining interpretability and formal soundness.

Looking ahead, exploring more expressive classes of formal languages—such as context-free languages, visibly pushdown languages, counter automata, and recursive state machines—is an exciting direction for future work. These models strike a balance between expressivity and structure, and could potentially enable reasoning over richer task specifications while preserving many of the benefits offered by DFA-based representations.

Responses to Specific Questions.

• Skill Chaining: CEDAR’s skill chaining is not equivalent to straightforward sequential execution. If the first skill ends in a rejecting state, subsequent skills are not executed, ensuring logical consistency and robustness. In contrast, Voyager’s JavaScript-based skill chaining lacks formal success criteria and may proceed even after a failure.
• Quantity Conditions in Skills: We handle quantity constraints via symbolic events such as has_3_acacia_log, allowing the DFA to halt execution upon reaching the desired state. This avoids internal counters while supporting bounded accumulation tasks.
• Graph Comparable to Voyager Figure 1: Yes, we will include a comparable graph in the camera-ready version and have included a summary table above for reference.
• Causal Graphs (ADAM): Thank you for this reference. We agree that causal graphs provide valuable representations for task decomposition and reasoning. While orthogonal to our current verification focus, methods such as ADAM are complementary and can be integrated to enhance alphabet construction. We will discuss [2] accordingly.
• Majority Voting (SELP): Thank you for the great suggestion. Group voting schemes, as explored in SELP [3], are indeed compatible with CEDAR and could be leveraged to verify noisy or ambiguous DFA constructions produced by LLMs. We will include a discussion of this approach in the revised Related Work section and consider it as a promising avenue for improving robustness in formal specification inference.

References

[1] Voyager: An Open-Ended Embodied Agent with Large Language Models, Wang et al., NeurIPS 2023

[2] ADAM: AN EMBODIED CAUSAL AGENT IN OPENWORLD ENVIRONMENTS, Yu & Lu, ICLR 2025

[3] SELP: Generating Safe and Efficient Task Plans for Robot Agents with Large Language Models, Wu et al., ICRA 2025

We thank the reviewer for their time, feedback, and suggestions. We are grateful for the opportunity to clarify our contributions and address the concerns raised.

R1 Novelty

While our framework integrates established tools such as DFA learning and LLM prompting, the core novelty lies in rethinking DFAs as a practical, central representation for skills of open-world agents. In particular: :

• We introduce a novel DFA construction method via retrieval-augmented generation (RAG) that enables symbolic planning and fine-grained control by constructing task-specific sub-alphabets tailored to each specification.
• CEDAR unifies pretrained LLMs, environment feedback, and human-in-the-loop counterexamples to jointly infer formal skill and constraint representations.
• Skills are encoded as nested/hierarchical DFAs, allowing for symbolic skill retrieval based on automaton structure instead of brittle embedding similarity.
• While DFAs are celebrated for their theoretical properties, this work is the first to demonstrate their practical utility in a dynamic, open-world setting like Minecraft, where they offer tangible gains in controllability, robustness, and explainability.

R2: Comparisons with NL2LTL and Lang2LTL

Thank you for pointing us to these relevant and important works. We view them as complementary, and will add a discussion to the revised manuscript. However, direct comparison is not appropriate for several reasons:

• These works focus on offline translation of natural language into LTL specifications, not on learning or executing grounded policies.
• CEDAR supports interactive refinement via counterexamples and verification, whereas existing NL2LTL methods are typically one-shot translations.
• Several of the cited approaches are domain-specific or supervised, relying on curated datasets for grounding. In contrast, our approach operates zero-shot in a complex open-world environment.

We will include these papers in the Related Work and clarify how CEDAR’s goals and design differ.

R3: Improving Narrative Structure and Technical Clarity.

We thank the reviewer for the helpful suggestions regarding narrative clarity. We agree that a clearer exposition will further improve readability and accessibility. To implement this, we plan to introduce a running example (e.g., “Mine diamonds but sleep at night”) early in Section 3 to contextualize the agent’s control loop. We will also organize Section 3 along CEDAR’s full pipeline: specification → DFA learning → symbolic execution → runtime verification and skill refinement. To further aid clarity, we will supplement the Skill Manager and Verifier sections with algorithmic summaries and diagrams.

R4: Specific Clarifications

• Figure 3 (All States Accepting): Thank you for pointing this out. To avoid clutter, we omitted edges that lead to rejecting states. For instance, in state 8, transitions triggered by incorrect symbols (e.g., anything other than Midnight) would go to a sink state. We will revise the figure and caption to clarify this.
• Figure 8 (Pixelation): We will provide a higher-DPI, scalable version in the next revision.
• Runtime Failures: Yes, our framework handles runtime failures explicitly. If the Skill Manager encounters an action not found in the program logs (e.g., an unavailable transition), that edge is treated as failed and temporarily removed. The system then recomputes a new path to the accepting state. If no valid plan remains, the agent logs the failure as a counterexample, which can be used for future DFA refinement. This fallback mechanism ensures robustness even in dynamically changing or partially observable environments.

References

[1] Fuggitti, Francesco, and Tathagata Chakraborti. "NL2LTL–a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas." AAAI 2023

[2] Pan, Jiayi, Glen Chou, and Dmitry Berenson. "Data-efficient learning of natural language to linear temporal logic translators for robot task specification." ICRA 2023

[3] Liu, Jason Xinyu, et al. "Lang2ltl-2: Grounding spatiotemporal navigation commands using large language and vision-language models." IROS 2024

We thank the reviewer for their time and valuable comments. Below, we respond to each of the concerns and suggestions, and clarify our methodology, positioning, and future directions.

R1: Evaluation on Additional Domains. Thank you for the suggestion. We selected Minecraft as our primary testbed to enable a direct and fair comparison with Voyager, which was designed specifically for this environment. We agree that evaluating CEDAR in additional domains such as DMLab, VirtualHome, or AI2Thor would strengthen the case for generality. We are actively pursuing this direction as part of ongoing work.

R2: Comparison with World Models and RL-Based Techniques. We appreciate the reviewer’s suggestion to compare against world model and reinforcement learning approaches. That type of comparison definitely helps readers to better understand our method. However, our work specifically targets improving the decision-making abilities of LLM agents under the same assumptions as Voyager—namely, access to a pre-defined set of low-level skills (which RL is typically used to acquire). Unlike traditional RL agents that depend on extensive environment interaction and high-throughput simulators, both Voyager and CEDAR operate in low-throughput Minecraft environment without structured observation design. These limitations make standard RL training approaches impractical.

Our approach is grounded in DFA learning, which offers formal convergence guarantees. For example, active learning ensures that, given a finite hypothesis space (e.g., regular policies), the correct DFA can be identified with a bounded number of queries. In contrast, RL methods depend on noisy gradient estimates and typically require thousands of rollouts. Furthermore, CEDAR enables efficient skill synthesis and formal verification—capabilities that are difficult to achieve through RL policies. We will clarify this distinction in the revised manuscript and thank the reviewer for encouraging a deeper discussion of these tradeoffs.

R3 Novelty Clarification. While our approach builds on established components such as DFA learning and RAG, CEDAR contributes a novel integration of these components into a coherent agent architecture designed for open-world environments. In particular:

• CEDAR treats skills as regular languages that can be learned, composed, and verified—bridging natural and formal specifications.
• Unlike Voyager, which entangles control and planning in code generation, CEDAR uses explicit automata for skill execution, enabling verifiability, reuse, and symbolic generalization.
• The agent actively refines DFAs using counterexamples from the environment, supporting lifelong learning while maintaining formal rigor.

To the best of our knowledge, no prior work combines LLM-based automata learning, symbolic formal-language based skill execution, and environment- or human- driven counterexample refinement in this manner. We will revise the manuscript to better highlight this contribution and its implications for planning, safety, and alignment.

R4 Human Interaction.

Thank you for pointing this out. We clarify that human-provided counterexamples (CEs) are not used in CEDAR’s task completion experiments, including those reported in Tables 1 and 2. This design choice was made to ensure a fair comparison with Voyager, which does not involve human intervention. CEDAR accepts counterexamples from two sources:

• Environment-Collected CE: Counterexamples are gathered automatically through interaction with the environment. This is the primary mode used in our evaluations.
• Human-Provided CE: Used selectively to formalize high-level constraints or correct misaligned specifications, not during task completion.

The latter is demonstrated in Figures 5 and 6, where human counterexamples are used only to refine constraint DFAs, not to learn task-specific skills. This capability highlights CEDAR’s support for expert oversight and explainability, but it is not required for general skill learning.

We will clarify these distinctions in the revised manuscript to avoid any further confusion.

We thank the reviewer for their thoughtful and detailed evaluation of our work. Below, we address each of the reviewer’s concerns in turn, and clarify the motivation, design decisions, and experimental scope of our framework.

W1 Runtime performance comparison. Thank you for highlighting this point. To address the challenge of runtime efficiency in alphabet construction, we adopt a modular approach that decomposes the retrieval process into independent selection of verbs and nouns. Minecraft contains approximately 10 core control primitives (verbs), which enables lightweight LLM querying for verb selection. For nouns (game objects), we rely on embedding-based retrieval to identify the top-20 most relevant candidates based on the task description. These are combined to form a compact sub-alphabet, significantly reducing the search space and minimizing LLM usage during DFA construction.

Below, we provide a runtime comparison (mean ± standard deviation) for key execution stages between Voyager and CEDAR:

Although Voyager is slightly faster in most stages, it often requires multiple LLM iterations for code refinement, increasing its true cost. In contrast, CEDAR constructs and verifies DFA-based skills once and reuses them symbolically—eliminating repeated LLM queries. CEDAR’s skill retrieval is also faster and more robust due to symbolic matching over verb–noun pairs, with slightly higher variance arising from fallback LLM prompts when noun mismatches occur (see Section 3.2).

W2: Why Combine LLMs and DFAs? We appreciate the opportunity to clarify this design decision. Our goal is to integrate natural and formal languages to develop trustworthy and generalizable agents. LLMs are well-suited for interpreting high-level human intent, while DFAs offer unambiguous, interpretable and verifiable models of behavior over time. Existing RAG pipelines typically retrieve static documents, which lack the temporal structure and compositionality required for sequential decision-making. In contrast, DFAs naturally encode temporally extended behaviors, enabling CEDAR to learn, reuse, and verify structured skills. By retrieving over DFAs rather than raw text, we combine the expressivity of LLMs with the algorithmic properties of regular languages (minimization, canonical representability, closure operations, and efficient learning algorithms), yielding agents that are both generalizable and controllable.

W3: Online Skill Acquisition. Yes, CEDAR supports online learning of new skills during runtime. When the agent fails to retrieve a skill from its library, it invokes the active DFA learning algorithm (LAPR) to synthesize a new skill. This mirrors the task completion pipeline in Section 3.1, except that here, the task specification is generated by the LLM from contextual cues rather than given directly by a human. To manage Minecraft’s large action space, we employ: Task Decomposition to break complex instructions into smaller sub-tasks, and RAG-based Alphabet Construction to narrow the space of APIs to a relevant subset per skill. These design choices enable efficient and scalable lifelong learning, even in open-ended environments.

W4: Additional Baselines and DFA-only Variant. Our primary comparison is with Voyager, the state-of-the-art Minecraft agent at the time of submission. Given the rapid progress in LLM-based agents, we chose not to include comparisons with older methods like ReAct or AutoGPT, which lack the planning and verification capabilities necessary for fair benchmarking.

We appreciate the suggestion to evaluate the DFA skills without LLMs to show the upper bound performance. These DFAs are manually designed (Note that active and passive learning were not feasible in this setup, as the size of the Minecraft API space is too large to construct a reasonable alphabet without LLM assistance). The expert-designed DFA skills consistently achieved high performance across tasks. The only observed failure occurred due to an unfavorable map initialization, where the diamond block was too far from the agent’s spawn location.