A recent approach to neurosymbolic reasoning is to explicitly combine the strengths of large language models (LLMs) and symbolic solvers to tackle complex reasoning tasks. However, current approaches face significant limitations, 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 their scalability and applicability across diverse domains. In this paper, we introduce VERUS-LM, a novel framework designed to address these challenges. VERUS-LM employs a generic prompting mechanism, clearly separates domain knowledge from queries, and supports a wide range of different logical reasoning tasks. This framework enhances adaptability, reduces computational cost, and allows for richer forms of reasoning, such as optimization and constraint satisfaction. We show that our approach succeeds in diverse reasoning on a novel dataset, markedly outperforming LLMs. Additionally, our system achieves competitive results on common reasoning benchmarks when compared to similar state-of-the-art approaches, and significantly surpasses them on the difficult AR-LSAT dataset. By pushing the boundaries of hybrid reasoning, VERUS-LM represents a significant step towards more versatile neurosymbolic AI systems.

翻译：近期，一种实现神经符号推理的方法是显式结合大语言模型（LLMs）与符号求解器的优势，以应对复杂的推理任务。然而，现有方法面临显著局限，包括因任务特定提示导致的泛化能力差、知识与查询未分离造成的效率低下，以及推理能力受限。这些缺陷阻碍了其在多样化领域的可扩展性与适用性。本文中，我们介绍了VERUS-LM，一个旨在应对这些挑战的新型框架。VERUS-LM采用通用提示机制，清晰地将领域知识与查询分离，并支持广泛的逻辑推理任务。该框架增强了适应性，降低了计算成本，并允许进行更丰富的推理形式，如优化与约束满足。我们证明，我们的方法在一个新颖的数据集上成功实现了多样化推理，显著优于大语言模型。此外，与同类先进方法相比，我们的系统在常见推理基准测试中取得了有竞争力的结果，并在困难的AR-LSAT数据集上显著超越了它们。通过拓展混合推理的边界，VERUS-LM代表了迈向更通用神经符号人工智能系统的重要一步。