Certified Deductive Reasoning with Language Models

Thank you for the review and the encouraging comments! We provide clarifications on the approach and other questions below, and are happy to discuss any of these further.

What is the interface between the LLM and Peano? (What is the input of each and what is the output?

We're happy to expand on the explanation in Section 3.1 (we'll update the Appendix with pseudocode based on the description below and the discussion here). Essentially, three components that are tightly integrated: the LLM decoding algorithm, LogicGuide, and Peano. The LLM decoding algorithm will output token by token while constraining the output for the next token to come from a subset of the vocabulary determined by LogicGuide. Outside of a guided block (delimited by "[[" and "]]"), there are no constraints on which token can be emitted. When the model opens a guided block with "[[", LogicGuide first constrains it to output one of the LogicGuide actions followed by a colon. In the cases where the model outputs the "infer" action, LogicGuide calls Peano to determine which inferences are valid at this point. Peano will take as input all the formalized premises and previous inferences, which are extracted from the LLM's output so far, and output a list of valid one-step inferences. LogicGuide will take this list and compute token constraints for the LLM decoding algorithm so that its output, even over multiple tokens, will come from this list. Thus, looking at Figure 2, all three components are tightly connected to produce the output. The input here for the model is just the Context and Question. The model then starts to write its "Formalized context", then the goal, and finally the reasoning and answer. Every time the model opens a block with "[[", LogicGuide is called to determine constraints. In particular, in the [[infer]] blocks, LogicGuide calls Peano to determine valid inferences.

In general, applying such constraints is non-trivial because LLM tokens can break up these sequences (such as "[[", where the brackets might be split up in separate BPE tokens depending on the surrounding context). These complications are handled by CSD, which we use for decoding with constraints.

Does Peano have any knowledge built-in (e.g., axioms for deontic logic)?

In our experiments, we initialized Peano with an empty theory in PrOntoQA, ProofWriter and DeontiQA -- the relevant axioms are formalized by the LLM in-context. However, it might also be interesting for future work to explore scenarios where some background knowledge is given to the language model implicitly through the theory used to initialize Peano.

What is an example application beyond artificial logic puzzles? (The legal reasoning is a good example, but it only used the theorem prover for bootstrapping.)

The framework of guides can generally serve to explore connecting formal systems with LLM reasoning, besides the examples we provided. Many other important fragments of reasoning have been formalized into different logics - temporal logic (e.g., for reasoning about events), modal logic (e.g., connected to theory of mind reasoning), deontic logic (e.g., permissions, obligations), and so on. We provide a starting point for these, since these logics can be formalized in Peano and thus used to guide LLMs.

What does "bias the logits" mean? How is it done? How does the theorem prover determine how to bias them?

The output layer of the Transformer will predict unnormalized weights (logits) for each token in its vocabulary at each iteration. These logits are passed through a softmax to then become a probability distribution for sampling. When doing constrained decoding, such as in CSD, we want to "select" a subset of the tokens that will be allowed for sampling the next token. In some APIs like the OpenAI API, there is no option for directly selecting vocabulary tokens, but there is a way to add a "logit bias" - a weight that will be added before softmax to the output logit of the given vocabulary tokens. A sufficiently large negative bias effectively sets the probability for that token to zero. This trick, which was used in the CSD paper [1], is how we effectively constrain the OpenAI LLMs to valid completions. We use the same trick with LLaMA offline.

(My rating assumes there is a satisfactory answer to these questions. I will downgrade my rating if I still cannot understand the interface after the rebuttal period.)

That is fair – we will be happy to answer further questions or try to explain in different ways! Let us know what would be most helpful.

[1] Poesia, G., Polozov, O., Le, V., Tiwari, A., Soares, G., Meek, C., & Gulwani, S. Synchromesh: Reliable code generation from pre-trained language models. ICLR 2022

Thank you for the thoughtful comments on our work! We address the questions below, and are happy to engage further.

