Certified Deductive Reasoning with Language Models
Authors: Gabriel Poesia
Kanishk Gandhi
Eric Zelikman
Noah Goodman
Venue: Accepted by TMLR ()

Abstract: Language models often achieve higher accuracy when reasoning step-by-step in complex tasks. However, even when arriving at a correct final answer, their rationales are often logically unsound or inconsistent. This is a major issue when reliable reasoning traces are needed,
such as when fine-tuning on model-generated reasoning for self-improvement. To tackle these issues, we introduce a class of tools for language models called guides, that use state and incremental constraints to guide generation. A guide can be invoked by the model to constrain its own generation to a set of valid statements given by the tool. In turn, the model’s choices can change the guide’s state. We show how a general system for logical reasoning can be used as a guide, which we call LogicGuide. Given a reasoning problem in natural language, a model can formalize its assumptions for LogicGuide and guarantee that its step-by-step reasoning is sound. In experiments on PrOntoQA, ProofWriter and Syllogism Validity datasets, LogicGuide significantly improves the performance of GPT-3, GPT-3.5 Turbo and LLaMA (accuracy gains up to 35%), while drastically reducing content effects — the interference between unwanted prior assumptions and reasoning, which humans and language models suffer from. We then explore bootstrapping GPT-3.5 Turbo and LLaMA using their own reasoning traces. We find that LogicGuide is critical: by training only on certified self-generated reasoning, models can self-improve, avoiding learning from their own hallucinations. Moreover, bootstrapped models enjoy significant boosts on ReClor, a challenging real-world reasoning dataset, even when not relying on formalization at inference time.

Published in Transactions on Machine Learning Research (05/2024)
Certified Deductive Reasoning with Language Models
Gabriel Poesia, Kanishk Gandhi", Eric Zelikman", Noah D. Goodman
Stanford University
(poesia, kanishkg, wwelikman, wtg.llmmm..goommm/eaaafrorr.....
Reviewed on OpenReview:
Abstract
Language models often achieve higher accuracy when reasoning step-by-step in complex tasks. However, even when arriving at a correct final answer, their rationales are often logically unsound or inconsistent. This is a major issue when reliable reasoning traces are needed, such as when fine-tuning on model-generated reasoning for self-improvemett. To tackle these issues, introduce class of tools for language models called guides, that use state and incremental constraints to guide generation. A guide can be invoked by the model to constrain its own generation to a set of valid statements given by the tool. In turn, the model's choices can change the guide's state. We show how a general system for logical reasoning can be used as a guide, which we call LOGICGUIDE. Given a reasoning problem natural language, a model can formalize its assumptions for LOGIGGUIDE and guarantee that its step-by-step reasoning sound. In experiments on PrOntoQA, ProofWriter and Syllogism Validity datasets, LOGICGUIDE significantly improves the performance of GPT-3, GPT-3.5 Turbo and LLaMA (accuracy gains up 35%), while drastically reducing content effects the interference between unwanted prior assumptions and reasoning, which humans and language models sulfer from. We then explore bootstrapping GPT-3.5 Turbo and LLaMA using their own reasoning traces. We find that LogicGuide is critical: by training only on certified self- generated reasoning, models can self-improve, avoiding learning from their own hallucinations. Moreover, bootstrapped models enjoy significant boosts on ReClor, a challenging real-world reasoning dataset, even when not relying on formalization inference time.
1 Introduction
Consider langunge-based autonomous agent tasked with managing user's calendar and email. The user might want to specify general principles how the agent should behave, such as "if the email is from any of my managers, you must send me notification", and important pieces of information such as "T'm part of the research team", or "Grace manages research". When the agent analyzes an email and decides what actions to take, we'd like to respect the given instructions. Doing so might require reasoning: the agent should conclude that an email from Grace warrants a notification, even if that wasn't said explicitly. How should the agent draw such conclusions?
A Large Language Model (LLM), such GPT-3 (Brown et al., 2020) PaLM (Chowdhery et al., 2022), can in principle take in the given instructions and context, choose actions to take and, before each action, ask itself "is this permitted?" The answer might require making chains of inferences based on the user's input. For this class of problems, LLMs have been shown to dramatically benefit. from chain-of-thought reasoning (Wei et al., 2022; Suzgun et al., 2022). Empirically, allowing LLMs to generate reasoning steps before their answer consistently yiclds higher accuracy across a wide range of tasks (Suzgun al., 2022). Qualitatively, reasoning steps are often seen as "an interpretable window" into how the model arrived at the answer (Wei al., 2022), in contrast to opaque guess.
1

---

Published in Transactions on Machine Learning Research (05/2024)
Language Model
jane
Jane is friend [aaiiom((rried jane)]]
infer:( lo pri max)
Jane is
Friends are high-priority [I..]] That means
high-pri alex)
jane)
high-priority person
r Tou
Ts FO
LogicGuide
Figure 1: A language model can invoke guide tool, such as our LOCICGUIDE, perform certifiable generations. Here, when the model decides to generate an infer block, it is constrained to generate one of the formal deductions established by an external theorem-proving environment.
But much like humans, language models can also produce unsound reasoning: even after correctly interpreting problem, they can take logically invalid inference steps, or produce a guess at the final answer that is not supported by their own rationale (Saparov & He, 2022). Moreover, LLMs have also been observed to show human-like like content effects in reasoning: their accuracy drops significantly when asked to reason with assumptions that contradict their prior beliefs (Dasgupta et al., 2022).
How can avoid unsound, perhaps dangerous, inferences? This question illustrates the central concern that led to the development of formal logic. Proof systems formally encode core patterns underlying valid reasoning, allowing sound inferences to be generated mechanically from deduction rules. If we arrive at an answer after series of formal deductions, we know that not only the conclusion is correct, but the reasoning that led to it was entirely valid. This is in contrast to a free-form rationale that can arrive at the correct. answer even through incorrect means.
To that end, we aim allow LLMs rely on trusted formal deductions during reasoning by building on the recent paradigm of tool use in language models (Cobbe et al., 2021; Schick et al., 2023). In prior work, LMs invoke external tools by generating special sequences, intercepted by the decoding algorithm. They generate inpuls (e.g., mathematical operalion, or search query) and receive the Lool's oulput as if it was their own generation. We generalize this input-output paradigm to a broader class of LM tools we call guides. When a guide is invoked by the model using a special delimiter, the tool computes a space of valid outputs, as illustrated Fig. 1. We then employ construined decoding (Poesia el al., 2022) to ensure the model will incrementally generate one of the valid outputs. Guides thus enable a more declarative interaction ween tool and model: the guide declares a set of possible sequences, while the model brings prior expectations used to generate sequence of choices up to that point.
among them. A guide maintain state: its next valid outputs might depend on the
We use this framework to allow LMs to locally constrain generation to a set of valid statements determined by an external tool. We leverage the Peano theorem ppovvengproving environment (Pocsia Goodman, 2022) to construct LOGICGUIDE, which an LM can use formalize assumptions, set proof goals, and make sound inferences step-by-step. The model can intersperse formal reasoning and natural language during generation. Language conditioned on previous formal steps is highly reliable since the generations allowed by LOGICGUIDE are formally certified.
We first validate our mothod on three logical reasoning datascts, PrOntoQA (Saparov & He, 2022), ProofWriter (Tafjord et. al., 2021), and Syllogistic Validity (Dasgupla el. al., 2022). We also follow the format and methodology of PrOntoQA to introduce a new dataset, DeontiQA, where problems require reasoning using dcontic logic principles to determine whether actions are permissible, obligatory or forbidden. When used with few-shot prompting, we find that LOGICGUIDE significantly improves the accuracy of OpenAI GPT-3 and GPT-3.5 Turbo, and LLaMA 13B. Moreover, models using LOGICGUIDE have drastically lower content.
2

---

it fine tunes Published in Transactions on Machine Learning Research (05/2024)
effects: show this both with PrOntoQA and in the Syllogism Validity dataset, used previously to measure content effects in LMs.
While for these problems we could leverage an external solver to obtain a final answer after the model produces a sufficient formalization, a key advantage of LOGICGUIDE is that the LM still generates a step-by-step rationale. This allows us to then apply self-improvement methods, such as the Self-Taught Reasoner (STaR; Zelikman et al. (2022)), which improves the model's own reasoning by fine-tuning on rationales that led to correct answers. In the tasks we analyze here, there's high probability of guessing the answer (e.g. true or false, so at least 50%). Hence, STaR alone fails to yield meaningful improvements, incorrect reasoning that does not generalize. In contrast, we show that running STaR using only certified solutions generated with LOCICGUIDE is highly effective: LLaMA 13B enjoys accuracy gains of up to 17% on PrOntoQA, while naïve STaR fails to improve the model.
Finally, we investigate whether bootstrapped models Iearn reasoning patterns that generalize beyond problems where full formalization is possible. We fine-tune GPT-3.5 Turbo on its own correct solutions for problems in PrOntoQA and ProofWriter and evaluate it on ReClor, challenging set of problems from real-world stan- dardized exams requiring reading comprehension and logical reasoning, as well as 6 tasks in the LENALBENCI dataset. Bootstrapped GPT-3.5 Turbo outperforms both the base model, and performs best when fine-tuned on its solutions generated with LOGICGUIDE. These results suggest a promising avenue for bootstrapping language models on logical reasoning.
2
Related Work
Our work builds on two elasses of systems for reasoning: language models, which can reason flexibly in natural language, and formal reasoning systems, which rely on formal logic to derived certified inferences. To interface these two systems, we leverage recent methods for constrained decoding from language models. Specifically, we employ Constrained Semantic Decoding (CSD, Poesia et al. (2022)), an algorithm that guarantees valid samples by construction. CSD does not require full access to the model, only the ability to bias its logits. This allows us to use GPTT3 and GPT-3.5 Turbo through their public APls, as well as LLaMA (Brown et al., 2020; Touvron et al., 2023). Other decoding methods, such as NouroLogic Decoding and NeuroLogic A *esque decoding (Lu et al., 2021; 2022), have been proposed to enforce lexical constraints at inference time.
LLMs have been increasingly used agents interacting with other systems, by both using tools to delegate compulation to trigger external actions (Schick el al., 2023; Yao el al., 2022; Yang el al., 2023; Hosseini-Asl et al., 2020; Shah et al., 2023). In prior work, LLMs can provide inputs to an external tool, such as search query (Schick et al., 2023) or a mathematical operation (Cobbe et al., 2021), and reccive the output in the decoding stream. Our framework of guides ($3) can be seen as a generalization of this paradigm, where the tool defines a space of outputs and the LM chooses one using its own probabilities.
Our approach to certifying reasoning from LMs relies grounding their inferences in interactive theorem prover, Peano (Poesia & Goodman, 2022). Similar to other popular theorem proving languages like Lean (de Moura et al., 2015) and Coq (Barras et al., 1997), Peano uses dependent type theory as its logical foundation. Most theorem proving environments are designed for the verification of given proofs. In contrast, and of special interest to us, Peano is designed to aid in generation by exposing a finite action space. Many other recent works have integrated LLMs and interactive theorem provers in the context of formal mathematical reasoning. Rocent work on autoformalization has shown that LLMs can be effective in translating informal to formal mathematics (Wu et al., 2022). This idea is related to how we use LLMs to formalize their assumptions given in natural language, though our end goal is to produce reliable natural language rationales rather than formal proofs.
Many prior works have broadly used neural networks for logical reasoning. One prominent line of work has focused on using neural networks to approximately execute logical reasoning on symbolic knowledge bases. This includes Neural Thcorem Provers (Rocktäschel & Riodel, 2017) and Conditional Thcorem Provers (Minervini al., 2020). Other approaches use encoders for allowing problem statements in natural language and perform reasoning in latent space, such as Alscouree-Aware Graph Networks (Huang et al., 2021). Unlike
3

