FLARE: Faithful Logic-Aided Reasoning and Exploration

## Abstract

Abstract Modern Question Answering (QA) and Reasoning approaches based on Large Language Models (LLMs) commonly use prompting techniques, such as Chain-of-Thought (CoT), assuming the resulting generation will have a more granular exploration and reasoning over the question space and scope.
However, such methods struggle with generating outputs that are faithful to the intermediate chain of reasoning produced by the model.
On the other end of the spectrum, neuro-symbolic methods such as Faithful CoT (F-CoT) propose to combine LLMs with external symbolic solvers.
While such approaches boast a high degree of faithfulness, they usually require a model trained for code generation and struggle with tasks that are ambiguous or hard to formalise strictly. We introduce F aithful L ogic- A ided R easoning and E xploration ( FLARE ), a novel interpretable approach for traversing the problem space using task decompositions. We use the LLM to plan a solution, soft-formalise the query into facts and predicates using a logic programming code and simulate that code execution using an exhaustive multi-hop search over the defined space.
Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers. Our methods achieve SOTA results on 𝟕 7 \mathbf{7} bold_7 out of 𝟗 9 \mathbf{9} bold_9 diverse reasoning benchmarks.
We also show that model faithfulness positively correlates with overall performance and further demonstrate that FLARE allows pinpointing the decisive factors sufficient for and leading to the correct answer with optimal reasoning during the multi-hop search.

## 1 Introduction

Complex Reasoning in natural Question Answering (QA) tasks assumes the capability to explore the problem space of the designated query with a formalised set of facts, relations, commonsense knowledge and logical implications.
In line with this, LLMs have been enhanced with CoT (Wei et al., ) prompting, which supplements the QA process by generating intermediate reasoning chains given a set of in-context examples (Brown et al., ), as shown in Figure 1.
This allowed for advancement in commonsense (Madaan et al., ), symbolic (Wang et al., ; Sprague et al., ) and mathematical (Jie et al., ) reasoning.
Although CoT allows for a problem exploration in natural language steps, such an approach has been shown to cause performance degradation for nuanced reasoning tasks involving multi-hop planning (Valmeekam et al., ; Suzgun et al., ), problem exploration (Yao et al., ) and arithmetic (Hendrycks et al., ; Madaan & Yazdanbakhsh, ).
These discrepancies arise as CoT suffers from a limited ability to decompose, search, verify and backtrack using intermediate rationale chains (Yao et al., ), cascading hallucinations and errors (Ling et al., ) and that natural language might not be an optimal representation for describing the reasoning process (Li et al., ).
Simultaneously, LLM output has been shown to be unfaithful and inconsistent w.r.t. the intermediate CoT rationale (Jacovi et al., ; Lanham et al., ; Turpin et al., ).

Figure: Figure 1: A depiction of the *plan*, *code* and simulated *search* in FLARE. Each module has a breakdown of the relevant components composed by the LLM explained in Section 2.
Refer to caption: x1.png

To circumvent the problem of CoT faithfulness and allow for more robust reasoning during QA, Xu et al. (, Faithful CoT) suggested generating code which is further executed using an external symbolic solver.
Producing and executing code allows one to both create an output that can be conditioned on heuristic search in the problem space and perform backtracking.
However, strict translations of natural language queries into code, such as autoformalisation (Szegedy, ; Wang et al., ), is a non-trivial task involving direct inference of implicit commonsense and domain-specific knowledge and the ability to align abstract and informal concepts directly to constrained formal definitions for further execution (Wu et al., ).
An example query *“Do all parts of the aloe vera plant taste good?”* seen in Figure 1 is not trivial to formalise, nor to provide a strict algorithmic solution for it, making it much more suitable for soft reasoning.
Using external solvers makes such fuzzy reasoning impossible and requires consistently generating syntactically correct executable code.
While some LLMs have coding capabilities stemming from their pretraining (Jiang et al., ; Aryabumi et al., ), relative code consistency is more probable with models explicitly trained for coding (Chen et al., ).

To overcome these problems with CoT and F-CoT, we propose Faithful Logic-Aided Reasoning and Exploration (FLARE), an interpretable method that allows for planning, fuzzy reasoning, and traversing the problem space with backtracking, exact task decomposition, and measuring faithfulness.
In FLARE, given a natural language query, we prompt an LLM to sequentially generate a *plan* that includes an analysis and the logical steps necessary for formalising and answering the question, a logical programming Prolog (Wielemaker et al., ) *code* that allows formalising the query into a set of facts, relations and their composition forming the problem space and the *search* which is an LLM generated simulation of exhaustive multi-hop traversal of that space from the code.
An illustration of FLARE can be seen in Figure 1.
In our framework, the generated code must not be consistently executable by an external solver, allowing for the soft-formalisation of natural language. Although we see that even generalist LLMs are able to produce executable code in $\geq 50\%$ of cases.
FLARE allows us to measure the faithfulness of the outcome w.r.t. the simulated multi-hop logical traversal by directly comparing the search paths generated from executable Prolog code to that LLM generation. This comparison also allows for pinpointing model hallucinations and inconsistencies.
We systematically study the effectiveness of our method using $4$ general-purpose LLMs of varying scales across $9$ diverse benchmarks, covering Math World Problems, Multi-hop QA and Relation inference and show that our method achieves state-of-the-art results in $7$ out of $9$ in comparison to CoT and F-CoT. We also show that the method is rather competitive for models tuned for coding, with an average overall increase of $16\%$ over F-Cot and $9\%$ over CoT. Our findings show that model accuracy strongly correlates with the faithfulness of the reasoning process towards the problem space. We also provide ablations showing that the model can interpretably pinpoint hallucinations, search degeneracies, and the limitations of the search over the problem space.
Our key contributions are the following:

