Veritas: Structuring and verifying LLM knowledge for logically consistent behavior tree generation in LLM-based agents

Behavior trees (BTs) have been widely adopted in autonomous task planning because of their modularity and reactivity. Recently, automatic BT generation based on Large Language Models (LLMs) has attracted growing research attention. However, synthesizing BTs for long-horizon tasks without relying on predefined expert rules remains an open problem, and it poses two key challenges: ensuring the logical consistency of the generated BTs, and maintaining their factual alignment with the ground truth of the environment. To address these challenges, this paper presents Veritas, a novel verification-driven framework for automatically generating logically consistent BTs. Veritas integrates STRIPS-like symbolic operators with a multi-layered verification mechanism, thereby transforming the planning process into a coherent chain of logical derivations. We further introduce Veritas+, which augments this framework with a memory module that accumulates both successful and failed execution experiences, enabling dynamic self-correction and improving factual consistency. We evaluate the framework on 67 long-horizon tasks in Minecraft and 116 real-world tasks in AndroidWorld. Experimental results show that Veritas and Veritas+ are highly effective and significantly outperform state-of-the-art baselines. • Proposes Veritas, integrating LLMs with symbolic logic for consistent behavior trees • Uses STRIPS-like operators and multi-layer verification for plan consistency • Introduces Veritas+ with contrastive memory for dynamic self-correction • Achieves state-of-the-art results on long-horizon tasks without manual modeling