---

Published in Transactions on Machine Learning Research (05/2024)
these, which learn to perform reasoning "in- "in-weights" via fine-tuning, our goal is to augment chain-of-thonght reasoning in language models, where all inputs, reasoning steps and outputs are realised in language.
3 Certified Reasoning with Guides
Previous work in tools for language models assumed an interface where the model provides inputs to the tool and receives back single output, conditioning this output for further generation. For instance, Cobbe et al. (2021) allowed the model to rely on calculator by generating string such as <51#12=. At this point, the decoding algorithm would execute the operation externally and copy the result as if it was generated by the language model. Here, we want to leverage a trusted reasoning tool to answer the question: "what logical inferences can be made next?" Unlike an arithmetic operation, this question (1) can have potentially large set of answers, and (2) can depend on previous choices made by the model. Thus, our key idea is to leverage constrained generalion to allow the model to implicitly choose one of the valid inferences during decoding, while remaining contained in those that are valid. However, while prior work constrained generation enforced constraints for the whole output, we want to allow the LM itself to locally enable constrained generation when performing certified reasoning steps, while being able to freely generate otherwise.
To operationalize this idea, a guide tool defines a set of valid generations given previous choices. Formally, let == be the set of strings in the guide's alphabet Σ, with S denoting the set of finite sequences of such strings. We define guide g to be a function g : S - P(S) that takes a sequence of previously generated strings and returns a regular set of allowed next generations. Our idea is to use g at specific points when sampling from a language model PLM(() so that when the guide is invoked at prefix 8o, will sample a contimuation from PLM(( (s (o) that belongs to the set allowed by g when given the previous guided generations in the prefix 80 (e.g,, previous valid logical inferences).
3.1 From guides to completion engines
Given any guide function g as above, we want to provide a tool for LMs that, once invoked by a special sequence, will constrain the immediate subsequent output using g. Let t, and tz be two arbitrary delimiters, such that t begins a guided block in the LM's generation, which is then closed by t2 (e.g., we later use t1 " "[[" and 12- "]]"). Intuitively, we would like to decode from PLM as follows: (1) we sample tokens until the model generates Lú; once that happens, we (2) use g along with the generation so far to obtain set of valid contimuations, then (3) trigger constrained generation to sample from that set, and finally (4) return to unconstrained generation once the model outputs t2. Unfortunately, tokenizers drastically complicate implementing this procodure, as different models often have different vocabularics (c.g., each of the models we leverage in $4 do), and LM tokens can be arbitrarily misaligned with 4 and l2. For example, the string " "[[" might be a single token, contained in a larger token, or be broken up across two tokens depending on the context and the vocabulary.
To overcome these issues and implement LM guides in a model-agnostic manner, we employ the Constrained Semantic Decoding algorithm (CSD; Poesia et al. (2022)). CSD effectively solves the vocabulary alignment problem by providing the abstraction of a "completion engine", which incrementally dictates valid generations by constructing local regular expressions. CSD samples from the LM while guaranteeing a valid output (i.e., one that respects the completion engine). While CSD enforces constraints for the entire LM generation, we operationalize the idea of allowing the LM to turn constraints on and off by creating a completion engine that (a) accepts any string that does not contain ti and is followed by t (i.e., free generation until a guided block starts), and then (b) only accepts what the guide g does, given the context far, followed by to (Le.. constrained generation until the end of the guided block). Alternating between these constraints allows the model lo intersperse guided and unguided generation, as in Fig. 2. We define our completion engine for guide tools in detail in the Appendix. Using our implementation, users can simply implement an arbitrary function 9 with the signature above and obtain a procedure to sample from any LM with the guide invoked when needed. This framework allows us to easily design rich, context-sensitive LM tools, such as the LOGICGUIDE. We describe several other guides in Appendix A, leaving their exploration to future work.
4

---

