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.