On LLM-generated Logic Programs and their Inference Execution Methods

TL;DR

This paper explores techniques to extract and execute logic programs from Large Language Models, enabling sound reasoning and verification of LLM outputs through novel execution methods like soft-unification and GPU acceleration.

Contribution

It introduces new methods for eliciting logic programs from LLMs and executing them efficiently, including soft-unification and GPU-based minimal model computation.

Findings

Effective extraction of propositional and relational logic from LLMs

Development of soft-unification for reasoning with LLM-generated facts

GPU acceleration significantly speeds up inference with large logic programs

Abstract

Large Language Models (LLMs) trained on petabytes of data are highly compressed repositories of a significant proportion of the knowledge accumulated and distilled so far. In this paper we study techniques to elicit this knowledge in the form of several classes of logic programs, including propositional Horn clauses, Dual Horn clauses, relational triplets and Definite Clause Grammars. Exposing this knowledge as logic programs enables sound reasoning methods that can verify alignment of LLM outputs to their intended uses and extend their inference capabilities. We study new execution methods for the generated programs, including soft-unification of abducible facts against LLM-generated content stored in a vector database as well as GPU-based acceleration of minimal model computation that supports inference with large LLM-generated programs.