Published in Transactions on Machine Learning Research (05/2024)
Context: 1- The mouse visits the tiger. (...) 3- If something visits the tiger then it visits the mouse. (..) 12- If something visits the mouse then it is blue. (...)
Question: True false: The mouse is green?
Formalized context:
1- The [[objec:: mouse]] [[relation: visite]] the [[object: tigerl] [[axion: (visits mouse tiger)]] (...) something [[relation: visits]] the [[object: tiger]] then it [[relation: visits]] the [[object: nouse]] [[axion: (visits 'x tiger) >> (visits 'x nouse)]] (..) 12- something [[relation: visits]] the [[object: nouse]] then is [[prop: blue]] [[axiom: (visits mouse) (blue 'x)]] (...)
Formalized goal:
[[goal: (green nouse)
Reasoning:
mouse)]] The mouse visits itself. [[infer: (blue nouse) The mouse blue. [[infer: (green mouse]]] The mouse green. This satisfies the goal.
[[infer: (visits
Answer:
TRUE
using LOGICGUIDE in a problem from Proo/Writer. The model's generation starts at the "Formalized context". This example shows all 6 actions we implement in the LOGICGUIDE: object declares particular entity, prop and relation mark unary and binary predicates, respectively; axiom denotes propositions assumed to hold (possibly implications), goal sets target to be proven or contradicted, and infer marks deductions.
Figure Example solution of
3.2
The LogicGuide
We now construct LOGICGUDDE, guide tool for LMs to perform externally certified reasoning. Our logical backend of choice is Peano (Poesia & Goodman, 2022), a theorem-proving environment for incremental proof generation. The main feature of Peano we rely on is that provides a finite action space. Thus, given a partial argument, Peano gives us a list of valid inferences that can be made in a single step given the background theory, assumptions (possibly previously added by the model) and past inferences. We then use this list guide the LM when decides to formally derive logical conclusion. While Peano makes the guide implementation particularly simple, other theorem-proving environments may be adaptable for this purpose.
We use the delimiters " "[[" and "]]", and implement a guide function that accepts strings with the format action: acctionppraneee parameter. We define 6 actions (exemplified in Fig. 2) that allow the model to (1) formalize its assumptions (object, prop, relation, axiom), (2) set a goal (goal), and (3) perform logical inferences (infer). For (1) and (2), the guide returns constraints that ensure the model's formalization to be syntactically impossible to guarantee
valid. Since these actions are the boundary between natural and formal language, they are semantically valid in the sense that the model has properly interpreted the natural language context. What is certifiable is that the logical inferences (action type 3) follow from the model's formalization, i.e. its inference are valid given its explicit assunptions. ($4 provides empirical evidence that formalization errors rarely lead to wrong conclusion; most often they make the model unable to prove or disprove the goal).
Using the guide In the typical setup for logical reasoning problems (Tafjord al., 2021; Saparov & He, 2022), the input contains context (the set of assumptions) and a question (a goal that the logical argument must conclude or negate). In our experiments, examples with the proper LOGICGUiDE action annotations (as in Fig. 2). Specifically, we add section before the rationale named "Formalized context" where we repeat the assumptions in the scenario while marking objects, properties and relations, and formalizing each of the assumptions into an [[axiom:]] block. We do the same for the goal. Then, we prepend each reasoning step with the appropriate [[infer:]] action. this way the model encouraged first generate a formal inference step and only then its natural language counterpart. We include all of our prompts in the Appendix.
demonstrate how use the guide by creating few-shot
4 Experimental evaluation
We now evaluate the effectiveness of LOGIGGUIDE improving language models on reasoning tasks. (Our code and data are available at https://github. cotp http://gttbb...oogggsss////ettte arboesiaccotifiedrreaaaoo research questions: (RQ1) Does LOGICGUIDE improve the accuracy of language models in multi-step
We focus on four
5

---

Published in Transactions on Machine Learning Research (05/2024)
PrOntoQA False
PrOntoQA Fictional
1.0
Model
GPT-3 Davinci
Accuracy
0.8
GPT-3.5
LLaMA 138
LogicGuide?
0.6
No
Yes
0.4
PrOntoQA True
ProofWriter
1.0
Accuracy
0.8
0.6
0.4
3 # of hops
2
4
5
# of hops
Figure 3: Final answer accuracies with guided and unguided language models on PrOntoQA and ProofWriter, with bootstrapped 95% confidence intervals. We also show unguided GPT-4 accuracy for 5-hop splits.
reasoning? (RQ2) Does LOgiCGUIDE reduce content effects in language model reasoning? (RQ3) Can an LLM self-improve using LOGICGUidE by learning from its own solutions? (RQ4) Do bootstrapped models also improve in tasks where they cannot rely on LOCICGUIDE during inference?
4.1 Impact of LogicGuide in multi-step reasoning accuracy
Datasets We first use two recent natural language reasoning datasets: PrOntoQA (Saparov & He, 2022) and Proo/Writer (Tafjord al., 2021). Both datasets contain reasoning problems with (1) a list of assumptions (e.g. "Every dog is a mammal", or "Sam is a dog"), and (2) a proposition that can be reasoned about from the assumptions (e.g. "Sam is mammal?"). In both datasets, the goal to answer the question with either true false. Problems
categorized by how many reasoning "hops" the solution needs (1 to 5). In addition, PrOntoQA has three splits: "Truc Ontology", where the rules align with common sense, "False Ontology", where rules violate common sense (e.g., "Every composite number is prime"), and "Fictional Ontology", which uses made-up concept. (e.g., "Every wumpus is feisty."). ProofWriter uses real concepts for all rules (e.g,, people, animals, colors), but the rules are generated at random thus they also often contradict common sense. We use the problems from ProofWriter where the answer can be proved (i.c. ignoring the " "closod-world assumption" and "unknown" problems, where fully justifying the answer requires meta-logical reasoning).
Language models We evaluate three language models in the few-shot setting: OpenAl GPT-3 (text-davinci-003, Brown et al. (2020)), OpenAI GPT-3.5 Turbo 1.pt-3.5-turil and LLaMA 13B (Touvron et al., 2023). We use 4 few-shot examples for the vanilla models. For guided models, the prompt examples are augmented show formalized reasoning. In the prompt, we first show the model how to formalize the assumptions and the goal, and then present the chain-of-thoughh where natural language sentences preceded by guided inference (in an infer block, c.f. $3.2). Since this makes the prompt longer, we only use two prompt examples for the guided models: one where the answer is true and one where it is false. We implement CSD on the OpenAl models using their public API, which exposes parameter to bias the logits on given tokens (setting this bias to its maximum value on a set of tokens acts as a hard constraint to restrict the next token that subset). We use the rejection- sampling procodure described in Poesia al. (2022). gpt3.5-ture t-turbo requires slight adaptation (to resume generation after a constraint is applied) because of its chat-based APT; we detail this along with all of prompts in the Appendix.

---

Published in Transactions on Machine Learning Research (05/2024)
Results Fig. 3 shows few-shot results on multi-hop reasoning, measuring final-answer accuracy. Overall, guided models perform significantly better. GPT-3 and GPT-3.5 are highly accurate in formalizing assump- tions, and enjoy the largest benefits (with nearly perfect performance on PrOntoQA with LOCICGUIDE, and improving from chance to 80% correct on ProofWriter). For them, LOGICGUIDE essentially eliminates single-step reasoning errors, and the impact of this benefit grows solutions requiring more hops a single error enough to reach the wrong final conclusion. LLaMA 13B sees gains between 10 and 20% in PrOntoQA False and Fictional, while LOCICGUIDE hurts its performance in PrOntoQA True (where, effectively, reasoning is not necessary, only commonsense) and ProofWriter (where LLaMA is more often inconsistent in its formalization). We also include results for unguided GPT-4 in the 5-hop datasets, observing that our best guided models either match or exceed GPT-4 in all cases. Notably, GPT-4 also suffers from content effects in the PrOntoQA False ontologies (89% accuracy, while performing at ceiling on True ontologies), while guided text-davinci-O0 is near ceiling in both.
We observe two main failure modes: (1) models can misformalize assumptions, and (2) they can fail at planning, making a sequence of valid inferences that do not ultimately lead to the goal. When formalization ion errors happen, it's more common that no conclusion can be drawn, rather than wrong conclusion: in only 1.6% of the solutions did a guided model formally derive a wrong answer; these cases were mostly due to missing a negation when formalizing a sentence (mostly LLaMA on ProofWriter). A more common formalization failure (especially for I.aMA) was to use inconsistent properties or relations during formalization. For instance, in one case, LLaMA formalizes "the dog sees the cat" using a binary relation in one case (sees dog cat) and as a unary property - -aat dog) in another part of the same problem. This mismatch prevents using the first derived conclusion to fulfiil the hypotheses of the second inference rule. When further inferences can be made, LOGICGUIDE generates the string nothing in the [[infer]] block. When that happens, we observed models spontaneously concluding that the answer is "Unknown" or "Cannot be concluded" despite that not being demonstrated in the prompt (models abstained in 78% of the cases where they exhausted the inferences that could be made). This contrasts with the unguided models, which most often still make an unjustified guess, writing as if it was a logical conclusion (only unguided GPT-3.5 Turbo ever abstained, in 9% of its predictions). Being able to identify this difference crucial for applying rel--improvement methods, which mitigate both failure modes in LLaMA as we show in $4.3.
Impact of constraints for aiding formalization We nole that LLMs equipped with LOGICGUIDE always produce well-formed formal statements, since LOCICGUIDE constrains the LLM inside formalization blocks (such as [[axiom:]]) to output valid expressions. This contrasts with approaches (c.g, LINC Olausson et al. (2023) where the LLM first parses the full question into a logical form in an unconstrained fashion, where the model is not guaranteed to output valid expressions. To assess the impact of constraints that aim at aiding formalization, we ran gpt-3. 5-t.rrbo on 100 problems from each of the 4 datasets used in Fig. 3, with such con- straints disabled. We found that, in 11.5% of these problems, gpt-3. 3pt-3.5-turbo 5-turbo generated malformed constraints - either syntax errors, or inconsistent arities in different uses of the same predicate. For instance, in one prob- lem in ProofWriter, the LLM generated " "(...) If something is (tprop:rough]) and furry] [[axiom: ( (rough 'x) -> (furry 'x)) -> (young "x)) " where the generated axiom (a) has extra parentheses in the first premise, and (b) has the wrong number of closing parentheses at the end. Albeit simple, these mistakes can completely prevent approaches based formal- ization to work, and they still occur with state-of-the-ar LLMs. Nonetheless, LOGICGUIDE is effective in preventing them - 100% of the formalizations that LLMs produce with it are well-formed.
then it is [[prop:young]]
DeontiQA Errors in LLM reasoning would be especially problematic when an agent must decide which actions are allowed by its instructions. Hence we created DeontiQA: a set of 60 new reasoning problems inspired by Deontic Logic (Von Wright, 1951). Deontic Logic is concerned with judgments of the type "action X is coanniiiible/bligatoo.r
(or not), rather than solely "proposition X is truc" (c.g., in first-order logic). Peano allows us to easily embed the deontic axioms on top of its lype theory. We follow the methodology used in PrOntoQA to create the problems, creating logical forms first and then realizing them in natural language. Like in PrOntoQA, we add distractor rules to prevent guessing the answer from surface shortcuts. In these problems, the goal is to decide whether a given action is permissible, obligatory, or impermissible in the context of managing calendar events for a group of people. We detail the creation of DeontiQA in
7

---

Published in Transactions on Machine Learning Research (05/2024)
GPT-3 Davinci
GPT-3.5 Turbo
LLaMA 13B
1.0
LogicGuide?
0.8
No
Accuracy
0.6
0.4
0,2
0.0
Consistent
Consistent
Incorsistent
Figure 4: Accuracics of models with and without LOGICGUIDE on the Syllogism Validity task.
the Appendix, and make the dataset available along with our code. DeontiQA problems are significantly longer (up to 28 rules) compared to PrOntoQA (maximum of 18). This increased length mcans we are only able to fit one prompt example in the context window of GPT-3 and GPT-3.5 Turbo. We find LOCICGUIDE to be helpful on DeontiQA: GPT-3 alone is correct on 61.6% of problems, which increases to 80.0% with LOGICGUIDE. GPT-3.5 Turbo achieves 66.7% accuracy which increases to 78.3% when guided.
Overall, this provides positive evidence for our first research question: LOGICGUIDE can signisicuntly improve the accuracy of base models in natural language reasoning problems. Their answers become not only more accurate but also more trustworthy: LOCICGUIDE makes models answer "Unknown" when they don't io have an answer, rather than producing an unsupported guess.
4.2 Mitigating content effects in reasoning
Both humans (Evans, 2002) and LMs (Dasgupta et al., 2022) have been shown suffer from content effects in reasoning: their accuracy in logical judgments is influenced by prior beliefs about the assumptions and conclusions. For instance, from the assumptions "Some librarians are happy people" and "Some happy people are healthy people", it does not logically follow that "Some librarians are healthy people". Humans and LMs have difficulty judging this argument as invalid because the conclusion agrees with prior beliefs. We hypothesize that LMs will have less influence from the content when formalizing assumptions, rather than reasoning from logical sentences. If that is the case, then using LOCICGUIDE will help mitigate content effects.
We use two tasks to investigate this hypothesis. First, we contrast the results in the different PrOntoQA ontologies. As in the original PrOntoQA results (Saparov & He, 2022), GPT-3 and GPT-3.5 Turbo is already close to ceiling in the True Ontology split (where the model doesn't 't. strictly need to reason correctly as long as it judges the conclusion using common sense). In contrast, accuracy is significantly lower in the False and Fictional ontologies and decays with more hops. However, both of these models are highly accurate in formalizing assumptions, and thus benefit from the guide in the False and Fictional ontologies: performance near ceiling. Interestingly, GPT-3.5 Turbo still exhibits occasional content effects, explicitly judging the conclusions derived using LOGICGUIDE as nonsensical in cases where they do follow from the problem. For instance, in one problem where the model must docide whether Sam is luminous not, it is given that "Sam is a snake", and from the given assumptions the model correctly concludes <... [[hneer sam)]] Sam is sheep". It then proceeds to question this conclusion and halts: "This contradicts the fact that Sam is snake. Therefore, we cannot infer whether Sam is luminous or not.".
that the base performance of
Second, we leverage the Syllogism Validity dataset (Dasgupta et al., 2022). In this task, the model given two assumptions and a conclusion and has to decide together they constitute a valid argument (i.e., the conclusion logically follows from the assumptions). The example above about librarians is taken from this dataset. Solutions have a single step: judging the argument valid or invalid. When using LOGICGUIDE, prompt the model to first perform single inference given its formalization of the assumptions and then judge the validity of the argument. Syllogism Validity has 3 conditions: "Nonsense", where rules are about made-up concepts, "Consistent ", where the conclusions agree with commonsense regardless of whether the argument is valid, and "Inconsistent", where the conclusion always violates world knowledge. Unguided models behave consistently with those Dasgupta et al. (2022): in the "Consistent" split, all models strongly tend judge the argument as being valid, thus performing close chance (GPT-3.5 Turbo is slightly better, 60%). Both GPT-3 and GPT-3.5 Turbo are, however, highly accurate at formalizing the assumptions
8

---

Published in Transactions on Machine Learning Research (05/2024)
and conclusions and tend to trust LOGICGUIDE, nearing ceiling performance for all conditions. LLaMA 13B
has much more difficulty judging the syllogisms, performing near chance in all conditions. However, it is still successful at formalizing many syllogisms, obtaining non-trivial performance (60% to 77%) when using LOGICGUIDE. In failure cases, it often confuscs logical connectives (c.g., formalizing "Some X are Y" as "X implies Y" and vice-versa). We overall see positive evidence for our second research question: models with LOGICGUIDE show greatly diminished content effects, with stronger benefits for models that are more capable of interpreting individual sentences (despite struggling to reason with them when unguided).
4.3 Learning to reason by guided self eefroveprv
We consider improving the reasoning ability of the base LM. When using LOGICGUIDE, the model still produces its rationales, though with constraints (in contrast to approaches that aim to fully offload reasoning to an
0.90
Mode
PrOntoQA Accuracy
0.85
Guided
Strict Guided
external tool). Thus, this lets us use successful rationales to improve the model itself. This is the essence of the Self-Taught Reasoner (STaR; Zelikman et al. (2022)) a simple method for improving LLM reasoning that has been shown to be effective in symbolic, mathematical and commonsense reasoning. Given a set of problems paired with correct final answers (but not reasoning traces), STaR iterates between (1) solving problems with chain-of-thougle prompting, and (2) fine-tuning the model on its own generated rationales that led to correct final answers. This allows the model improve its reasoning from small seed set of few-shot examples.
0.80
Unguided
0.75
0.70
0.65
0.60
STaR Iteration
Figure 5: LLaMA 13B accuracy on held-out PrOn- toQA problems when bootstrapping using STaR.
Crucially, STaR relies on the premise that if rationale led to the correct onswer, it is likely to be correct. While this holds in domains like arithmetic, it breaks down in most logical reasoning tasks. In these cases, right answers will happen often with bad rationales, leading STaR and similar approaches to fine-tune on incorrect reasoming that generalizes poorly. Indeed, the authors in Zelikman et al. (2022) remark that "filtering bad reasoning paired with correct answers remains an open question."
We thus consider STaR training on either all correct answers (with LOGICGUIDE or not) or only on certified correct answers. We run STaR iterations with LLaMA 13B PrOntoQA where attempt 200 random problems equally split between 1 and 5 hops, fine-tune on successful solutions, and evaluate on unseen problems.
Fig. 5 shows the results. As predicted in Zelikman et al. (2022), the high chance of guessing confounds STaR, and training on all rationales that yield correct answers does not give meaningful improvements ("Unguided", red curve). Training on all guided solutions leading to correct answers brings improvements ("Guided"; 72% to 80% after one iteration), but still ends up with accidentally-correet reasoning when the model guesses after reasoning for few steps. Fine-tuning only on certified correct answers avoids this trap and achieves high performance ("Strict Guided", up to 86%). This allows to positively answer our third research question: LOGIeGUidE can be used for effective self- aef-iimproveeent in reasoning, in cases where naive methods collapse.
4.4 Generalizing beyond formalization
Finally, we consider whether models bootstrapped on their own rcasoning in synthetic multi-stop reasoning tasks can generalize lo settings requiring similar reasoning with real-world language. To that end, we consider ReClor (Yu et al., 2020), a dataset of logical reasoning problems taken from standardized exams (e.g., LSAT and GMAT, 4-way multiple choice), as well as the tasks in LEGALBENCH (Guha et al., 2023) related to Diversity Jurisdiction (binary choice given facts about plaintiffs, defendants and claims, determine whether the criteria for diversity jurisdiction are met). These questions are challenging even for humans. Although
ProofWWiter has shorteuts that allow guessing the answer without reasoning (Zhang al,, 2022), which fine-tuning quickly learns. PrOntoQA avoids those with distractor rules. Thus, we focus on PrOntoQA here.
9

---

Published in Transactions on Machine Learning Research (05/2024)
Diversity1
Diversity2
Diversity3
Diversity4
Diversity5
Diversity6
ReClor
0.5
0.4
Model
Base Model
Base Bootstrap
LogicGuide Bootstrap
Figure 6: Zero-shot performance on six LEGALBENCH tasks and ReClor, compraing the base gpt-3.5-turbe model and as versions bootstrapped with and without LOGICGUIDE.
they require logical thinking, it is often unclear how to formalize them. Thus, directly using LOGICGUIDE with few-shot prompting is of limited use, and bootstrapping directly on ReClor is unlikely to get off the ground. So, we explore whether models bootstrapped from formalizable tasks transfer to ReClor and LEGALBBNNCH
Since these questions are very rich in terms of reading comprehension, we need a strong base model with non-trivial zero-shot performance. Thus, we use GPT-3355 Turbo, and leverage the OpenAl fine-tuning API. For bootstrapping, we use random sample of 120 correct solutions from a mixture of ProofWriter and PrOntoQA problems with 3+ hops, where the original model either used LOGICGUIDE not. For inference use zero-shot prompting, where we ask the model to first carefully analyze each of the options before solutions
deciding which is correct (prompt in the Appendix). Fig. 6 shows the results. Bootstrapping obtained with LOGICGUIDE yields the highest accuracy on ReClor (65%), compared to bootstrapping without LOGICGUIDE (58.3%) and to the base model (52.5%). The overall relative performance between the models is similar on LEGALBENCH tasks. When inspecting the solutions, we find that the model never explicitly tried use LOGICGUIDE (which we would see with bracket annotations) but the style of reasoning resembles the solutions to the synthetic problems when appropriate (e.g., "Reasoning: Liam and Amelia are from different. states. The amouut-in-conntroversy is greater than $75k. Answer: A. Yes, there is diversity jurisdiction." whereas for this same problem the base model outputs a 132-word long rationale). This style is similar in both bootstrapped models (we show several complete samples for ReClor in App. G). The higher-quality rationales obtained with LOGIGGUIDE seem to have better overall effect, leading to higher accuracy. Overall, we find positive evidence for our last research question: bootstrapping models with LOGICGUIDE can lead to better performance even when LOGICGUIDE not available at inference lime.
5 Discussion and conclusion
We introduced guide tools, which locally constrains generation when invoked by a language model. Log- ICGUide leveraged this idea for logical reasoning, allowing the LM to formalize its interpretation of input sentences and make sound inferences. Moreover, when booistrapping models on their own reasoning, they can generate better reasoning even when unguided at inference time.
The direct application of LOCICGUIDE is challenging for general natural language, which is often ambiguous and can be difficult faithfully represent in formal logic. Domains where arguments tend have more systematic logical structure, such as law, are more likely benefit from tools like LOGICGUIDE, Still, our work suggests that bootstrapping on formal problems might help models generalize. Even then, models can still fail at planning even when making correct deductions. Many current investigations into planning techniques for LM reasoning are complementary to our work and can be integrated with guides (Mehran Kazemi et al., 2022; Zhao et al., 2023).
Language models bring to reasoning the flexibility human language and a wealth useful prior knowledge. But that power comes with lack of reliability and difficulty verifying extended reasoning. Our approach points rich direction for seamlessly integrating reliable symbolic and flexible neural reasoning into unified text stream. The result. is better, and more easily verified, reasoning.
10

---

Published in Transactions on Machine Learning Research (05/2024)
Acknowledgments
This work was supported by a NSF Expeditions Grant, Award Number (FAIN) 1918771. GP was also supported by the Stanford Interdisciplinary Graduate Fellowship (SIGF).
References
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean- SannChhistophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assisland reference manual: Version 6.1. PhD thesis, Inria, 1997.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, al. Language models are few-shot learners. Advances in neurol information processing systems, 33:1877-1901, 2020.
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gchrmann, et al. Palm: Scaling language modeling with pathways. Xix preprinl arXiv:2204.020: 02311, 2022.
Karl Cobbo, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reicchiro Nakano, et al. Training verifiers to solve math word problems. aiviv preprinl ur Xrxi::1 10. 14168, 2021.
Ishita Dasgupta, Andrew K Lampinen, Stephanie CY Chan, Antonia Creswell, Dharshan Kumaran, James L McClelland, and Felix Hill. Language models show human-like content effects on reasoning, ar preprint arXiv:2207.07051. 2022.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Peduution-CAAD--2. 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
Jonathan St BT Evans. Logic and human reasoning: assessment of the deduction paradigm. Psychological bulletin, 128(6))978, 2002.
Neel Guha, Julian Nyarko, Daniel E Ho, Christopher Ré, Adam Chilton, Aditya Narayana, Alex Chohlas- Wood, Austin Peters, Brandon Waldon, Daniel N Rockmore, et al. Tegalbench: A collaboratively built benchmark for measuring legal reasoning in large language models. arXiv preprint arXiv:2308. 11462, 2023.
Joy He- Hueya,, Gabriel Poesia, Rose E. Wang, and Noah D. Goodman. Solving math word problems by combining language models with symbolic solvers, 2023.
Ehsan Hosseini-Asl, Bryan McCann, Chien-Sheng Wu, Semih Yavuz, and Richard Socher. A simple language model for task-oriented dialogue. Advances in Neural Information Processing Systems, 33:20179 20191, 2020.
Yinya Huang, Meng Fang, Yu Cao, Liwei Wang, and Xiaodan Liang. DAGN: Discourse-aware graph network for logical reasoning. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pp. 5855, Online, June 2021. Association for Computational Linguistics. doi: 10.18653/ 2022 nancl-main.445 URL https://aace https///aacaanhooggoyo org/ naacl-main, 467.
Ximing Lu, Peter West, Rowan Zellers, Ronan Le Bras, Chandra Bhagavatula, and Yejin Choi. NeuroLogic decoding: (un)supervised neural text generation with predicate logic constraints. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguisties: Human Language Technologies, pp. 1288-4299, Online, June 2021. Association for Computational Linguistics. doi: 10. 10.18653/v1 mann:///m//m..an
maa.c-mman..nn-. 339. URL https: htapp::://aclanhhllog.o org/2021 naacl paacc-main
11

---

Published in Transactions on Machine Learning Research (05/2024)
Ximing Lu, Sean Welleck, Peter West, Liwei Jiang, Jungo Kasai, Daniel Khashabi, Ronan Le Bras, Lianhui Qin, Youngjae Yu, Rowan Zellers, et. al. Neurologic a* esque decoding: Constrained text generation with lookahead heuristics. In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pp. 780-799, 2022.
Scyed Mchran Kazemi, Najoung Kim, Deepti Bhatia, Xin Xu, and Decpak Ramachandran. Lambada: Backward chaining for automated reasoning in natural language. orXiv e-prints, pp. arXiv 2212, 2022.
Pasquale Minervini, Scbastian Riedel, Pontus Stenetorp, Edward Grefenstette, and Tim Rocktäschel. Learning reasoning strategies in end-to-end differentiable proving. In ICML 2020, 2020.
Theo X Olausson, Alex Gu, Benjamin Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger Levy. Line: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. arXiv preprint Xrx:22330. 15164, 2023.
OpenAI. Gpt-4 technical report, 2023.
Gabriel Poesia and Noah D Goodman. Peano: Learning formal mathematical reasoning. Xiv preprint arXiv:2211.1586, 2022.
Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable code generation from pre-trained language models. In International Conference Learning Representations, 2022.
Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. Advances in neural informalion processing systems, 30, 2017.
Abulhair Saparov and He He. Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. arXiv preprint arXiv:2210.01240, 2022.
Timo Schick, Jane Dwivedi- Yu, Roberto Dessi, Roberta Raileanu, Maria Lomeli, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. arXiv preprint arXin:2302.04 04 2023.
Dhruv Shah, Blažej Osiński, Sergey Levine, al. Lm-nav: Robotic navigation with large pre-trained models of language, vision, and action. In Conference on Robot Learning, pp. 492-504. PMLR, 2023.
Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gchrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoe V Le, Ed H Chi, Denny Zhou, al. Challenging big-bench tasks and whether chain-of- thought can solve them. arXiv preprint arXiv:2210. 0.09611, 2022.
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Associalion for Computational Linguisties: ACL-IJCNLP 2021, pp. 3621-3634, 2021.
Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Ami Lachaux, Timothée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, et al. Llama: Open and efficient foundation language models. arXiv preprint urXiv:2302. 13971, 2023.
Georg Henrik Von Wright. Deontic logic. Mind, 60(237): 1951.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fd Chi, Quoc Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. arXiv preprint urXiv:2201.11903 2022.
Jason Weston, Antoine Bordes, Sumit Chopra, Alexander M Rush, Bart Van Merriënboer, Armand Joulin, and Tomas Mikolov. Towards ai-complete question answering: A set of prerequisite toy tasks. arXiv preprint xrXv:11002.05695 2015.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353- -222333--3268,, 2022.
12

---

Published in Transactions on Machine Learning Research (05/2024)
Zhengyuan Yang, Linjie Li, Jianfeng Wang, Kevin Lin, Ehsan Azarnasab, Faisal Ahmed, Zicheng Liu, Ce Liu, Michael Zeng, and Lijuan Wang. Mm-react: Prompting chatgpt for multimodal reasoning and action. arXiv preprint arXic:2303.1100 2023.
Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. React:
Synergizing reasoning and acting in language models. arXiv preprint arXit:2210.0360 2022.
Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. Reclor: A reading comprehension dataset requiring logical reasoning. arXiv preprint arXiv:2002..420 2020.
Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. Star: Bootstrapping reasoning with reasoning. Advances in Neural Information Processing Systems, 35:15476-15466 2022.
Honghua Zhang, Liunian Harold Li, Tao Meng, Kai- Chang, and Guy Van den Broeck. On the paradox of learning to reason from data. arxiv preprint ar arXi:22255.11002 2022.
Hongyu Zhao, Kangrui Wang, Mo Yu, and Hongyuan Mei. Explicit planning helps language models in logical reasoning. arXiv preprint arXiv:2303. 211112303.15144 15714, 2023.
A Other Guides
In $3.2 explored LOCICGUIDE, which captured rich set of operations that both set and leverage state, as well as a complex external logical support tool. Nonetheless, many other guides can be easily defined in this same framework. We survey several such guides here as potential ideas for future work:
Memory Guide A simple guide in the same format of LOCICGUIDE can be one where the model can set and later on retrieve the value associated with given key ([[gee::eyy=value]]] When retrieving, the guide can limit the key to be within one of the existing values, and will force the value to be the last stored one. Values can be either overridden added to a set, depending the domain. This can elfectively implement memory, and this can extend beyond a simple context window provided that the guide keeps external memory. In problems like the bAbl tasks Weston et al. (2015) requiring models to keep track of the state of objects and characters through long stories, this guide can reduce the problem of remembering locations (and avoiding interference self-aitention) by the problem of translating each question into a query, using only local information.
values to keys
Quote Guide Language models often hallucinate quotes, e.g. saying that " "According to Wikipedia, 'YZ: Therefore...". P. We can implement a simple quote guide that forces quotes to actually come from a trusted source. Specifically, whenever a prefix like [[quote:]] is generated, the guide can force the subsequent output to be one of the sentences contained in a certain web page (that set regular). Externally, an UI can even mark guided quotes with their source, which can be kept by the guide.
Algebra Guide Mathematical reasoning tools can be also integrated as guides for math problem-solving:
Peano itself was originally used with algebra problems, and can thus also serve as a guide for mathematical reasoning. We can also leverage other tools, such as computer algebra systems, as guides. One example the SymPy integration with Codex used previously to solve math word problems He- Yueya et al. (2023), where some instructions can add variables, and some can indicate to the solver variable to be solved for. In the case of He- Yueya et al. (2023), the model simply indicates which variable to solve for, and the answer is externally extracted. When specifying equations in an [[eq]] block, the guide can force the model to output a syntactically valid equation, and also one that only uses already existing variables. This will guarantee that parentheses will be correctly closed (the completion engines in Poesia et al. (2022) achieve this by deriving a completion engine from a parsor) and that variables are used after they are introducod. If we wanted the model to also use the results from the solver, we can turn the [[answer]] block into a [[solve: xx=v]] guided block, where is constrained to be one of the existing variables, and is given by the algebra solver.
13

---

Published in Transactions on Machine Learning Research (05/2024)
B
DeontiQA
We generate the DeontiQA problems following the general methodology of PrOntoQA Saparov & He (2022), where we first sample assumplions and prools in logical form and then realize those in natural language. The main qualitative differences are (1) in the specific logical framework we use and (2) in how we translate logical sentences into natural language.
Logical framework We formalize logical framework for general domain of managing calendar and event invites in Peano. We create a base type for actions, as well as the deontic predicates permissible and obligatory, to be applied to actions. We have 5 object types: person, entity, reminder, event and invite. From these, we create kinds of actions:
Given an event invite, the agent can accept, decline or send notificaiio for that invite.
Given an event, the agent can cancel_event.
Given reminder specification (constructed with person and time period before the event), the agent can set_ set_reminder.
Given an event and an entity, the agent can add_ aod_paratiippnt or cemove_participar
Given event and person, the agent can delegate_ event.
event.
For event, person might eequest_event _ suggest_ alternative_time, Sheck_availabilit,
Given event and proper event properly to be changed, the agent can apdate_event reschedule_ event, or lhange_visiblltty with the property describing the proper update.
Problem generation To generale problem, we first sample theory set of hypotheses and using those assumptions we try to construct random derivation (applying axioms and assumptions to hypotheses or previous conclusions). The conclusion of the derivation (or its negation, 50% of the time) becomes the goal in the generated problem.
Translation to natural language To realize the problem in natural language, we use the aid of GPT-4 OpenAT (2023), prompted to translate the logical statements into a story in natural language given a few examples, with sentences describing the axioms. All stories were manually checked to still be unambiguous and logically sound, and we only use GPT-4 to help with diversity. As result, the DoontiQA problems show greater linguistic variation than both PrOntoQA and ProofWriter, especially at their beginning. We show 3 example problems in Fig. 7, Fig. 8 and Fig. 9, The full set of 60 problems is released along with the supplementary material.
C Constrained Semantic Decoding with Chat Models
Originally, Constrained Semantic Decoding was proposed to work with standard autoregressive language models Poesia et al. (2022). This relied on the ability to bias the logits of the model during generation, which is both possible in local models as well as through the OpenAl API? The OpenAI gpt3. 5-turbo has different API, since is chat-based model. In this API, we pass list of messages with roles (user assistant, where the model understands the latter marking its past generations). The AP1 also has logit bias parameter. However, we unfortunately cannot pass an incomplete prefix for the model's response. Thus, we are unable to force the model to complete a certain message while also applying logit biases. Every completion starts a new message. This requires an adaptation to the procedure in Poesia et al. (2022).
2https: ptttpss//platfor:. openai http:///wwwootatete//cctcttttttt
14

---

Published in Transactions on Machine Learning Research (05/2024)
Context: 1- In a company, there are three employecs: Alice Bob, and Carol. 2- They have a group called 'WorkTeam", 3- They have three upcoming events: a team event, a team- baamdiuiliing event, and a product launch event. 4- Bob is the organizer of the team- nan-building event. 5- Carol is participant in the product launch event. 6- 'The team event is a conference. 7- The team-building event is yearly. 8- The team event is a monthly event and is short event, while the product launch event is a long event. 9- Alice is busy during the team event, while Bob is free during the product launch event. 10- The team event is a private event, and the product launch eveut is a public event. 11- If a person is busy during event, event, it is permissible to add them
it is impermissible to add them as participant. 12- If person is free during participant. 13- If an event is a long event, it is obligatory to add groups a participant. 14- If an event has high priority for person, then it is not obligatory to set reminder for few days before the event for that person. 15- If an event is conference, it is permissible to update the event be public. 16- If an event has low priority for a person, it is permissible cancel the event. 17- If event is short, is impermissible has low priority for person, then obligatory to set reminder for a few days before the event for that person. 19- If event private,
reschedule the event yearly. 18- If an event
participant. 20- If person is participant permissible request an event update from them. 21- person the organizer of an event, it obligatory change the event's visibility to confidential. 22- If an event is a monthly event, is a short event. 23- If an event is yearly event, it is a long event. 24- If an event is long, then Carol has high priority for that event. 25- an event is conference, it a public event. 26- If an event is private, it is a meeting. 27- If an event is public, it is social event. 28- a person is the organizer of an eveut, they are a participant in that ovent.
obligatory to remove Carol
an event, it
Question: Civen the rules above, is it not obligatory for Carol to sot a reminder for a few days before the team-building event?
Reasoning: The team-building event is a yearly event. The team-building event is a long event. Carol has high priority for the team-building event. If an event has high priority for a person, then it is not obligatory to set a reminder for a few days before the event for that person. Thus, it is not obligatory for Carol to set a reminder for few days before the yearly team- bainn- event.
Answer (yes or no): Yes, it is not obligatory for Carol to set a reminder for few days before the yearly team- haam-building event.
Figure 7: Example #1 of a DeontiQA problem.
Context: 1- In a marketing agency, there are three employees: Alice, Bob, and Carol. 2- Alice is the marketing manager, Bob is graphic designer, and Carol is a content writer. 3- The company has a remote team called 'Creative Team'Tem''. 4- They have three upcoming events: a brainstorming session, company party, and a progress event. 5- Alice is the organizer of the brainstorming session, Carol is participant in the company party, and the Creative is group participant in the progress event, 6- The brainstorming session is short, while the company party is long event. 7- The brainstorming session is moeting, and the company party is social event. 8- If an event has high priority for person, it is permissible for them to suggest participant. 10- If person is free during an event, is permissible for them to accept an individual invite to the event. 11- If group is participant an event, it is permissible during an event, it is impermissible to set a reminder for few minutes before the event. 13- If person a participant an event, it permissible
alternative time. 9- If a person is the organizer of event, it is obligatory to add them as a
delegate the event to the group. 12- If person busy
remove them as a participant. 14- For short events, it is permissible to update the event to a social event. 15- If person's 's status is tentative for an event, it is obligatory to check the availability of the person for that event. 16- If an event has high priority for a person, it is obligatory to set a reminder for a few days before the event. 17- If a person is a participant in an event, it is impermissible for them to suggest an alternative time. 18- If an event is public, it is obligatory to add Alice as a participant. 19- Meetings are public events. 20- Public events are short events. 21- If person is the organizer of an event, their priority for that event is high. 22- If a person is a participant in an event, they are available for that event. 23- If an event is short, Bob is a participant. 24- Daily events are short events. 25- If a person has high priority for an event, they are busy during that event. 26- If a person has a low priority for an event, they are free during that event. 27- If a group is participant in an event, the event is public. Question: Given the rules above, is it permissible for Bob to suggest group participant in the progress event. The progress event is public event. The progress event is short event. Bob is a participant in the progress event. It is impermissible for participant to suggest an alternative time for event they are participating in. Auswer (Yes or no): No
alternative time for the progress event? Reasoning: The CreativeTTamm is a
Figure 8: Example #2 of DeontiQA problem.
15

---

Published in Transactions on Machine Learning Research (05/2024)
Context: 1- In a software company, there are three project managers: Alice, Bob, and Carol. 2- They have a team called "DevTeam'. 3- They have two upcoming events: a team-building activity and a project review event. Alice is the organizer the team- team-building building activity, Bob is a participant in the team-building activity, and the entire DevTeam is particlpating in the team- baam-buidding activity. 5- The project review is a short event. 6- The buildiilding activity is a social event. 7- The team-building activity is public event, 8- If a person is the organizer of an event, it is obligatory to add them as a participant. 9- If a person is a participant in an event, it is permissible for them to accept an individual invite to the event. 10- If am event is short, it is impermissible to cancel the event. 11- If a group is participating in an event, it is obligatory to add the group as participant. 12- If person is free during an event, it is permissible to set reminder for a few hours before the event. 13- If a person is busy during an event, it is impermissible to reschedule the event to be daily event. 14- If an event is public, it is obligatory to check Alice's availability for the eveut. 15- If person is a participant in event, it is permissible to delegate the event organization to them. 16- If person's availability for an event is tentative, it is permissible for them suggest alternative time for the event. 17- If event has high priority for a person, then it is obligatory to is impermissible for them suggest an alternative time for the event. 19- If an event is short, then it is meeting. 20- If an event is meeting, then Bob's availability for the event is tentative. 21- If Alice's availability for event is tentative, then she is participant in the event. 22- If person free for an event, then the event has low priority for them. 23- If event is public, then it is social event. 24- an event private, then is personal event. 25- If an event is daily, then it is not a weekly event. 26- If an event is weekly, then it not a monthly event. Question: Given the rules above, is it permissible for Bob to suggest an alternative time for the project review? Reasoning: The project review is meeting. Bob's availability for the project review is tentative. It is permissible for person with tentative availability to suggest an alternative time for the event. Therefore, it is permissible for Bob to suggest an alternative time for the project review. Answer (Yes or uo): Yes, it is permissible for Bob to suggest an alternative time for the project review.
reminder for them for few days before the event. 18- If person's availability for an event is free, it
Figure 9: Example #3 of a DeontiQA problem.
We start with the usual rejection-based CSD procedure: we put few-shot examples in the previous messages showcasing the response format we want, and sample a full response from the model. We then use token-by- token CSD to validate the response. If this terminates without finding any violation, we're done- - the entire generation, including choices made in guided blocks (e.g., infer), were valid. If not, like in original CSD, we take the largest valid prefix and use the CSD algorithm to compute the set of tokens that are valid after that prefix.
Here we reach the main difference in the API. We want the model to continue its message from the last valid token. However, this is not possible in the current API. Instead, we must request a new message. Fortunately, we found incomplete.. We exploit this behavior and (1) request new message with a single token, passing the set of valid tokens in the logit bias, (2) append the sampled token to the previous message and request a new, unconstrained message, and (3) repeat until we have received a full response.
to very frequently simply continue its generation when its last message appears
When the model continues from where it stops, this approach is essentially equivalent to rejection-based CSD. Unfortunately, it is not fully reliable. In a number of cases, we found the model to insistently apologize after noticing that its previous message was incomplete. This is problematic when the previous message started a guided block that is to be finished in the next message. In this case, the model's apology is contained in the guided block, and is thus always an invalid generation. What happens is that this immediately triggers violation, and the CSD procedure above is executed.
Often, the CSD corrections will eventually get the model to make enough choices to complete the guided block, at which point its apology is not an issue anymore (c.g., see Fig. 10. In rare (< 0.1%) cascs, the issuc persists and we cannot recover from the apology (Fig. shows an example). To avoid a prohibitive number of APT calls, we aborted sampling when more than 20 violations were hit in the same solution.
D Experimental Details
Experiments with the OpenAI models were made using their public API. For LLaMA 13B, we ran and fine-tuned the model on an NVIDIA A100 80GB GPU. For fine-tuning when running STaR (64.3), we performed inference on 200 problems 40 for each number of hops from 1 to 5 in each STaR iteration, and
We hypothesize this done that models also complete their messages when the token limit hit in the Open Playground and users immediately request a new completion
16

---

Published in Transactions on Machine Learning Research (05/2024)
Formalized context: 1- Every [[proxdumppu]] is an [[prop:impus]] [[axiom:[ddumpus 'x) ->> (impus 'x)]] 2- Each [propwumpus]]] is not [[prop:luminous]] [[xxoo:(yumppu 'x) -> (not (luminous 'x]]]] 3- [[prop:dumpus]] are [[prop:orange]] [axiom:[dumpus 'x) -> (orange 'x]]]. 4- Every [[prop:wmmpus]]] is [[prop:bitter]]-
[[axiom(wwumpus 'x) -> (bitter 'x]]] 5-
Each [[prop:jmmpui]] is not [propxorange]]. [[axiom:[jompu> 'x)>> (not (orange 'x]]]] 6- [[prop:umpuu]]] are [[prop:numpus]] [axiom: (wumpus xx] (numpus 'x)]]. 7- [[prop:impus]] are [[prop:rompual] [Impus 'x) ->> (rompus 'x]]]- 8- Every (opaque 'x]]] 9- [[prop:uumppu]] are [[prop:dul]]] [[amps -x)>> (dull xx]]] 10- [[prop:vmmpus]] are [prop:wumpus]]. [[umpom:(vumpus 'x) -> (wumpus 'x]]]. 11- Each [[prop:mmmpu]] is [propxdumpus]]. [[axiom: 'x) -> (dumpus 'x)]]. 12- [[object:wee]]]
[prop:impuu]]] is [[rroxoopqquell- [[axiom:(impus
[[prop:dumpus]] [[exiom:(dumpus
wren)]]. Formalized goal: [[goa] wren)]]
Reasoning: ['infer:iimpus wren)]] Wren an impus. [[infer:(rompna wren)]] Apologies for incomplete message. Continuing from where stopped: [linfertopaque wren].] My apologies for the incomplete message. Continuing from where stopped: [linfer: wren)]]] Wren orange. This was goal.
Answer: True
Figure 10: Example generation of gpt3.5-turbe 55-turbo with LOGICGUIDE on PrOntoQA where the model started to apologize twice after violating the guide, but it eventually recovered with our chat adaptation of CSD.
Formalized context: 1- [[abject:bob]] [[prop:blue]]- [[axiom:(bluu bob)]]. 2- [[object:bob]] [[propsquiet]]- [[axiom:(quiet bob)]]. 3- [[object:bob]] [[propared]]. [[axiom:[red bob)]]. [[object:bob]] is [[proptrough]]- [[uxiom:[rough bob]]]. [[object:bob]] [[prop:smart]]. [[axiom:(ssmat bob]]]. 6- [[object:charlic]] [[propxcold]]. [[axiom:(cold charlic)]]. 7- [[objcctcchrric]]] [[propared]]. [[aiiom (rod charlie)]]. 8- [[object:dave]] is [[prop:bluc]]. [[axiom:(bluee dave)]]. [[ob- ject:dave]] is [prooequiet]]. [[axiom:(quiet dave)]]. 10- [[objectserin]] [[prop:cold]]. [[axiom:(cold erin)]]. [[object:rrn]]] is [[prop:witte]]. [laxiom:(white erin)]]. 12. Tf something is [[propssmart]] then is [propewhite]]. [[axiom:((mart 'x) -> (white 'x]]] 13- All [[propqquiet]], [prop:rouuh]] things are [[propsmaat]]. [aaxiom: (isiom:((ssommthinn isPSSorryPSI apologizePST apologizePSI spologizePSI apologizePSI apologizePSI apologizePSI apologizePSI apologizePSI apologizePSI apologizePSI apologizePSI PSologizePSFormall contextPSI apologize for the previous messagePSIPSIPSI apologize for the previous messageSS
Figure 11: Example generation of gpt3. 50t3.5-turbo with LOGICGUIDE on ProofWriter where the model started to apologize after violating the guide, and did not recover. Here, it violated the s-expr syntax for defining axioms in Pcano, but after being constrained still insists apologizing, instead of trying to finish the formula. This behavior is rare (< 0.1% of the cases), and would be avoided if the APT had a parameter give the model an incomplete message for to complete.
17

---

Published in Transactions on Machine Learning Research (05/2024)
collected the generations where the model reached the correct answer (with each of the 3 criteria described in $4.3). We fine-tuned for epoch (i.e., seeing each example exactly once) with batch size of 2 and a learning rate of 2e-5. We used the Adam8bit optimizer with default parameters, reset in each iteration of STaR.
E Prompts
All of our prompls are provided in the allached supplementary material. We use JSON files for the chat. model prompts, exactly we pass them the OpenAl API.
F Complete Samples PrOntoQA/ProofWiic
We here provide full samples of solutions generated by language models with LOGICGUIDE, also showcasing the most common failure modes.
Fig. 12 shows one case of text-davinci-003 on the PrOntoQA False Ontology, where the model properly formalizes all of the assumptions, but still tries to make wrong conclusions very often. As a result, its solution ends up taking long detour eventually get to the goal, but eventually does so correctly (it can be concluded directly from two of the assumptions).
Fig. 14 shows one example of gpt3.5-turbe 5-turbo on Proo/Writer, where the model further justifies its solution based on the axioms. We found these post-hoc justifications to be highly accurate. Unguided models sometimes also justify their inferences even if not prompted to do so, but to do so they must procuce hallucinations (or assume general world knowledge, such that "an animal cannot chase itself").
Fig. 13 shows one rare failure mode where the model misclassifies whether it has already proved the goal, and thus does not proceed further. We can detect this failure mode with LOGICGUIDE, since we have access to the Peano state and ask the environment whether the goal proved or not. In this way, explained in App. D,, we can distinguish certified and uncertified answers.
Fig. 15 shows a case where LLaMA 13B misformalized (several) assumptions, whereas Fig. 16 shows a similar case with text-davinci-003 (much more rare). The result in both cases is that the model cannot make progress in its formal inferences, instead of making invalid deductions. Again, since we can detect when the answer was not formally derived, we can avoid fine-tuning on these cases where the model still guesses the right answer but with unsond reasoning, exploited in $4.3.
G Complete Samples ReClor
We here show three full examples of questions and answers from the ReClor datasct, highlighting the differences in the base GPT-3.5 Turbo model and both of its bootstrapped versions. The zero-shot prompt we used was: "Answer the problem below. First, carefully analyze the context and each of the options before deciding which is correct. Then, the end of your response, end with line with the format "Answer: X', indicating one of the options.". We tested several variations of these instructions, picking the one where the base model obeyed the expected format the best
18

---

Published in Transactions on Machine Learning Research (05/2024)
Context: Every dog is small. Every feline is snake. Every animal is not bitter. Sheep bitter. Cats carnivores. Each vertebrate is a mamuaal Mammals are felines. Each vertebrate dull. Snakes are cats. Cats are not kind. Every snake is not happy. Every shoep a vertebrate. Each feline cold. Each dog a sheep. Every mammal is not liquid. Every carnivore is cow, Every carnivore is brown. Alex a sheep.
Question: True or false: Alex is not bitter.
Formalized context: 1- Every [[propadog]] is [[prop:small]] [[axion[[dog 'x) -> (small 'x]]]- 2- Every [[prop:feline]] is a [pprossnakel]] [[axiom:((fline -x)>> -> (smake 'x)]l. 3- Every [[propaniiaa]]] is not [[prop:bitter]]] [[axiom:(aninal 'x) -> (not (bitter xx)]l- 4- [[prop:hhepp]] are [[prop:bitter]]. [[axion: 'x) -> (bitter 'x]]]. 3- [|rrpxcat]] are [|propxcarnivord]. [aaxiom:[cat: 'x) -> (carnivore 'x)]]_ 6- Each [|prop.vertebrate]] is a [|prop:mammaa]]- [[axiom: (vertebraeee 'x) -> (mammal x)]]- 7- [[prop:mammaa]] are [[prop:feline]] (ixiom:(vertebratee 'x) +> (dull 'x]]]- 9- [[propssnake]] are [[prop:cat]]] [[axiom:(snakee 'x) -> (cat. 'x)]]. 10- [[propecat]] are not [[prop:kind]]. [[axiom:[cat 'x)-> (not (kind 'x)]]]. 11- Every [prop:snake]] is not [[prop:happsi]] [[exiom: 'x) ->> (not (happy xx]]]]. 12- Every [[prop:sheep]] is [[pro:vertebrate]]] (sheep 'x) -> (vertebrate 'x)]]. 13- Each [[prop:feline]] is [[prop:cold]]- [[axiom:(feline] 'x) -> (cold 'x)]]. 14- Each [[prop:dog]] is a [[prop:sheep]] [[axiom:(dog 'x) -> (sheep 'x]]] 15- Every [[prop:mammal]] is not [[prop:liquid]]- [faxloo::mammal 'x) -> (not (liquid 'x)]]] 16- Every [proopccaruivore]] is [[prop:cow]]. [|axiom:(carnivore 'x) -> (cow 'x)]]. 17- Every [[propxcarnivore]] [[prop:brow]]. [axiom:[carnivore "x)>> (brown 'x]]]. 18- [[oject:alex]] is [[prop:sheep]]. [[exiom(ssheep alex)]]. Formalized goal: [[goal:[not (bitter alex))]]
maxxiom:(maamii -x)-> (fellne 'xj]]. 8- Each [[prop.vertebraae]]] is [[prop:dull]-
Reasoning: [jinfer:vvertebbatt alex)]l Alex is vertebrate. []infer[dulll alex)]] Alex is dull. [[infer:(maamnn alex)]] Alex a mammaal finfer:[feline alex)]] Alex is a feline. []infer((not (liquid alex)]]] Alex is not liquid. [[infer: (snake alex)]] Alex a snake. [[infer[ccat alex]]] Alex is cat. [iineer(carnivore alex)]] Alex is carnivore. [[infer[[oot (kind alex)]]] Alex is not kind. [[infor:[uot (happy alex))]l Alex is not happy. [[infer(coodd alex)]] Alex cold, [[infer alex)]] Alex is brown. [[infer[cow alex)]] Alex is a cow. [[infer:bittter alex)]] Alex is bitter. This contradicts the goal. Answer: False.
Figure 12: Example generation of text-davinci-00s with LOGIeG on the PrOntoQA False Ontology- The solution to this problem can be reasoned in one step, but the model is strongly biased towards making wrong conclusions. LOGICGUIDE avoids those, but the model still takes many more inference steps to eventually reach the goal, deriving many useless facts first
Formalized context: 1- The [[object:cat]] is [prop:red]]. [[axiom::(red eat)]]. 2- 'The [[object:cat]] [[relationvviiits]]] the [object:cow]]. [[axiom:[visits cat cow)]]. 3- The [[object:cow]] is [[propbbig]] [[axiom:(big cow)]]. 4- The [[object:cow] [relation:needs]] the [object:dog]]- [[eeio cow dog)]]. 5- The [[object:cow]] [[elation:needs]] the [[object:aqiirel]]] Maxiom:[[ccde: cow squirrel]]]. 6- The [[object:doo]] does not [[relation:nce]]] the [[object:cat]]. [[axiom: (noods dog cat)) cat))]]. 7- The [[objoct:dog]] [[claaiion.vsits]]] the [[object:cow]]. [[axion: (visits dog cow)]]. 8- The [[objcttsquirrel]] [[relation:chases]]] the [[object:cow]]. Maxcoom:chasee squirrel cow)]]. 9- The [[objectssquireel] is [[prop:nice]]. [[axtiom: (nice squirrel]]]- 10- The [[object:squirrel]] [[relationanedds]] the [[ojjct:doo]]-- [[axiom:(needs squirrel dog)ll- 11- Tf someone [[relation:needds]] the [[objec:squirrel]] then they [[relation:chase]]] the [jobject:cat]]. [[uxiom:[needds 'x squirrel) -> (chases 'x cat:)]]. 12- If somcone [[rclation:chases]]] the [objectscaa]] then the [[bject:cat]] [[relationwiisite]]] the [[object:cow]]. [[axiom:: (chases 'x cat) -> (visits cat cow)l]. 13- If somcone [[cclationcchases] the [[object:cat]] then they are [[rro:nncc]]. [[axiom: (aaxioom(chases (chases 'x
cat) -> (nice 'x]]]_ 14- If someone [[relationschases]] the [qobjet::qqirre]]]] then the [[object:quirree]] [[elation:chases]] the [ob]ect:cow]]- [[axion:fehases 'x squirrel)- >> (chases squirrel cow]].. 15- If someone [[relationschosses]] the [[object:oo]]] and they [[relation:needd]]] the [[oject:squirrel]]] then the [[bject:eoo]] [[elatioo:needs]]] the [[objectasquirel]] [[axiom:(chasess 'x cow) -> (needs cow squirrel)- -> (needs cow squirve]]]]. 16- If someone is [[prop:nice]] then they do not [[eelationneed]]] the [object:cat]]. [[axiom:(nice 'x) -> (not (needs 'x cat))]]. 17- someone [[eeaationneedd]]]] the [[objectdoo]] and they are [[proprred]] then they [[relation:chase]] the [[oject:<do]]]- [[axiom::(nedds "x dog) -> (red 'x) -> (chases 'x dog]]]- 18- If someone is [[propanice]] and not [[rropgrree]]] then they do not [[relation:visit]] the [[object:cat]]- [[axiom:(nice 'x) -> (not (green 'x)] -> (not (visits 'x cat])]].
Formalized goal: [[goal:(not (needs cow cat))]]
Reasoning: [linfer[chasee cow cat)]] The cow does not chase the cat. [[infer[noo (needs aquirrel cat))]]] The cow does not need the cat. This was the goal.
Answer: True
with LOGICGUIDE on ProofWriter where the model misidentifies whether it has reached the goal or not. Given the Peano state and the formalized goal, we can at any point detect whether the model has indeed proved its goal or not, Le. whether its answer was certified or not. This can likely be avoided by making the step of outputting a conclusion be prefixed with a formal step, which can be constrained to only be allowed once the goal has been proved or disproved.
Figure 13: Example generation of
19

