CEDAR: 言語誘導型身体的行動のための検証可能なインターフェースとしてのオートマトン
CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action
自然言語の指示を正規言語として表現し、決定性有限オートマトンに変換することで、制約を検証可能な実行可能なオブジェクトとして扱うフレームワークを提案。Minecraftで時間的・空間的制約を維持し、LLMクエリを削減できることを示した。
詳しい要約
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術・手法の肝は？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
※ AIが要旨から生成した要約です。正確性は原文をご確認ください。
著者: Lekai Chen, Alvaro Velasquez, Ashutosh Trivedi
分類: cs.AI, cs.CL, cs.FL
原文アブストラクト
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.