- •
We introduce FLARE a novel paradigm for logic-aided and interpretable formalisation and search over the problem space in QA and reasoning tasks.
- •
We perform a systematic evaluation across $9$ benchmarks and $4$ models of varying scales, showing the advantages of using FLARE for QA in a few-shot setup over prior approaches.
- •
The modularity of FLARE allows defining a simple ingrained method for measuring model faithfulness and shows that it is strongly correlated with performance.
- •
We further show that using FLARE allows us to interpretably and rigorously detect hallucinations along with sub-optimal and inconsistent reasoning patterns.

## 2 Faithful Logic-Aided Reasoning and Exploration

### 2.1 LLM Simulated Search

FLARE comprises three modules for generating a *plan*, *code* and simulated *search* for answering a natural language query $\mathcal{Q}=\{T_{1}\dots T_{|\mathcal{Q}|}\}$, where each $T_{i}$ is a token.

#### Generating A Plan

For each query $\mathcal{Q}$, given an LLM $\mathcal{M}$, we initially prompt it to generate a *plan*, $\mathcal{P}$, which should be comprised of task explanation, analysis and a plan for further formalising the query. An example of this can be seen in the *plan* section in Figure 1. We use in-context few shot examples $\mathcal{E}_{\mathcal{P}}$ of such *plan* generations along with greedy decoding for obtaining the final plan.

$$ $\displaystyle\mathcal{P}_{i}\sim\operatorname*{arg\,max}p_{\mathcal{M}}(T_{i} \mid\mathcal{E}_{\mathcal{P}},\mathcal{Q})$ (1) $$

#### Generating Code

After generating the *plan*, we prompt the LLM $\mathcal{M}$ to generate a Prolog code $\mathcal{C}$, an example of which can be seen in Figure 1. We append executable code generation samples $\mathcal{C}_{\text{sample}}$ to the previous in-context examples $\mathcal{E}_{\mathcal{P}}$ and obtain few-shot code generation demonstrations $\mathcal{E}_{\mathcal{C}}=[\mathcal{E}_{\mathcal{P}};\mathcal{C}_{\text{sample
}}]$

$$ $\displaystyle\mathcal{C}_{i}\sim\operatorname*{arg\,max}p_{\mathcal{M}}(T_{i} \mid\mathcal{E}_{\mathcal{C}},\mathcal{Q},\mathcal{P})$ (2) $\displaystyle\mathcal{F}_{\text{\emph{code}}},\mathcal{R}_{\text{\emph{code}}} ,\mathcal{G}_{\text{\emph{code}}}=\text{EXTRACT}(\mathcal{C}_{i})$ $$

#### Benefits of Prolog

Prolog is a symbolic logic-programming engine (Bowen, ) used for heuristic search over Horn Clauses (Chandra & Harel, ). It is a declarative programming paradigm (Lloyd, ), meaning that the code is expressed as the logic of computation. In particular, this logic is formalised as a set of facts $\mathcal{F}$ and relations $\mathcal{R}$ forming our problem space, while the final goal $\mathcal{G}$ is a first-order logic combination of them. As a default, Prolog uses a depth-first search (DFS) strategy (Bowen, ) for sub-goal decomposition and feasible traversal of the problem space that satisfies the goal $\mathcal{G}$. Such a traversal is referred to as the *trace*. At each trace step, the program can either confirm or invalidate the sub-goal using the feasibility of fact and relation combinations, expand the search tree or retry satisfying a failed sub-goal with new combinations. An example of such a search can be observed in Figure 1.
It is possible to complete an exhaustive search, exploring all possible paths that do or do not satisfy the goal.
These characteristics are beneficial as we can explicitly access and segment the facts and relations that form the problem space and the search strategy used for query formalisation. As Prolog is declarative, it is sufficient to use a regexp heuristic for the segmentation, which is referred to as EXTRACT in Equation 2 and Equation 3.
Furthermore, including exhaustive traversal traces in-context allows the LLM to simulate sub-goal decomposition, backtracking, intermediate goal invalidation, etc. We discuss this in more depth in the next paragraph.

#### Simulating Search

After generating the logic-programming *code*, we want to simulate program execution by generating a problem space traversal trace with our LLM $\mathcal{M}$. We update our in-context samples by appending search traces $\mathcal{S}_{\text{sample}}$ constructed from Prolog execution of sample codes $\mathcal{C}_{\text{sample}}$, i.e. $\mathcal{E}_{\mathcal{S}}=[\mathcal{E}_{\mathcal{C}};\mathcal{S}_{\text{sample
}}]$.

$$ $\displaystyle\mathcal{S}_{i}\sim\operatorname*{arg\,max}p_{\mathcal{M}}(T_{i} \mid\mathcal{E}_{\mathcal{S}},\mathcal{Q},\mathcal{P},\mathcal{C})$ (3) $\displaystyle\mathcal{A}_{\text{\emph{search}}},\mathcal{F}_{\text{\emph{ search}}},\mathcal{R}_{\text{\emph{search}}}=\text{EXTRACT}(\mathcal{S}_{i})$ $$

During iterative problem space traversal, we can segment the facts $\mathcal{F}_{\text{\emph{search}}}$, relations $\mathcal{R}_{\text{\emph{search}}}$, completed and backtracked paths with their answers $\mathcal{A}_{\text{\emph{search}}}$ used during the search simulation. To get the final answer we update in-context samples with the correct final answers $\mathcal{A}_{\text{sample}}$ from the executed search $\mathcal{S}_{\text{sample}}$, $\mathcal{E}_{\mathcal{A}}=[\mathcal{E}_{\mathcal{S}};\mathcal{A}_{\text{sample
}}]$.