---

Published in Transactions on Machine Learning Research (05/2024)
(...) Formalized goal: [igoal:(quiet gary]ll
Reasoning: [[infer(yyoung gary)]. Gary young because he is round (from axiom 9). [[infe:[white gary)]l Gary white because round and round people are white (from axiom 5). [[infer:[not (quiet gary]]]] Gary is not quiet because is young and white, and all young, white people are not quict (from axion 7). Therefore, the answer False.
Figure 14: Example generation of 5-t.bbo with LOGIGGUIDE on ProofWriter, where the model provides further justification on the inferences. We found that models are highly accurate in justifying the inferences post-hoc, provided that they are correct.
Formalized context: The [[object:[ion]] chases the [[objert:qqirree]]] [[axiom:(chasees lion squirrel]]]- 2- The [[object:lion]] is [[prop:big]]. [[axiom:(big liou)]]. 3- The [[object:lion]] is [[prop:blue]]. [[axiom: lion]]]. 4- 'The [[object:loo]] is [prop:kind]]. [[axiom: (kind lion)]]. 5- 'The [[object:lion]] is [[prop:nice]]. [[axiom:[nice lion)]]. 6- 'The [[object:ioo]] is [prop:young]]. [[axiom:[youut (young lion]]]. 7- The [[object:lion]] needs the [oobjct:squirvel]] [[axiom:[needs lion squirrel]]]. 8- The [[object:lion]] visits the [[objet:squirrell]- [[axiom::viiits lion squirrel]]]- 9- The [[object:squirre]]] chases the [[object:lio]]]. [[axiom:(chasee) (chases squirrel lion]]l- 10- The [[objectssquireel]] is [[prop:big]] [[axiom:(big squirrel)]]. 11- The [[objct:squirree]] is [[prop:blue]]. [[axiom:((bue squirrel]]]. 12- The [object:squrree]] is [[prop:kiud]]. [|axiom: (kind squirrel]]]. 13- The [[bjjct:squirrel]] is [[rrop:iice]]. [exiom::(icc) squirre]]]]. 14- The [[uurect:suüire]]]] is [[prop:youn]]]. [[axiom: squirrel]]]. 15- The [[object:suirree]]] needs the [[object:lion]]- [nexds squirrel [ion)]]. 16- The [[ujjettaquirrel]] visits the [[object:lion]]- [[asion:(visits squirrel lion)]]. 17- If somcone visits the [[object:squiree]]] then they chase the [[object:lion]]. [jaxiom((vsiits squirrel lion) -> (chases lion)]]
Formalized goal: [[goal:(chascs lion lion)]]
Reasoning: [infer:nothing]] The lion does chase the lio.. This contradicts the goal. Answer: False
Figure 15: Example generation of LLaMA 13B with LOGICGUIDE on ProofWriter, where the model misfor- malizes assumption 17. The natural language sentence reads "if someone visits the squirrel, then they chase the lion", but the logical formulation written by the model would translate to "if the squirrel visits the lion, then the lion chases", As a result, the model not able to make any formal inferences. It still outputs an uncertified answer, which we can detect.
(...) 13- If something [[relation:visits]]]] the [[objcctsquirre]]]]]] and the [[objectaquirrel]]] [[relation:nedds]] the [[ob- jectsbald_ _oclle then the [[ojectaaquirel]] is [[prop-green]]] (uxiom:((vsitt. 'x squirrel) -> (needs squirrel bald bald_cagle) -> (green 'x]]] 14- If something [[eeattonnneeds]]] the [object:squirve]] then it is [[rropggree]]. [[axiom[[needs 'x squirrel) -> (green 'x]]]-
Formalized goal: [[geal squirre]]]]
Reasoning: [infer:(green bald eagle]]] The bald eagle is green. [[infr:[grreen cow)]] The cow is green. [[infer.notiin]] Nothing can be inferred from the context about the squirrel. This contradicts the goal.
Answer: False.
Figure 16: Example generation of text-davinci-008 with LOGICGUIDE on ProofWriter, where the model misformalizes assumption 13. The natural language sentence reads "if someone visits the squirrel and the squirrel ncods the bald cagle, then the squirrel is green", but the logical formulation written by the model would translate to "if someone visits the squirrel and the squirrel needs the bald eagle, then they are green" (not the squirrel is green). Like in Fig. 15, the model is not able to make any formal inferences after its second step, and we can detect that its answer was not certified.
20

