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

TL;DR

This paper introduces Neurosymbolic Transition Systems, a new principled computational model for building more reliable and scalable neurosymbolic reasoning tools by better integrating neural networks with symbolic logic.

Contribution

It proposes a formal model that combines symbolic states with neural intuition, providing a foundation for improved neurosymbolic reasoning systems.

Findings

The model can scale logical reasoning beyond current methods.

It retains the guarantees of traditional symbolic algorithms.

It offers a pathway to reify neurosymbolic reasoning in logic programming.

Abstract

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.