$$ $\displaystyle\mathcal{A}_{\text{\emph{Final}}}\sim\operatorname*{arg\,max}p_{ \mathcal{M}}(T_{i}\mid\mathcal{E}_{\mathcal{A}},\mathcal{Q},\mathcal{P}, \mathcal{C},\mathcal{})$ (4) $$

The prompts used for generating each part in FLARE can be seen in Appendix A.

### 2.2 Detecting Reasoning Inconsistencies

For each query $\mathcal{Q}$ given the *code* $\mathcal{C}$ and the simulated *search* $\mathcal{S}$ along with the extracted facts $\mathcal{F}_{\text{\emph{code}}},\mathcal{F}_{\text{\emph{search}}}$ and relations $\mathcal{R}_{\text{\emph{code}}},\mathcal{R}_{\text{\emph{search}}}$ from each designated module, we aim to detect the inconsistencies during the reasoning process of the LLM. We use exact string matching between all these facts and relations in *code* and simulated *search*.

$$ $\displaystyle\forall i,\exists j\quad\text{such that}\quad\mathcal{F}_{\text{ code}}^{i}=\mathcal{F}_{\text{search}}^{j}\quad\text{and}\quad\forall v, \exists q\quad\mathcal{R}_{\text{code}}^{v}=\mathcal{R}_{\text{search}}^{q}$ (5) $\displaystyle\forall j,\exists i\quad\text{such that}\quad\mathcal{F}_{\text{ code}}^{i}=\mathcal{F}_{\text{search}}^{j}\quad\text{and}\quad\forall q, \exists v\quad\mathcal{R}_{\text{code}}^{v}=\mathcal{R}_{\text{search}}^{q}$ (6) $$

With this framework in mind, we define two reasoning failure modes.
In the *first* failure mode, given that some fact or relation was used in the simulated *search* but did not exist in the generated *code*, i.e. $\exists j\text{ such that }\mathcal{F}_{\text{search}}^{j}\notin\mathcal{F}_{
\text{code}}$, we claim that the LLM has *hallucinated*. We postulate that the model either produced incomplete knowledge during formalisation to *code* or created a piece of non-existing information during the *search*. We do not consider facts that emerged during a direct inference step within the simulated search during our calculation. For example, if we are dealing with a mathematical query $4\cdot(5+6)=?$, the search would involve separately evaluating the expression $5+6=11$. In this case, $11$ will not be treated as a hallucinated fact within the search but rather as an emergent fact obtained from direct inference.
The *second* failure mode is the reciprocal case, where a fact or relation present in the *code* is not used during the *search*. We refer to this phenomenon as *sub-optimal reasoning* as it shows that the LLM could not explore the problem space completely or injected unsuitable knowledge during formalisation into *code*.

Table: Table 1: The following table shows the performance of each of the tested models given a technique for reasoning. Each bold, underlined, and italicised element highlights the best, second best and worst technique per specific model. The overall best method per dataset is highlighted in green.

### 2.3 Measuring Faithfulness

We propose a method to measure the faithfulness of the LLM reasoning process when using FLARE. As mentioned in Section 2.1, for each query in a dataset $\mathcal{D}=[\mathcal{Q}_{1},\dots,\mathcal{Q}_{|\mathcal{D}|}]$, we generate a set of codes $\Phi=[\mathcal{C}_{1},\dots,\mathcal{C}_{|\Phi|}]$ and simulated problem space searches $\Psi=[\mathcal{S}_{1},\dots,\mathcal{S}_{|\Psi|}]$. We use the Prolog engine to execute all of the codes $\Phi$ and obtain a set of correctly written programs $\Phi^{\prime}$ and exact search paths $\Psi^{\prime}$. As we do not require explicit programmatic correctness during inference in FLARE for any code $\mathcal{C}_{i}$, some Prolog executions resulting in an error are filtered out in $\Psi^{\prime}$. To assess model reasoning faithfulness towards code formalisations, we compare the search paths $\Phi^{\prime}$ obtained from Prolog execution with their designated counterparts $\Phi_{\text{\emph{gen}}}^{\prime}$ generated by the LLM from the same code. We use ROUGE (Lin, ) to compute the matching score for each executed and simulated search path. In particular, we use ROUGE-Lsum, which uses the longest common subsequence (LCS) over each line to obtain the final score. This method fits our cause as a line in a Prolog search execution represents a single logic step within the traversal. This allows us to measure the similarity of the reasoning contents and structure in exact and simulated searches.

## 3 Experimental Setup

### 3.1 Datasets

To evaluate FLARE, we use a benchmark of $9$ tasks that cover Math Word Problems (MWP), multi-hop QA and relation inference. For testing numeric and mathematical reasoning, we follow CoT (Wei et al., ) by including GSM8K (Cobbe et al., ), SVAMP (Patel et al., ), MultiArith (Roy & Roth, ), ASDiv (Miao et al., ) and AQuA (Ling et al., ). Among these, GSM8K, SVAMP, MultiArith and ASDiv cover elementary and middle school arithmetic word problems with a set of integers or decimals as the answer. AQuA is a multiple-choice numerical, symbolic reasoning dataset where each answer is a mathematical expression containing notations, values and expressions not defined in the query.
We also test FLARE using three multi-hop QA datasets. We use StrategyQA (Geva et al., ), which is a boolean QA task that requires sub-goal decomposition and a multi-hop reasoning strategy to answer. The example *“Do all parts of the aloe vera plant taste good?”* used in Figure 1, is taken from StratedyQA. The multi-hop QA testing also includes Date and Sports Understanding, subsets of BIG-Bench (bench authors, ). The tasks involve inferring an exact date given some calculations in the relative time period and understanding if an artificially created sports statement is feasible.
Finally, we assess FLARE on Relational Inference using CLUTRR (Sinha et al., ), which involves inferring the familial relation between two entities mentioned in a natural language description of the partial family graph.
We adopt the same in-context samples used in (Xu et al., ; Wei et al., ). The complete descriptions, statistics and examples for each dataset can be found in Table 7 in Appendix A.

