提出新框架让大模型与逻辑推理协同，突破现有工具的随意性限制
Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc -- and We Can Do Better
- 用符号状态与直觉并行的过渡系统构建神经符号推理架构
- 支持可扩展的逻辑推理，同时保持传统符号算法的可靠性保证
- 适合构建可信自动化推理工具的研究者与工程团队
当前利用大语言模型（LLMs）和传统符号算法构建自动化推理（AR）工具的方法缺乏系统性，既无法提供传统符号算法的严格保障，也未能实现神经网络与符号推理的深度协同。本文提出神经符号转换系统（Neurosymbolic Transition Systems），作为构建神经符号推理工具的基础计算模型。该模型将符号状态与直觉并行处理，状态转移同时作用于符号与直觉。论证表明，这一新范式可在保留符号算法强保障的同时，显著拓展逻辑推理能力，并可在未来通过逻辑编程语言实现具体化。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。