---

Published in Transactions on Machine Learning Research (05/2024)
Pharmacists maintain that doctors should not be permitted to sell the medicine that they prescribe because doctors would then be tempted prescribe unnecessary medicines in order earn extra income. But pharmacists have financial interest having monopoly the sale of prescription medicines, so their objection the sale of medicines doctors cannot be taken scriously. The patient's argument proceeds by attempting to discredit a position by questioning
Patient:
motives the proponents that position rejecting questionable position on the grounds that the general public does not support that position C. pointing out an unstated assumption on which the pharmacists' argument relies and then refuting it D. asserting that pharmacists lack the appropriate knowledge to have informed opinions on the subject under discussion Answer: A
ept=3.5-turbo: In this problem, the patient presenta an argument against the objection raised by pharmacists regarding doctors selling medicines. The patient claims that the objection ion cannot be taken seriously because pharmacists have a financial interest in maintaining a monopoly on the sale of prescription medicines. To determine how the patient's argument proceeds, let's examine each option:
A. The patient's argument does question the motives of the pharmacists by suggesting that they have financial interest in the matter. However, it does not discredit the entire position of the pharmacists based solely on their motives. Therefore, option A not the correct choice.
The patient's argument does rely the fact that the general public does support the pharmacists' position. Instead, focuses on the financial interest of the pharmacists. Therefore, option B not the correct choice. unstated assumption of the pharmacists' argument and then refute it. Instead, it directly challenges the motives the pharmacists by highlighting their financial interest. Therefore, option not the correct choice.
The patient's argument does explicitly point
The patient's argument does not discuss the knowledge pharmacists or their opinions on the subject under discussion. Therefore, option
not the correct choice.
After considering all the options, we can conclude that none of the given options accurately describes how the patient's argument proceeds.
Answer: None of the options.
gpt-3.5-turbo + Base Bootstrap: Reasoning: The patient argues that the objection raised by pharmacists is not valid because they have a financial interest in maintaining monopoly on the sale of prescription medicines. Answer: A. attempting to discredit position by questioning the motives of the proponents of that position sptt33.5-trlhe + LogicGuide Bootstrap: Reasoning: The patient argues that the objection of pharmacists to doctors selling medicine cannot be taken seriously because pharmacists have financial interest in maintaining monopoly the sale of prescription medicines. Answer: A. attempting to discredit position by questioning the motives of the proponents of that position
Figure 17: Example #1 of ReClor problem. Here, the base model does very long analysis that ultimately discards option A, by questioning whether it "discredited the entire position of the pharmacist", which is irrelevant to the question. Bootstrapped models recognize the form of the argument as sufficiently matching option A.
21

