Abstract
A recent approach to neurosymbolic reasoning is to explicitly combine thestrengths of large language models (LLMs) and symbolic solvers to tacklecomplex reasoning tasks. However, current approaches face significantlimitations, including poor generalizability due to task-specific prompts,inefficiencies caused by the lack of separation between knowledge and queries,and restricted inferential capabilities. These shortcomings hinder theirscalability and applicability across diverse domains. In this paper, weintroduce VERUS-LM, a novel framework designed to address these challenges.VERUS-LM employs a generic prompting mechanism, clearly separates domainknowledge from queries, and supports a wide range of different logicalreasoning tasks. This framework enhances adaptability, reduces computationalcost, and allows for richer forms of reasoning, such as optimization andconstraint satisfaction. We show that our approach succeeds in diversereasoning on a novel dataset, markedly outperforming LLMs. Additionally, oursystem achieves competitive results on common reasoning benchmarks whencompared to other state-of-the-art approaches, and significantly surpasses themon the difficult AR-LSAT dataset. By pushing the boundaries of hybridreasoning, VERUS-LM represents a significant step towards more versatileneurosymbolic AI systems