In this paper, we build from the preliminary work in [1] on using deep learning architectures to control inferential glut in a logical reasoning agent. Inferential glut is the well-known problem that symbolic reasoners encounter combinatorial explosions in the numbers of formulae they have to process. In [1] we proposed a neural architecture that employed a simple deep-reinforcement-learning network to prioritize potential inferences and control glut. This architecture was able to successfully control pre-inferential glut (inferential glut arising from ineficiencies in the reasoner's algorithm) and a limited form of inferential glut (that didn't use state). Work on this architecture continues; in this work we explore the use of Decision Transformers [2] as a replacement for the original deep reinforcement learning model. The decision transformer models reinforcement learning as a sequence modelling problem - specifically it employs transformers to generate the action likely to lead to a given return given the trajectory of (states, actions, returns) seen so far. In [2], the authors showed that using a pre-trained and ifne-tuned transformer (such a GPT2) can lead to near state-of-the-art on ofline reinforcement learning tasks. Since glut control as envisioned is largely a matter of selectively attending to the most promising avenues of reasoning, the attention-based mechanisms which underwrite transformers seem a natural fit for our application. In this paper we will explore the efectiveness of using a ifne-tuned GPT3 model [3] to predict salient actions as a proof-of-concept.
Our architecture is based on Perlis’ Active Logic reasoning engine ALMA [
Then location(a) can be used in conjunction with any one of these to derive location(left(a)) or location(right(a)), So to reach the next timestep, the active logic machine might apply a single deduction and add location(right(a)) to its knowledge base1.
For simplicity, in this preliminary study we restrict our attention to reasoning the proceeds
completely by way of applications of the resolution inference rule. See Section 9.5 of [
While resolution is a complete inference rule it is also particularly prone to producing glut as we shall see. We will focus our attention in this paper on the set of axioms . Although simple, this set of axioms provides for a meaningful study of glut-control for a few reasons, which we will examine in turn.
In Figure 1, we have given a short transcript of the first few steps of ALMA’s reasoning with using resolution. The extremely rapid growth of the knowledge base is immediately apparent.
1It is worth noting that this behavior is somewhat diferent from the traditional behavior of ALMA, where a step would refer to applying all such options a single time; thus at time 1 we would derive left(a), right(a) but not, e.g., left(right(a)). of Θ( ) in steps of reasoning. − We also note that this growth has two sources – a growth in literals that comes from repeated application of rules 2 and 3 of joined with rule 1 and a growth in universal formulae that comes from applying resolution to pairs of universal formulae. The latter type of formulae will be produced by resolution but not by forward chaining. These formulae also give a mechanism for growing the lengths of the potential consequents very rapidly. Indeed, in our study we will explore a reward structure that is based on the number of right functions applied to an instance of a; for example location(right(right(left(a)))) will have a reward of 2. The continual creation of these universal formulae will allow us to get more highly rewarded literals in the knowledge base rapidly, but some care is needed. By themselves, these rules do not produce any reward at all because the new formula are not instantiated. So an optimal strategy for an agent reasoning for steps will be to create the longest possible universal rules for 1 steps and then instantiate the longest such rule at the final reasoning step. This requires that an agent know how many steps it will reason for and how many it has already reasoned for – in particular it will need to keep track of a state. This in contrast to a forward-chaining based agent, whose optimal policy will be to repeatedly employ rule 2 from to get a reward
It is important to note that the growth of sentences from is so rapid that glut control becomes absolutely necessary – our workstation with over 300Gb of memory crashed after a few steps without it. Indeed, we conjecture that the growth in the number of sentences in the knowledge base is doubly exponential with Θ(2 2 ) sentences in the knowledge base after steps of (classical) ALMA reasoning.
Our glut-control architecture relies crucially on identifying, at each time-step, the set of potential
inferences that can be applied and viewing these as actions. By a potential inference we mean
a pair of formulae which the system believes it can use in the resolution rule to create new
knowledge. A list of these is stored in an internal ALMA data-structure; in [
In this preliminary study, we are specifically interested in using an autoregressive language
generation model (such as one of the GPT models) to determine the best action. Specifically,
we are interested in testing the viability of the Decision Transformer [
In our particular case, our states will correspond to the current content of the knowledge
base, actions will correspond to potential inferences and returns will be based on the reward
function mentioned above which counts the number of right functions in location instantiated
with a. As an initial test, we represented each triple as text and fine-tuned OpenAI’s GPT-3
model using their available tools [
We represented 4000 such trajectories, each randomly generated with 6 reasoning steps and the same initial knowledge base. These representations were then used as a dataset for ifne-tuning GPT3 (using an empty string as prompt and the representation as the completion). This was close to the maximum number of trajectories allowable by the default parameters set by OpenAI; this dataset was then used to fine-tune a “curie” model of GPT3.
To test our preliminary system, we entered the prompt [<6====l(a); l(X) –> l(f(X)); l(X) –> l(g(X)); now(0):::: and asked GPT3 for a completion. Based on our syntax, this is essentially asking for an inference to take that will result in a return of 6 based on the initial knowledge base. We set the temperature to 0 and the response length to 1900 tokens, using )>] as a stop sequence. The beginning of the provided completion is l(X) --> l(f(X)); l(X) --> l(g(X))>. This indicates that the fine-tuned model has learned the syntax of our representation and selected a valid action – the pair of sentences is in the knowledge base and will resolve to give a new sentence l(X) --> l(g(f(X))). Further, the next part of the completion (with added whitespace) given is <6==== l(a); l(X) --> l(f(X)); l(X) --> l(g(X)); now(1); l(X) --> l(g(f(X))):::: l(X) --> l(g(f(X))); l(X) --> l(f(X))>|||||| this further shows that the model is capable of computing the correct returns since the inference selected will not lead to any immediate reward.
Subsequently, the model chooses • l(X) --> l(f(g(f(X)))); l(X) --> l(g(X)) leading to l(X) --> l(g(f(g(f(X))))); • l(a); l(X) --> l(g(f(g(f(X))))) leading to l(g(f(g(f(a))))) and a reward of 2; • l(g(f(g(f(a))))); l(X) --> l(g(f(g(f(X))))) leading to l(g(f(g(f(g(f(g(f(a))))))))) and a reward of 4
It is noteworthy that each choice the model makes is valid and that the correct returns and logical consequences are modelled. Importantly, this particular sequence does not appear in the training set, so the model has not simply memorized a solution. The overall robustness of this learned model will be a subject of future analysis.
As a final test, we note that the trajectory in the training set with the highest return has a return of 21. Can our model beat this and get a return of 22 in 6 moves? The model makes the following choices: • l(a); l(X) --> l(g(X)) leading to l(g(a)) and a predicted return of 22 • l(g(a)); l(X) --> l(f(X)) leading to l(f(g(a))) and a predicted return of 21 • l(f(g(a))); l(X) --> l(f(X)) leading to l(f(f(g(a)))) and a predicted return of 19 • l(f(f(g(a)))); l(X) --> l(f(X)) leading to l(f(f(f(g(a))))) and a predicted return of 16 • l(f(f(f(g(a))))); l(X) --> l(f(X))> leading to l(f(f(f(f(g(a)))))) and a predicted return of 12 • l(f(f(f(f(g(a)))))); l(X) --> l(f(X)) (the final element could not be completed because of the token limit) We note that: • The model wastes the first move by adding a g to get g(a). • The model employs the same rule every step, which is the same rule that a greedy policy would use. • The models returns are significantly of in many cases; if we take the decrease in returns as an estimate of the reward for each action.
Overall, our simple test shows promise but also a great deal of room for improvement. We emphasize that our preliminary investigation only trained on a relatively small model (“curie”) and with a small amount of data (4000 trajectories). This already shows a limited ability to correctly model returns and actions in our scenario. Notably, every action picked was viable; the syntactic structure of every completion was correct; and we have found no instances in which the model made a mistake about what new sentence would be entered into the knowledge base as a result of choosing a particular action (that is, it has learned the syntactic structure of resolution).
Further work will expand to larger models, both by using OpenAI’s “davinci” model with larger training sets and by fine-tuning open source large language models from HuggingFace. We will also explore training GPT models from scratch to try to measure the degree to which our model is exploiting the general modelling capacities of the pre-trained networks.