Figure: Figure 2: The trend of mean model accuracy w.r.t mean faithfulness (ROUGE-Lsum) for all the models. Faithfulness is positively correlated with model performance.
Refer to caption: x2.png

### 3.2 Benchmarks

We compare FLARE with CoT (Wei et al., ) as a prompting method that reasons using natural language chains and with F-CoT (Xu et al., ) that formalises the query into a code and offload the reasoning to an external symbolic solver. We use Llama3.1 (8B) (Dubey et al., ), CmDR (30B) (Cohere, ), CmDR+ (100B) (Cohere, ) and GPT3.5 (Brown et al., ) ($\geq 100B$ (Ye et al., )). As the coding model OpenAI Codex (code-DaVinci-002) (Chen et al., ) used in F-CoT has been deprecated, we replace it with the new GPT3.5 as suggested by OpenAI and recalculate the results accordingly.

## 4 Results

### 4.1 Main Results

Table: Table 2: The table shows the accuracy of an LLM with FLARE compared to prompting for a final answer directly after generating (plan-only) a plan $\mathcal{P}$.

Figure: Figure 3: The figure shows the percentage of executable code per model (right) and the accuracy of the executable code when answering the queries (left).
Refer to caption: x3.png

To evaluate FLARE, we use a set of models of varying sizes on diverse benchmarks, as defined in Section 3. We compare the performance of each model while using FLARE, CoT and F-CoT prompting. The results for F-CoT and CoT on all the models are computed using the codebase of the original study (Xu et al., ).

#### LLMs for general reasoning

Our results, presented in Table 1, show that using FLARE allows the LLMs to achieve state-of-the-art results on $7$ out of $9$ datasets, with an average $28\%$ increase over CoT. We can see a clear trend that FLARE increases the performance compared to CoT and F-CoT for all the models of varying scales. We also see that LLMs that are not explicitly tuned for coding suffer massive degeneracies when using F-CoT. We postulate that they are unable to consistently produce executable programs that satisfy a predefined scheme in F-CoT, thus resulting in an error during execution. This further highlights the value of simulating program execution using an LLM instead of using external solvers.
The results show that using FLARE yields more benefit on datasets that require longer chains of multi-hop and symbolic reasoning, like AQuA and StrategyQA.

#### LLMs for code generation

To understand the effect of FLARE on models tuned for coding, we use GPT3.5 (Brown et al., ) as it was the OpenAI suggested succession model for Codex (Chen et al., ) which is used in F-CoT and possesses strong coding capabilities (Ye et al., ). The results in Table 1 show that using FLARE is beneficial for models that are tuned for coding and boost the accuracy with a $16\%$ increase over F-CoT and $9\%$ over CoT. The reason is that many natural language queries with non-trivial formalisations are more suited to be tackled with more commonsense soft reasoning than direct code execution. This is evident in Table 1 where FLARE and CoT are consistently better than F-CoT in StrategyQA, Sports and CLUTRR.
The opposite case of numeric and algorithmic heavy reasoning tasks is also covered by FLARE as it maintains strong performance similar to F-CoT on MWP problems Table 1.
Consequently, FLARE allows combining algorithmic formalisation with simulated soft-reasoning, circumventing the pitfalls of using a deterministic external solver while still producing a query formalisation and problem space traversal.

### 4.2 Is simulating search useful?

To understand if simulating a search over the problem space is useful, we compare the performance of FLARE where we only generate the *plan* without the subsequent *code* or *search* components. We refer to this framework setup as *plan-only*, which can be seen in Figure 1 if we were to use only the *plan* for answer generation. We completed this ablation using CmDR, CmDR+, and GPT-3.5, and we used GSM8K, AQuA, and StrategyQA as our baselines. The results in Table 2 confirm that all of the models suffer massive performance degradation from $61.1\rightarrow 49.9$ when omitting the *code* and the *search* components of FLARE. We hypothesise that this is caused by insufficient problem space exploration when using the *plan-only* setting.
Furthermore, we have already seen in Table 1 that in methods, like F-CoT, that do not use simulated problem space exploration for soft-reasoning and only rely on *plan* and *code*, the performance also deteriorates even resulting in a complete breakdown of reasoning over the designated datasets. This can be viewed as a constrained version of FLARE with *code-only* execution.
Consequently, our results show that simulating problem space traversal is highly beneficial as it avoids the pitfalls posed by *plan-only* and *code-only* modes by exploring the problem space more rigorously and soft-reasoning during that traversal instead of using external solvers.

### 4.3 Faithful Reasoning Improves Performance

Table: Table 3: The table depicts the difference in the average explored paths, hops, and fails during the reasoning process, which leads to incorrect or correct answers. The purple colour illustrates that incorrect reasoning paths have fewer explorations that led to Failed search paths.