While the results on the ReClor dataset are quite encouraging, I find them quite surprising as well for multiple reasons. 1- Given that the model is finetuned only on 120 samples, and considering the size of the models used, I would expect that the models should just overfit to those examples without any task transfer. 2- If I understand correctly, the finetuning is not on a mixture of the original data and the 120 data points, so I would expect that the model's general task solving ability should go down. 3- The ProofWriter and PrOntoQA datasets only require deductively applying the modus ponens rule, whereas the ReClor dataset requires more complicated rules and reasoning. For these reasons, I found the improvements a bit surprising and the provided explanation does not give much insights.

Thank you for the question -- we will update the paper with a better discussion of the transfer results, which is indeed needed. Although we have few public technical details on the GPT-3.5 fine-tuning internals, the fine-tuning method is most likely a low-rank adaptation (like LoRA [1], which we used for our experiments on LLama), so the parameters of the base model are likely unchanged. Instead, a small number of parameters is learned on top of the model to adjust its behavior to the new examples. In general, parameter-efficient fine-tuning methods like LoRA tend to not overfit as easily or degenerate the model's behavior because they operate with relatively low capacity. This is also why we don't need many examples for fine-tuning (the OpenAI documentation recommends starting with an even smaller number, like 50, and iterating from there, which corroborates this). Our understanding is that low-rank fine-tuning is not necessarily "teaching the model completely new skills" (such as inference patterns unseen during pre-training), but rather reinforcing skills that were already present in the training data, at the expense of less relevant ones for the task. In turn, fitting higher-quality examples yields better results.

On which categories from Table 2 of the BoardgameQA paper do you expect your approach to fail/succeed? And why?

LogicGuide can in principle be applied to all of those types of rules and comparisons, except Ortography (since Peano does not currently have a representation for strings as sequences of characters). For problems where there are missing assumptions, we can ask the model to formally state those for use in inference. We previously ran a preliminary experiment with this using PrOntoQA False (where the rules violate world knowledge), where instead of giving the model the premises and asking it to reason with them, we gave it the reasoning trace, without any premises, and asked it to first formalize assumptions that would enable the argument to work, and only then proceed with the formal argument. We found few-shot prompting for completing with the assumptions to be effective, and we believe a version of this could also work for the kinds of gaps that happen in BoardgameQA, where the model also needs to identify and complete missing assumptions in the problem (e.g., that "every dog is a mammal" to connect "sam is a dog" and "every mammal …"). We are running a scaled up version of this experiment and will update the paper with results on it soon (and let you know here as well).

Given that the results in Table 6 are tested in a zero-shot setting, how do you extract the final answer? Is it possible that after finetuning on the 120 examples, the model mainly just learns to produce outputs in the specified format making it easier to extract the final answer (and hence higher predictive accuracy)?

In the zero-shot setting, we prompted GPT-3.5 Turbo with an explanation of both the task and the desired output format, and we did allow for some deviation by looking at the outputs of the base model and matching extra patterns. We observed that the original model before our fine tuning did follow the desired format, and only deviated from it in a few predictable ways (e.g., instead of saying just "Answer: A" as we asked, it would often say "Answer: A - <<option text here>>"). We note that the fine-tuned model was still subject to these variations because the format of ReClor was not exactly the one during training (e.g., here there were several options for the answers, while the training examples were just true/false).

Thank you again for the attentive review! Please let us know if we can clarify further. We'll update you here once we have the results on the experiments with missing assumptions.

[1] HU, Edward J. et al. LoRA: Low-Rank Adaptation of Large Language Models. ICLR 2022

Informal argument (given): Wren is an animal. Wren is a feline. Wren is a sheep. Wren is a mammal. Wren is a vertebrate. Wren is luminous.
(model):
Implicit premises: All animals are felines [[axiom:(animal 'x) -> (feline 'x)]]. Felines are sheep [[axiom:(feline 'x) -> (sheep 'x)]]. Sheep are mammals [[axiom:(sheep 'x) -> (mammal 'x)]]. Mammals are vertebrates [[axiom:(mammal 'x) -> (vertebrate 'x)]]. Vertebrates are luminous [[axiom:(vertebrate 'x) -> (luminous 'x)]].
Formalized argument: Wren is an animal [[axiom:(animal wren)]]. Wren is a feline [[infer:(feline wren)]]. Wren is a sheep [[infer:(sheep wren)]]. Wren is a mammal [[infer:(mammal wren)]]. Wren is a vertebrate [[infer:(vertebrate wren)]]. Wren is luminous [[infer:(luminous wren)]].

