DecoVer: A Decompose-and-Verify Neuro-Symbolic Framework for Embodied Task Planning with BC+

Despite their remarkable general capabilities, Large Language Models (LLMs) struggle with the precise grounding required for embodied task planning. To bridge this gap, neuro-symbolic approaches have emerged, leveraging action languages like BC+ for their formal expressiveness and reasoning flexibility. However, prior methods that naively couple LLMs with BC+ typically depend on one-shot program generation, which is brittle in dynamic environments and prone to sequential omission and causal inconsistency. To address these limitations, we propose DecoVer, a Decompose-and-Verify neuro-symbolic framework that systematically adapts BC+ to embodied task planning. Specifically, DecoVer employs a cascading decomposition strategy to partition complex knowledge into hierarchical subspaces and integrates a dual verification mechanism for syntactic and executable correctness. Extensive experiments demonstrate that DecoVer consistently outperforms LLM-based baselines across the majority of evaluation metrics, achieving a 12.9% success rate gain over the highly capable Gemini-3-Pro-Preview and a 60.9% improvement over GPT-5.1 on logically complex test cases.

We wish to deploy AI as brains of robots to perform specific daily household tasks. However, while advanced AI is smart, it often struggles with the strict physical rules of the real world. For example, an AI might forget a crucial step, like opening a cabinet before grabbing a cup inside, or it might lose track of the status of objects. Therefore, we shifted the AI's role from a direct decision-maker to a writer of a control program. To ensure these programs are flawless to our best effort, we broke down the writing process into smaller, manageable steps and added strict verification checks at key stages. This greatly improves the quality of the generated code. The final program can then reliably provide an accurate sequence of actions to safely control the robot upon execution. Our experiments prove that this method improve the success rate of planning tasks for even the most advanced AI models.