As described in Section 2, using FLARE allows us to measure the faithfulness of the LLM reasoning process by comparing the simulated problem space traversals ${\Phi}^{\prime}_{\text{\emph{gen}}}$ with actual traces ${\Phi}^{\prime}$ produced from a symbolic Prolog solver. To do this, we initially compute the percentage of syntactically correct executable code each LLM produces. We can see from the right part of Figure 3 that all of the models are capable of producing correct executable Prolog code in $67\%$ of cases on average and $\geq 50\%$ of cases at the very least. This shows that the simulated searches ${\Phi}^{\prime}_{\text{\emph{gen}}}$ can be considered a representative sample that will be further used to accurately measure the faithfulness of the simulated search w.r.t. the generated code. After measuring the reasoning faithfulness for each model, we want to understand what impact it has on the performance of the LLM. In Figure 2, we segment the models w.r.t. their ROUGE-Lsum scores. The results show that model performance is strongly positively correlated with reasoning faithfulness.
However, we also observe in the left part of Figure 3 that executing semantically precise code results in an accurate answer only in $47\%$ of cases on average. Indeed, having a simulated search trace with a ROUGE-Lsum faithfulness score of $1$, would be equivalent to simply executing the program as proposed in F-CoT. Yet we have priorly shown that F-CoT struggles with reasoning tasks that are hard to formalise and require multi-hop commonsense and soft reasoning.
These two discoveries show that optimal LLM reasoning, conditioned on a search in the problem space, should be increasingly faithful toward the facts, relations and the search strategy defined within the code while simultaneously maintaining the capability for soft-reasoning along more abstractly defined concepts. Our results show that FLARE allows LLMs to maintain a similar reasoning capacity.

### 4.4 What is important during the search?

Table: Table 4: The table shows how the percentage of unique emergent inferences in search, overlapping relations between code and search, and unused relations in code impact answer correctness.

We expand the analysis of the simulated search traces to detect the reasons which can lead to optimal reasoning within an LLM. For this purpose, we calculate several statistics, like the average number of explored paths, average and total hops and failures per path, for each model during the simulated traversal. The failure in a path is an invalidation of a solution for a sub-goal explored during the search, which is used for backtracking, as explained in Section 2. Calculating these statistics is simple as the *search* component of FLARE, seen in Figure 1, is a structured simulation of a Prolog trace, where each line contains a hop of reasoning inference.
We split these statistics for the reasoning paths that lead to correct or incorrect outcomes. Our results in Table 3 show that LLM performance and reasoning optimally are not directly connected to the amount of explored paths or multi-hop inferences per path. We also see that traces that lead to incorrect answers have a higher number of failures per path and in total. We explain this phenomenon with the hypothesis that LLMs with traces that were optimal for reasoning and led to correct answers could skip exploring degenerate solutions due to strong commonsense reasoning capabilities.
Further analyses focus on identifying inconsistencies and failure modes (Section 2.2). By comparing relations in code with those in search traces, we measure emergent hallucinations and unused relations, highlighting areas of sub-optimal reasoning. Additionally, we assess the uniqueness of emergent facts per inference hop, which indicates the extent of problem-space exploration (Table 4).
The results in Table 4 show consistently over each model that, on average, traces that lead to correct answers had a higher percentage of unique emergent facts and overlap in the relations used between the code and search, while the portion of underutilized relations was lower. This means that optimal reasoning with an LLM requires a great degree of problem-space exploration with fewer relation hallucinations during the search and more relation utilization from the defined code. This aligns with our prior discoveries, which show a strong correlation between simulated search faithfulness towards the formalised code and model performance. Our framework FLARE has these reasoning patterns ingrained within its inference pipeline.

Figure: Figure 4: The effect of the model parameter scale from 8B to 100B+ on model accuracy (left) and faithfulness (right).
Refer to caption: x4.png

### 4.5 The effect of scale

Table: Table 5: The table shows the changes in simulated search statistics when using FLARE w.r.t model scale from 8B to 100B+. Hallucinations refer to facts and predicates only used in trace, while unutilised knowledge relates to the facts and relations only seen in the code.

We want to assess the impact of the number of parameters in the model on the overall performance and faithfulness. The results in Figure 4 show no precise relation between model scale, performance and faithfulness. However, scaled models from the same family, i.e. CmDR (30B) and CmDR+ (100B), show improvements in reasoning faithfulness and model performance. We can also see in Table 5 that as the model size increases, the average number of hops and the portion of hallucinations and unutilised knowledge decreases. This further confirms our prior assumptions that models with strong commonsense soft-reasoning capabilities can skip steps during the search while maintaining the knowledge and structure of the traversal strategy outlined in the code.

## 5 Related Work

#### Reasoning in Natural Language

Few-shot prompting (Brown et al., ) has been shown to be an effective approach for increasing the reasoning capabilities of LLMs in natural language generation (Gehrmann et al., ; Reif et al., ; Sanh et al., ). LLM reasoning can be further enhanced with prompting techniques such as CoT (Wei et al., ), which attempts to segment reasoning into explicitly written intermediate steps. Concurrent work has also proposed that models *“think step by step”* (Kojima et al., ), or divide the problem into subtasks before the solution (Zhou et al., , Least-to-Most). These approaches have been shown to suffer from arithmetic inaccuracies (Lewkowycz et al., ; Hendrycks et al., ) and reasoning inconsistencies (Madaan & Yazdanbakhsh, ). Further attempts have been made to add a planning stage before reasoning by dividing the process into recursive plan formulation and execution steps (Yao et al., ; Wang et al., ). The *plan* generation step in FLARE is a hybrid technique inspired by these methods but focused on generating a natural language strategy for formalising the query into code.

#### Reasoning with Search

Several lines of work propose using techniques to expand the reasoning paths over the problem space. Self-consistency decoding (Wang et al., ) is an approach used to sample many natural language reasoning paths and take a majority vote for an answer. Another popular approach is Tree-of-Thoughts (ToT, Yao et al. ()), which proposes to explore the problem space with reasoning similar to a tree traversal, where each state is created and evaluated using an LLM. Similar techniques try to adapt symbolic search approaches akin to DFS, BFS (Besta et al., ), A^∗ (Lehnert et al., ) or other combinations (Gandhi et al., ) with direct tuning (Lehnert et al., ), imitation training (Yang et al., ) or few-shot prompting (Zhang et al., ). It must be noted that all of these techniques have only been tested in constrained mathematical puzzle-solving and algorithmic domains like the 24 Game (Yang et al., ), Countdown (Wikipedia, ), Sorting (Besta et al., ), maze solving (Yang et al., ), Sokoban (Lehnert et al., ) and others.
Although the *search* component of FLARE has some similarities to these techniques, we argue that our method allows for generalistic reasoning with interpretable multi-hop search through iterative logic-based problem space exploration.