---

Published in Transactions on Machine Learning Research (05/2024)
Traveler: Southern Airways far worse safety record than Air Dacentaria over the past years, in of both the frequency accidents and severity of accidents. Ttherefore, although Air Dacentaria slightly more expensive, will choose over Southern Airways for my flight from Pederton Dacenta, since it is worth paying extra to have safer flight. Which of the following, true, casts the most serious doubt on the traveler's argument?
Although the frequency accidents is greater on Southern Airways, on both airlines the proportion flights that have accidents is very small.
B. Most Southern Airways flights, but not its flight from Pederton to Dacenta, use Sarmouth airport, which because of its mountainous location is one of the world's most dangerous.
C. Only in the last few years has the cost of flying from Pederton to Dacenta been more expensive on Air Dacentaria than on Southern Airways.
D. Air Dacentaria's 's flight from Pederton to Dacenta is nonstop, whereas Southern Airways' flight touches down in Gorinda the way.
Answer: B
-pttB.5-turbo Let's analyze each of the options:
Option A states that although the frequency of accidents greater on Southern Airways, the proportion of flights that have accidents is very small on both airlines. If this is truc, it diminishes the significance of the difference safety records between the two airlines, as the overall likelihood of being in an accident is small for both.
Option claims that most Southern Airways flights, except for the one from Pederton Dacenta, use Sarmouth airport, which considered one the world's most. dangerous due to mountainous location. This information may suggest that the higher accident frequency Southern Airways might be due to use of particularly hazardous airport. However, since the traveler specifically referring to the flight from Pederton to Dacenta, this option may not significantly impact their argument.
Option C states that only in the last few years has Air Dacentaria become more expensive than Southern Airways for flying from Pederton to Dacenta. This suggests that the increased cost of Air Dacentaria might he recent change, and the traveler's decision may have been based on outdated information or prior pricing structures.
Option D mentions that Air Dacentaria's ss flight from Pederton to Dacenta is nonstop, while Southern Airways' flight makes a stop in Gorinda. If this is true, it may imply that the nonstop flight on Air Dacentaria would reduce the chances of potential accidents compared to the Southern Airways flight that involves a touch-down in Corinda.
After analyzing the options, appears that option D, which states that Air Dacentaria's 's flight from Pederton to Dacenta is nonstop, while Southern Airways' flight touches down in Gorinds, casts the most serious doubt on the traveler's argument. This information suggests that the nonstop flight Air Dacentaria could potentially offer safer flight experience even with the additional cost.
Answer: D
gpt-3.5-turbo + Base Bootstrap Reasoning: The traveler prioritizes safety over cost. Air Dacentaria slightly expensive but safer. A. This does not cast doubt on the traveler's argument, as it still supports the idea that Air Dacentaria is safer. This irrelevant
safety of Air Dacentaria and Southern Airways. C. This does not cast doubt on the traveler's argument, as still supports the idea choosing Air Dacentaria for safety reasons. D. This supports the traveler's argument, as it highlights that Air Dacentaria's flight is more convenient and potentially safer. Answer: gpt-3.5-turbo + LogieGuide Bootstrap Reasoning: The traveler's 's argument is based on the safety record the airlines. To cast doubt on the argument, we need to find information that undermines the relevance the safety record. This information does not undermine the traveler's argument, as the proportion of accidents is small on hoth airlines. B. This information weakens the traveler's argument, as the specific flight from Pederton to Dacenta is not affected by the dangerous sirport. C. This information does not undermine the traveler's argument, as the cost comparison is only relevant to the decision-making process. D. This information does not undermine the traveler's 's argument, as nonstop flights are generally considered safer. Answer: B
Figure 18: Example #2 of ReClor problem. Here, both the base model and the base boopstrapped model ignore the key connection between option B and the traveler's argument, which the SegicGuidd-boostrappee model picks up on..
22

