A Principled Programming Model for Constructing LLM-Powered Reasoning Tools

Speaker

Dr. Aaron Bembenek, Research Fellow, the University of Melbourne

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.

Bio

Dr. Aaron Bembenek is a Research Fellow in the University of Melbourne’s School of Computing and Information Systems, currently working with Prof. Toby Murray on using automated reasoning to ensure software security. He earned a PhD in programming languages from Harvard University in 2023 under the guidance of Prof. Stephen Chong. In July 2026, he will start a McKenzie Fellowship (at the University of Melbourne) in neurosymbolic AI.