A Category-Theoretic Approach to Neural-Symbolic Task Planning with Bidirectional Search (2025)

Abstract: We introduce a Neural-Symbolic Task Planning framework integrating Large Language Model (LLM) decomposition with category-theoretic verification for resource-aware, temporally consistent planning. Our approach represents states as objects and valid operations as morphisms in a categorical framework, ensuring constraint satisfaction through mathematical pullbacks. We employ bidirectional search that simultaneously expands from initial and goal states, guided by a learned planning distance function that efficiently prunes infeasible paths. Empirical evaluations across three planning domains demonstrate that our method improves completion rates by up to 6.6% and action accuracy by 9.1%, while eliminating resource violations compared to the existing baselines. These results highlight the synergy between LLM-based operator generation and category-theoretic verification for reliable planning in domains requiring both resource-awareness and temporal consistency.

## introduction effective task planning remains a critical challenge in artificial intelligence, particularly in domains where resource constraints, temporal consistency, and trustworthiness are paramount @xcite @xcite . large language models (llms) @xcite @xcite offer powerful generative capabilities for natural language planning, but frequently overlook domain constraints @xcite , yielding plans that violate resource limitations or temporal dependencies @xcite . in contrast, classical symbolic planners @xcite @xcite ensure formal correctness but suffer from limited flexibility and require extensive domain engineering. recent research has attempted to bridge this conceptual gap through methods such as chainof-thought @xcite , monte carlo tree search (mcts)-based planning @xcite , and reinforcement learning methods @xcite . however, these approaches encode constraints as heuristic signals or sparse rewards @xcite without providing structural guarantees. other reasoning-oriented approaches such as tree-of-thoughts (tot) @xcite , re-woo @xcite improve reasoning depth and search efficiency, but still lack mechanisms for ensuring compositional validity of generated plans. as benchmark evaluations of llm planning expand @xcite , the need for principled approaches that unify neural flexibility with formal constraint enforcement becomes urgent. we address these challenges by introducing neural-symbolic task planning (figure 1 ). the framework comprises three key innovations: our contribution centers on the integration of category-theoretic verification with neural operator generation and search. this enables our framework to act as a constraint-safety layer that can be applied to llm-driven planners, including cot @xcite , react @xcite , tot @xcite , ensuring that generated plans remain resource-aware, temporally consistent, and logically valid. we evaluate our framework across three diverse planning domains: cooking recipes (recipenlg) @xcite , procedural texts (processbench) @xcite , and standardized procedures (proc2pddl) @xcite . our method consistently achieves 15-25% higher completion rates than other baselines, while substantially reducing resource/time violations by up to 77%. these results demonstrate that combining llmbased operator generation with category-theoretic verification creates a powerful synergy for reliable, flexible planning in constraint-intensive domains. llm-based planning. recent approaches leverage llms @xcite to generate plans directly from text @xcite @xcite , avoiding domain engineering. however, these models often act as black boxes that violate logical, temporal, or resource constraints @xcite . to improve robustness, several works have introduced search-augmented techniques: monte carlo tree search (mcts) @xcite , react @xcite , reflexion @xcite , llmfp @xcite , integrate dynamic programming @xcite , or feedback-driven strategies @xcite . these methods demonstrate the potential of combining search with neural heuristics and llm judge @xcite but still lacking structural correctness guarantees @xcite . reasoning-oriented llm frameworks parallel to direct plan generation, reasoning-oriented frameworks such as tree-of-thoughts @xcite , rewoo @xcite enhance reasoning depth and search efficiency by structuring llm outputs into treeor workflow-like processes. while effective for improving exploration, these methods also do not guarantee principled categorical verification when integrating multiple constraints across domains. neural-symbolic methods. neural-symbolic approaches @xcite aim to combine neural flexibility with symbolic pre-cision in domains such as visual reasoning (hudson and manning, 2019) and program synthesis @xcite . category theory provides powerful mathematical frameworks for compositional reasoning @xcite @xcite @xcite , though prior applications have largely focused on symbolic systems without deep integration of neural operator generation. our framework uniquely combines the generative capabilities of llms with category-theoretic verification to structurally enforce resource, temporal, and logical constraints. by embedding pullback-based validation into a bidirectional search framework, we bridge the gap between the flexibility of llm planners and the formal guarantees of symbolic reasoning. ## problem statement we formalize task planning as a category-theoretic framework where states are objects and operations are morphisms. each state @xmath0, s, l, t) encapsulates resources r, symbolic progress s, logical constraints l, and temporal allocations t. morphisms f : w 1 → w 2 represent valid state transitions that preserve resource bounds, state validity, constraint satisfaction, and temporal consistency. definition 3.1 (planning problem). given an initial state w 0 = (r 0 , s 0 , l 0 , t 0 ) and goal specification w * = (r * , s * , l * , t * ), find a sequence of morphisms in planning category t : a more formal problem statement can be found in appendix a. ## theoretical analysis in this section, we analyze the formal properties of the category-theoretic verification framework. we establish three key guarantees: local reachability, global completeness, and probabilistic completeness. together, these theorems ensure that our approach preserves the rigor of symbolic planning while leveraging the generative flexibility of llms. crucially, they highlight our main contribution: by embedding category-theoretic constructs (in particular, pullback-based verification) into an llm-driven planner, we can provide structural guarantees that are missing from existing heuristic or black-box approaches. ## methodology we now turn to our neural-symbolic task planning framework, which combines llm-based operator generation, pullback-based verification, and bidirectional search to generate valid plans (figure 1 ). ## experiments we evaluate our approach on three datasets with diverse planning characteristics: planbench (goaloriented planning), recipenlg (resource and temporal constraints), and proc2pddl (formal planning with precondition/effect validation). ## conclusion we introduced a neural-symbolic task planning framework integrating llm-based decomposition with category-theoretic verification for resourceaware planning. by modeling states as categorical objects and operations as morphisms, our approach ensures constraint satisfaction through pullbacks while using bidirectional search for computational efficiency. experiments across three domains demonstrate significant improvements over existing methods for completion rate and violation reduction. our results establish category-theoretic verification as a promising approach for neuralsymbolic planning in resource-constrained tasks.