---

Published in Transactions on Machine Learning Research (05/2024)
Dario: The government should continue to grant patents for all new drug compounds. Patents promote innovation by rewarding pharmaceutical companies for undertaking the costly research needed to develop drugs. Cynthia: Promoting innovation is certainly important. For this reason, patents should be granted only for truly innovative drugs, not for minor variants of previously existing drugs. Since it much less expensive tweak existing drug than develop wholly one, pharmaccutical companics tend focus primarily on the cheaper alternative. Dario and Cynthia disagree over whether patents should granted all drug compounds
developing truly innovative drugs costly drug patents can promote innovation pharmaceutical companies have an incentive to create minor variants of existing drugs
Answer: A
gpt-3.5-turbo: In this argument, Dario believes that the government should continue to grant patents for all new drug compounds because patents promote innovation by rewarding pharmaceutical companics for the costly research needed to develop new drugs. On the other hand, Cynthia argues that patents should only be granted for truly innovative drugs, not for minor variants of previously existing drugs. She points out that it is much less expensive to tweak an existing drug than to develop wholly new one, and pharrnacettccal companics tend to focus primarily on the cheaper alternative. Analyzing the options: A. The disagreement between Dario and Cyuthia is not about whether patents should be granted for all drug compounds. Dario supports this idea while Cyuthia argues for granting patents only for truly innovative drugs. Therefore, option A can be eliminated. B. The disagreement between Dario and Cynthia is not about whether developing truly innovative drugs is costly. They both agree that it requires costly research. Therefore, option B can be eliminated. C. The disagreement between Dario and Cyuthia about whether drug patents promote innovation. Dario believes that patents promote innovation, but Cynthia argues that they should only be granted for truly innovative drugs to effectively promate innovation. This aligns with the subject of their disagreement. Therefore, option disagreement. between Dario and Cynthia is not about whether pharmaceutical companies have incentive create minor variants of existing drugs. Both agree that concern. Therefore, option D can eliminated. Answer: C. drug patents can promote innovation
valid choice. D. The
cheaper alternative, and Cynthia specifically mentions this as a
gpt-3.5-turbo + Base Bootstrap Reasoning: Cynthia agrees that patents promote innovation thinks they should be granted only for truly innovative drugs, not for minor variants of existing drugs. Answer: D. pharmaceutical companies have an incentive to create minor variants of existing drugs
gpt-3.5-6 spt-3.5-turbo + LogieGuide Bootstrap Reasoning: Dario supports granting patents for all new drug compounds, while Cynthia believes patents should be granted only for truly innovative drugs, not for minor variants of previously existing drugs. Answer: C. drug patents can promote innovation
Figure 19: Example #3 of ReClor problem. Here, all models choose incorrect options. The model with LogieGuide bootstrap does seem to pick up the key point of disagreement, but still fails to pick the option that best describes it.
23


