标题： 当前构建LLM驱动的推理工具的做法是随意的——我们可以做得更好 显示英文标题

标题： Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc -- and We Can Do Better

摘要： 对结合传统符号算法和大型语言模型（LLMs）来构建软件验证器、合成器和其他自动化推理（AR）工具的兴趣正在增长。 不幸的是，目前构建这种神经符号AR系统的做法是一种随意的编程模型，它既没有传统符号算法的强保证，也没有足够深入的神经网络和符号推理同步，以释放LLM驱动推理的全部潜力。 我提出神经符号转换系统作为一种有原则的计算模型，可以作为构建神经符号AR工具的基础架构。 在这个模型中，符号状态与直觉配对，状态转换并行地在符号和直觉上操作。 我论证了为什么这个新范式可以在保持符号算法强保证的同时，将逻辑推理扩展到当前能力之外，并简要描述了我提出的计算模型如何在逻辑编程语言中实现。 显示英文摘要

摘要： There is growing excitement about building software verifiers, synthesizers, and other Automated Reasoning (AR) tools by combining traditional symbolic algorithms and Large Language Models (LLMs). Unfortunately, the current practice for constructing such neurosymbolic AR systems is an ad hoc programming model that does not have the strong guarantees of traditional symbolic algorithms, nor a deep enough synchronization of neural networks and symbolic reasoning to unlock the full potential of LLM-powered reasoning. I propose Neurosymbolic Transition Systems as a principled computational model that can underlie infrastructure for building neurosymbolic AR tools. In this model, symbolic state is paired with intuition, and state transitions operate over symbols and intuition in parallel. I argue why this new paradigm can scale logical reasoning beyond current capabilities while retaining the strong guarantees of symbolic algorithms, and I sketch out how the computational model I propose can be reified in a logic programming language.