#### Reasoning with Formalisation

Another line of research has tried formalising natural language queries into code (Gao et al., ; Li et al., ) or pseudo-code (Chae et al., ; Gandhi et al., ). This allows the translation of the query into a strict structure and offloads the reasoning and search components to deterministic solvers like Python Chen et al. (), PDDL Xu et al. (); Liu et al. (), DataLog Xu et al. () and others. While models are reasonably capable of synthesising programs (Austin et al., ; Nijkamp et al., ) and benefit from the use of code in numerical and algorithmic reasoning settings (Chen et al., ; Gao et al., ), the usage of code for general QA has not been rigorously explored. The reasons are that formalisation from natural language into a strict and executable code is challenging (Wu et al., ), following the exact syntactic constraints of the programming language not abundantly used during pre-training is onerous (Liu et al., ) and can require models explicitly tuned for coding (Chen et al., ). Using an external solver for reasoning also limits the capability for soft reasoning in commonsense knowledge and implications. Although we formalise the natural language query into a logic programming Prolog program during the *code* generation part of FLARE, we do not explicitly require the code to be executable and do not use external solvers during inference. This allows for the further use of the LLM for soft-reasoning to simulate code execution in a logic-based problem space traversal similar to Prolog while circumventing the need for code tuning a generalist model.

#### Reasoning Faithfulness

An explanation is considered *faithful* if it explicitly and accurately describes the reasoning process of the model during inference (Gilpin et al., ; Jacovi & Goldberg, ). In the context of prompting techniques such as CoT, we are interested in the faithfulness of the intermediate reasoning chains towards the final output. Faithful intermediate reasoning chains should not just look *plausible* (Herman, ) but have exact reflections of the problem exploration and reasoning used to arrive at the final answer. Natural language reasoning chains prevalent in CoT and similar methods are shown to be unfaithful, either masking the reasoning biases (Turpin et al., ) of the model or outright ignoring the intermediate reasoning (Lanham et al., ). In FLARE, we introduce a method to seamlessly measure the faithfulness of the final outcome w.r.t. completed search.

## 6 Conclusion

This work introduces FLARE, a novel approach for logic-aided interpretable formalisation and reasoning with simulated search over the problem space. We show that models of varying scales obtain state-of-the-art results compared to prompting paradigms like CoT and F-CoT. We further pinpoint that using FLARE allows us to perform soft-reasoning with simulated search, making it flexible for diverse reasoning benchmarks. We introduce a method to measure model reasoning faithfulness w.r.t. the problem formalization ingrained within FLARE. Our results show that model performance is positively correlated with the faithfulness of the reasoning process. The systematic studies of the method show the benefits of using simulated search compared to natural language reasoning and external symbolic solvers. We further show that using FLARE allows us to interpretably and rigorously detect hallucinations and sub-optimal and inconsistent reasoning patterns.

## Reproducibility Report

To reproduce the results of our study, we provide the complete codebase, processing pipelines and prompts for each dataset. The only model hyper-parameter we explicitly fix is the temperature for greedy decoding. We also make the inference of all of the models using FLARE, F-CoT and CoT across all of the datasets publicly available for further experimentation and exploration.

## Acknowledgments

$\begin{array}[]{l}\includegraphics[width=28.45274pt]{figures/LOGO_ERC-FLAG_EU.
jpg}\end{array}$
Erik is partially funded by a DFF Sapere Aude research leader grant under grant agreement No 0171-00034B, as well as by a NEC PhD fellowship.
Pasquale was partially funded by ELIAI (The Edinburgh Laboratory for Integrated Artificial Intelligence), EPSRC (grant no. EP/W002876/1), an industry grant from Cisco, and a donation from Accenture LLP.
Isabelle’s research is partially funded by the European Union (ERC, ExplainYourself, 101077481).
This work was further supported by by the Pioneer Centre for AI, DNRF grant number P1, the Edinburgh International Data Facility (EIDF) and the Data-Driven Innovation Programme at the University of Edinburgh.

## Appendix A Appendix

### A.1 LLM Prompts

We define straight-forward prompts for generating *plan*, *code* and *search* simulation in FLARE, which can be observed in Table 6.

### A.2 Dataset Statistics

The datasets used in this study encompass a variety of domains, specifically targeting the performance of the models in interpreting Math Word Problems, multi-hop question answering, and relational inference. Table 7 provides a detailed breakdown of each dataset, including the number of few-shot in-context samples (shots), the number of test samples, and representative examples from each dataset. The datasets provide a comprehensive basis for evaluating the models’ abilities to handle complex tasks across different domains, facilitating an in-depth analysis of model performance under few-shot conditions.

Table: Table 6: Table of Prompts for Plan, Code, Simulated Search, and Final Answer generation for GSM8K (Cobbe et al., ).

Table: Table 7: The statistics and examples of the datasets used in benchmarking. Shots refers to the number of few-shot in-context samples used during benchmarking.

## Peer Reviews

confidence: 4
contribution: 2
initial_rating: 3
presentation: 2
questions: 1) It would be helpful to include the notations for equations (Eq. (1)-(4)) and explanations for figures (e.g., Figure 1) to enhance readability and logical flow. Additionally, there are a few specific points that may benefit from clarification. For example, $T$ as a single token in query $Q$ is misused in Eq. (1)-(4). In Eq. (4), there might be a redundant comma or a missing variable.