We thank the reviewer for the thoughtful comments, and the encouraging remark that the approach is "versatile across a range of reasoning scenarios"! We respond to the questions and concerns below, and are happy to discuss these further.

The proposed method necessitates a reliance on a complex formalization process during training and inference.

While this is true for problems that can be adequately formalized, our results (Section 4.4) show that bootstrapping GPT-3.5 Turbo on such problems, where formalization helps during training, can also improve reasoning when not formalizing at inference time.

In more generalized contexts, it might be challenging to formalize and identify corresponding actions, such as objects, relations, etc.

We agree that this can be hard in more naturalistic problems. Our experiments in Section 4.4 show that bootstrapping on simpler problems can still help even when not formalizing at inference time.

Overlap with prior work on the Peano theorem and the constrained Semantic Decoding algorithm

Our framework of guides is a novel interface between these components. Peano itself is simply a formal theorem proving environment, with no natural language component. Moreover, while Constrained Semantic Decoding was originally used in cases where the entire output is constrained, our framework of guides generalizes this to allow the model to selectively turn the guide tool (and therefore the constraints) on and off during generation. Thus, we build on these prior works but ultimately implement new capabilities.

It seems the proposed idea is similar to the idea in Logic-LM.

Thank you for the reference. We'll add it to our Related Work section. In summary, works like Logic-LM use the LLM to parse the problem, and then offload reasoning entirely to an external engine. Thus, the model does not produce a reasoning trace in natural language (a "chain-of-thought"), since reasoning is carried out by the external tool (note that none of the tools used in Logic-LM produce such a trace either). In our work, Peano is only used to limit what inferences the model itself can do, but ultimately the LLM is still the reasoner, and still produces a chain-of-thought. We need these reasoning traces to fine-tune the model itself in a self-improvement fashion (which we show in Sections 4.3 and 4.4).

How likely that encountering a formalization failure may happen, and are there strategies in place to minimize formalization errors?

It varies from model to model - the OpenAI models were fairly good at formalization in our experiments, whereas LLaMA lagged behind. For the formalization blocks, LogicGuide still imposes constraints on well-formedness during generation to minimize errors. Namely, the constraints guarantee that the model will output expressions that are syntactically valid and coherent with its own proposition and object annotations, thus avoiding errors due to such inconsistencies. These constraints were triggered in around 5-10% of the cases depending on the dataset for text-davinci-003 and gpt-3.5-turbo, where otherwise there would have been formalization errors. We are running a more in-depth analysis on this and will add it to the paper soon.

To what extent does using constrained generation reduce the reasoning space, so as to mitigate the issue of "logical inferences made next can have a potentially large set of answers"? Is it possible that still there may be a considerably large set of answers, if so, how does your method decide on the the most appropriate content to generate next?

The number of possible valid inferences for the datasets we used were in the order of dozens in the worst case. In these cases, the language model is constrained to generate from that set when it opens an [[infer]] block, and uses its own log-probabilities to decide what is most appropriate in the current context / solution. Thus, we allow the model to choose its logical inferences while constraining it to logically sound ones. Allowing the language model to decide amongst logically valid continuations is unique to our guide approach.

In scenarios challenging to formalize, what amount of preparatory work, such as the number of samples of formalizable tasks, is essential to ensure the model with strengthened generalization inference capabilities?

This is a good question. In general, we cannot strictly guarantee that positive transfer will happen between the training and inference tasks. However, using low-rank fine-tuning methods [1], we observe that even a few hundred high-quality training examples can improve reasoning performance. In turn, the guided models are able to produce higher quality training examples for this purpose, as our results show.

Please let us know if we have clarified your concerns. We're happy to discuss these further or provide more information!

[1] HU, Edward J. et al. LoRA: Low-Rank Adaptation of Large Language Models. ICLR 2022

(...) If something is [[prop:rough]] and [[prop:furry]] then it is [[prop:young]]. [[axiom:((rough 'x) -> (furry 'x)) -> (young 'x))]]