Reviews:
[{"review_id": "Bjrm0nz07g", "reviewer": "Reviewer_2WYM", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The motivation is clear. LogicGuide provides the following advantages :\n- Reducing content effects\n- Reliable single-step formal reasoning: LogicGuide eliminates single-hop errors. This positive impact grows with the number of hops.\n- Trustworthiness: LogicGuide makes models answer \"don't know\" when they don't have an answer, as opposed to producing unsupported guesses.\n- LogicGuide can help overcome limitations of Transformers, such as the inability to recognize *Parity*.\n- LLMs can self-improve by finetuning on self-generated texts which have been certified by LogicGuide, whereas STaR (self-taught reasoning) cannot improve because they finetune on all self-generated texts.\n- Easy integration with closed-sourced LLMs, as long as the API exposes a parameter to bias the logits on given tokens\n\nThe paper presents experiments with GPT3, GPT3.5-Turbo and LLaMA-13b, demonstrating consistent improvements of reasoning accuracy on PrOntoQA, ProofWriter and Syllogism Validity. And the reduction in contect effects is demonstrated via experiments on Syllogism Validity. \n\nThe framework of constrained semantic decoding can be naturally extended to implementing memory guide, quote guide, or algebra guide, where models can benefit from formal knowledge.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This work propose LogicGuide, a system for constrained semantic decoding (CSD), in the context of performing logic reasoning with LLMs. LogicGuide leverage formal knowledge (*guide* based on regular expressions) to constrain the decoding space for more logical generations. Specifically, given an alphabet and a partial generation, CSD leverages formal knowledge to compute a regular expression over the alphabet, which contains the set of valid continuations. A *guide* can be invoked by an LLM via a special delimiter <open delimiter> during generation. The regular expression can end in <close delimiter> to smoothly transit back to free generation. In this manner, LogicGuide supports interleaved generation of both semantically constrained decoding and free decoding.\n\nTo facilitate research in logical reasoning, this paper also introduces a new dataset, DeontiQA. The goal is to decide whether a given action is permissible, obligatory, or impermissible in the context of managing calendar events.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Figure 2, in the \"Context\" box, should premise 12 be \"If something visits the mouse then it is ***green***\" to make the reasoning chain valid? Or are there further premises that aren't shown in the figure connecting \"mouse is blue\" to \"mouse is green\"?", "broader_impact_concerns": "There isn't a major ethical concern. \n\nThis paper mentioned that LogicGuide only ensures the *correctness* of logical inferences, but not their *usefulness*. Thus, when deployed in domains such as law, such a system should still be paired with verifiers for the removal of redundant outputs.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "84LMSr8xqw", "reviewer": "Reviewer_m2Y2", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n- Clear description of the approach and its motivation\n- Experiments show benefits of using the approach both during inference time, and as a method for curating better fine-tuning data for reasoning tasks\n\nWeaknesses/uncertainties:\n- Typically, methods that rely on formalizations like this require significant hand-engineering as a tradeoff for the formal guarantees they provide. Here, it doesn't necessarily seem like LogicGuide requires this manual engineering / specification of primitives. Can you confirm this is the case? \n- Most of the datasets used appear to be synthetically generated. I.e., not natural language (a nitpick is that the term \"natural language\" should not be used to describe this data, e.g., in the section on DeontiQA which I believe is synthetically generated). Is ReClor and LegalBench using real human-written language? If not, what are the limitations of the proposed approach to noisier natural language data?", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper proposes an approach for decoding from language models that explicitly uses a formal reasoning system (Peano) to constrain model outputs. As an LM generates output, it is prompted to make calls to the formal proving system, which maintains a list of formal assumptions stated in the LM's input. Experiments show that the decoding approach improves performance for formal reasoning tasks and can also be used to improve policies via self-improvement (i.e., sampling from an LM with the guide at inference time, then using these outputs as finetuning data for the LM) even when LogicGuide isn't available at inference time.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- In Fig 2, I don't follow the logic wrt whether the mouse is blue or green?\n- Please put an example from DeontiQA in the main paper so readers can see what the dataset looks like", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "lIrvLh5Lrc", "reviewer": "Reviewer_gJ3z", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Strengths**\n\nThe paper is well-written and provides a clear and comprehensive description of the pathological phenomena that occur in automated reasoning for large language models. The use of many pedagogical examples adds to its effectiveness. While the concept of a \"guide\" is not novel, it is well-presented in this paper, with a detailed review of related work. The experimental evaluation using LogicGuide is also well-detailed, including results concerning comparative accuracies, content effects, the ability to learn from guide improvements, and the ability to generalize beyond formalized prompts.\n\n**Weaknesses**\n\nWhile Section 3 provides an understanding of guides at an informal level, some details are missing for understanding this concept at a fine-grained level. While the notion of guide described as a mapping $g$ is relatively clear, the next paragraph is very unclear:\n\n“Our idea is to use $g$ at specific points when sampling from a language model $P_{LM}(·)$ so that when the guide is invoked at a prefix $s_0$, we will sample a  continuation from $P_{LM}(s|s_0)$ that belongs to the set allowed by $g$ when given the previous guided generations in the prefix $s_0$ (e.g.,previous valid logical inferences).”\n\nFirst of all, a formal definition of $P_{LM}(\\cdot)$ would be helpful. Next, from this paragraph, it is not clear when $g$ is called. Finally, from the last sentence, it is not clear what is the prefix $s_0$. Does it include all guided generations?", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This study aims to enhance the soundness of reasoning for large language models in the context of learning-to-reason, by using a concept called “guide”. In essence, a guide is a mapping that takes the model's state and a series of formalization constraints as input, and produces a set of valid statements as output. When the model invokes the guide, the statements returned by the guide are first ranked by the model based on its prior expectations. Then, one of these statements is used to generate a new state which is then communicated back to the guide. This paper proposes LogicGuide, a guide that uses the Peano theorem prover to create step-by-step sound, first-order logical inferences. LogicGuide is empirically validated through various experiments that use different learning models (such as GPT-3, GPT-3.5 Turbo, and LLaMA13B) and different reasoning tasks (such as PrOntoQA, ProofWriter, DeontiQA, LegalBench, and ReClor).", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Section 3 could be improved for a clearer understanding of the interaction between the model (via $P_{LM}$) and the guide (via $g$).", "broader_impact_concerns": "I don't think this study on improving large language models' automated reasoning has any specific societal impacts worth mentioning.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: All reviewers are positive on the work.  There is a minor request for additional technical details in the final revision (I believe this is in reference to section 3) however all reviewers felt the paper was clear and well written -- minor points were already addressed in the revision.  I believe the concerns regarding section 3 will be addressed by the promised code/data release.
Decision: Accept (poster)