2) In Section 3.1, the Simulating Search section might benefit from additional details. Specifically, elaborating on how a problem space traversal trace is formed would be valuable. Including a detailed description, pseudocode, or examples could provide further clarity. It would also be helpful to include a detailed explanation of the backtracking mechanism.

3) The complete process could be further clarified by explaining the steps following inconsistency detection and faithfulness measurement. For example, it would be valuable to know if a best-of-n selection, weighted voting or other strategies are used to decide the final answer. A pseudocode of the entire framework could also enhance understanding here. In addition, it's better to include some full examples for inconsistency detection and faithfulness measurement.

4) The framework may benefit from adaptive capabilities. Currently, the plan generation is done in one pass without a feedback loop. Introducing a mechanism to refine the generated code if errors are detected during subsequent simulation could also improve adaptability.

5) For simulating Prolog execution, the choice to use LLMs over an external solver might benefit from further clarification. Understanding the reasoning behind using an LLM-based simulation instead of an external solver, particularly in terms of handling the self-bias of LLMs, would be insightful.

6) Since Prolog is tailored for rule-based logical reasoning, the specific adaptations for solving math word problems need to be clarified. Further implementation details and example outputs could illustrate the achieved improvements and highlight the framework's effectiveness.

7) It would be valuable to expand the evaluation to include other general methods, such as Tree of Thought, Program of Thought, and Self-Consistency, alongside comparisons to similar methods [1-3]. Additionally, for Llama-3.1-8B, CmDR, and CMDR+, the F-CoT results are zero. Could the authors provide more context on this outcome?

8) Code and data are not provided for reproducibility.

Reference:

[1] Pan, Liangming, et al. "Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning." The 2023 Conference on Empirical Methods in Natural Language Processing.

[2] Yang, Sen, et al. "Neuro-symbolic integration brings causal and reliable reasoning proofs." arXiv preprint arXiv:2311.09802 (2023).

[3] Xu, Fangzhi, et al. "Symbol-LLM: Towards foundational symbol-centric interface for large language models." arXiv preprint arXiv:2311.09278 (2023).
soundness: 2
strengths: Improving LLM-based reasoning with neuro-symbolic integration is a good research problem. Empirical results are given.
summary: This paper introduces Faithful Logic-Aided Reasoning and Exploration (FLARE) to enhance the interpretability and faithfulness for LLM-based reasoning. FLARE uses task decomposition and logic programming to guide LLMs. It combines planning with logical reasoning, where the query is formulated into structured facts and predicates, and then explored through an exhaustive multi-hop search within a defined problem space. At the end, there are some reasoning inconsistencies detection and faithfulness measurement.
weaknesses: The writing could benefit from adjustments to improve clarity, strengthen notation, and correct typos. The advantages of using LLMs to simulate Prolog execution are ambiguous. Some key design and implementation details are missing. Code and data are not provided for reproducibility.

---

confidence: 5
contribution: 3
initial_rating: 6
presentation: 2
questions: 1. Considering that DFS can become computationally intensive as search depth increases, and that appending search traces to prompts may risk exceeding the LLMs' context length, how do you manage the generated Prolog program to avoid an unacceptable search space?
2. Would it be possible to set a faithfulness threshold and continue the simulated search only until this threshold is met (i.e., early stopping)? Testing this approach could make the way to faithfulness calculation more convincing.
soundness: 4
strengths: 1. The authors address limitations in current methods, which either struggle to maintain faithful, consistent reasoning steps or fail to handle fuzzy reasoning for difficult-to-formalize problems. They tackle these issues with a soft-formalization approach and a simulated search mechanism.
2. Unlike F-CoT, their approach doesn’t require programming expertise or additional fine-tuning for the LLMs. The LLMs aren’t required to generate perfectly accurate code but instead simulate Prolog execution internally, bypassing the need for an external interpreter.
3. The use of Prolog encourages the LLM to explicitly outline facts and relations in its reasoning, enhancing control and enabling verification of correct fact and relation usage, which helps reduce hallucinations.
4. Prolog’s DFS feature ensures thorough exploration of the problem space, increasing the likelihood of finding the correct answer.
5. The experiments are well-designed and thorough, demonstrating the method’s effectiveness with results that surpass or match those of CoT and F-CoT. The ablation study results for simulated search align well with expectations.
6. The correlation between faithfulness and reasoning performance is effectively highlighted through experimental results, supporting the model’s interpretability and reliability.
summary: This paper presents a reasoning framework capable of answering fuzzy and multi-hop questions while ensuring transparency in its reasoning steps. The framework achieves this through three key phases: task decomposition, soft formalization, and simulated search. In the first phase, the LLM is prompted to analyze the question and generate a structured plan for subsequent formalization. Following this, the LLM translates the question into ProLog programs according to the provided plan, called "soft formalization." Finally, the framework searches for answers by simulating a depth-first search over the problem space, essentially emulating Prolog execution within the LLM. This structured pipeline allows the framework to detect inconsistencies in reasoning by examining the facts and relationships used during inference. Additionally, it assesses the faithfulness of the reasoning process by comparing the actual execution paths to simulated paths generated by the LLM. Their methods achieved SOTA performance on 7 out of 9 common reasoning benchmarks.
weaknesses: 1. The paper would benefit from more detailed examples to illustrate how the simulated search operates and how it benefits intermediate reasoning steps.
2. There is no theoretical analysis of search complexit. If complexity analysis isn’t feasible for certain fuzzy problems, a time cost comparison between FLARE and baseline methods (e.g., CoT and F-CoT) would be a useful alternative.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 4
questions: - Could FLARE’s framework extend to other tasks that require complex reasoning? Insights on its limitations in such settings would be helpful.
- The method seems to work more reliably on LLaMa 8b and CmDR rather than on GPT3.5. Is there a reason why? 
- The framework seems to fail on sports and date Q&A - some insight into why that happens would be useful. 
- Is it true that if the model outputs a Prolog code that is not executable (or wrong syntax), it's not possible do any error detection or faithfulness measure? 
- Can you please summarize the 'characteristic' of problems for which the method is applicable and for which kind of problems it is not applicable?
soundness: 3
strengths: - The prompting technique proposed in the paper is very interesting for tasks that are hard to fully formalize yet it can benefit from a semi-formalized approach for logical reasoning. 
- The framework seems to reliably improve accuracy on multi-hop QA and MathWord tasks and it is relatively easy to adapt to new problems with just writing few shot examples.
-  The faithfulness metric proposed by the paper seems to correlate well with accuracy which can be used to "weigh" after multiple samples from the model to get more reliable results. This metric also provides a proxy for how reliable the answer is in a very simple way. 
- The paper is very well written and easy to read.
summary: This paper introduces a new method named FLARE for logic-aided reasoning of LLMs using a semi-formal language that is not necessarily executable to allow flexibility. The model is given a problem and proceeds in 3 steps:

