Although Large Language Models (LLMs) have demonstrated impressive formal reasoning abilities, they often break down when problems require complex proof planning. One promising approach for improving LLM reasoning abilities involves translating problems into formal logic and using a logic solver. Although off-the-shelf logic solvers are in principle substantially more efficient than LLMs at logical reasoning, they assume that all relevant facts are provided in a question and are unable to deal with missing commonsense relations. In this work, we propose a novel method that uses feedback from the logic solver to augment a logic problem with commonsense relations provided by the LLM, in an iterative manner. This involves a search procedure through potential commonsense assumptions to maximize the chance of finding useful facts while keeping cost tractable. On a collection of pure-logical reasoning datasets, from which some commonsense information has been removed, our method consistently achieves considerable improvements over existing techniques, demonstrating the value in balancing neural and symbolic elements when working in human contexts.

翻译：尽管大型语言模型（LLMs）已展现出令人印象深刻的正式推理能力，但在需要复杂证明规划的问题上它们往往失效。一种改进LLM推理能力的有前景方法是将问题转化为形式逻辑并使用逻辑求解器。尽管现成的逻辑求解器在原则上比LLMs在逻辑推理方面效率更高，但它们假设所有相关事实都已包含在问题中，无法处理缺失的常识关系。在本工作中，我们提出了一种新颖方法，该方法利用逻辑求解器的反馈，以迭代方式通过LLM提供的常识关系来增强逻辑问题。这涉及通过搜索潜在的常识假设来最大化发现有用事实的机会，同时保持计算成本可控。在一系列纯逻辑推理数据集上（其中部分常识信息已被移除），我们的方法始终比现有技术取得显著改进，证明了在人类语境中工作时平衡神经与符号元素的价值。