1. Generate a natural language plan given few-show examples. 
2. Model is prompted to generate a Prolog code given few-shot examples. In this step, the problem is decomposed into set of facts $F$, relations $R$, and a goal $G$.
3. The model is prompted to $\textbf{simulate}$ the execution of the code generated in stage 2 via prompting. This simulation is later used to detect reasoning inconsistencies and measuring faithfulness (to the intermediate reasoning steps) of the model. 

There are 2 failure modes in reasoning inconsistencies. First is when a fact or a relation that was not in the Prolog code from step 2 is used in step 3. Second is when a fact or a relation in the code is $\textbf{not}$ used in the reasoning steps, which authors classify as "sub-optimal reasoning."

Authors demonstrate that such prompting with language models such as CmDR and GPT-3.5 results in stronger accuracies on various Q&A and mathematical reasoning benchmarks. The paper has extensive evaluation demonstrating that simulating search and writing code is actually necessary for the performance increase and faithfulness of the generated text/code correlates with the accuracy of the results.
weaknesses: - Although the method seems powerful for QA tasks, its adaptability to harder algorithmic and reasoning tasks seem difficult.
- The authors run experiments with GPT3.5 rather than GPT4o or GPT4o-mini which makes applicability to SoTA models questionable. 
- Although the framework increases performance, it does not have the benefits a fully formal system that has guarantees. However, I believe this is okay as they target problems for which it's difficult if not impossible to have guarantees.

---

confidence: 4
contribution: 3
initial_rating: 8
presentation: 3
questions: 1) How cost effective is the proposed method over baselines methods since a lot of search is needed?
2) How effective is the proposed method over the methods like LLM + external symbolic solver such as LogicLM [1] ?
3) As mentioned in the cons section, can you please show the effectiveness of proposed method on more complex logical reasoning datasets?

[1] Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
soundness: 3
strengths: 1) The paper is generally is well written with crisply defined mathematical notations and easy to follow presentation of authors works
2) Experimentation section of the paper is sound demonstrating the effectiveness of the proposed method
summary: Authors introduce a new logic aided interpretable formalization search propmting mechanism namely FLARE, where given a query a plan is generated by the LLM following which a logical prolog code is generated given the plan which is simulated with multihop search.
weaknesses: 1) Expensive: Given that the LLMs have been used for planning, code generation and the execution of code via multi-hop search, instead of relying on symbolic solvers, this might increase the cost for computation. 
2) Weak baselines: Experiments have been performed with relatively simpler datasets. Authors should experiment with more complex datasets that are already present in the literature for question answering such as LogiQA [1], PrOntoQA [2],  ProofWriter [3] 
3) Figures: Figure 1 present in the paper is too cluttered and hard to read. Please break it down so that it is easy to read or please add a more detailed explanation in the appendix
4) Prompt Templates: Ideally since the proposed method is a prompting method, prompt templates are necessary to evaluate the performance of the proposed method in detail but Appending A2 does not include and since there is no supplementary material provided with paper, it is hard to effectively judge the paper in total.

[1] LogiQA: A Challenge Dataset for Machine Reading Comprehension with Logical Reasoning
[2] Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought
[3] ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language

Meta-review: This work investigates a prompting workflow for solving reasoning tasks where a problem is formalized as a logic program but its execution is simulated by a language model rather than delegated to an external solver, which theoretically trades precision for coverage, and allows quantifying the extent to which the language model is faithfully simulating the solver. An advantage of this is that it allows a more careful experimental study of reasoning breakdowns: Does reasoning fail due to failures of formalization or failures of execution? It also leads to modest gains across benchmarks, at least against the baselines considered. The weaknesses of the paper are that it is effectively a prompting pipeline, and it foregrounds the engineering results instead of the scientific insight that might be obtained by experimental study of reasoning breakdowns, as well as problems with the baselines described below. 

It is particularly unclear that the baselines are fair: The authors are unable to reproduce strong numbers from various baselines, and instead present lower numbers that they themselves generated. *This might not be the author's fault!* Perhaps the original papers got it wrong. But it should give pause, especially been combined with the fact that *their reproduction of F-CoT does not even do the minimal check of filtering programs for syntactic correctness*, leading this baseline to have a misleading "0%" accuracy. Given that they extend the same grace to their own method (from the rebuttal), it is hard to have a charitable interpretation of the baseline numbers.

The biggest reason to reject the paper is because of these issues with the baselines. There are other reasons as well, such as the fact that it is essentially a prompting pipeline with an emphasis on the engineering result instead of scientific insight, and that the engineering itself is not particularly methodologically novel.

Decision: Reject