Are Language Models Efficient Reasoners? A Perspective from Logic Programming

Thank you for the overall positive review and helpful feedback.

We can definitely include some discussion on practical implications of the results. While we did not spell this out in the paper, our findings that LMs are generally unable to distinguish relevant from irrelevant information signifies that there is room for improvement in this regard in the training paradigm of current LMs. For instance, efficiency might be improved by penalizing inefficient proofs through the reward function used for finetuning LMs with RL techniques and this could be studied in future work. We will add a discussion to the conclusion.

In response to your questions:

1. This is a great suggestion; we will make sure to include it in the final version of the paper.
2. The smallest proof is always tree-shaped because it does not contain cycles, all vertices are connected, and each premise is used at most once (by construction). We will add this clarification to the paper.
3. We actually mentioned A* in a previous draft, but decided to omit it since, in our setting, the costs of the hyperedges (or proof steps) are uniform. But we agree that it is a good idea to add it back in for the sake of contextualization in the final version of the paper, and will do so.

Thank you for the thorough review and for the structured, concrete feedback. We are happy that you appreciate the formal treatment of proof systems and the novelty and comprehensiveness of the evaluation methodology. We have incorporated most of the feedback, which definitely strengthens the paper, and respond to each of your questions below.

1. Clarify the "Distraction" Conclusion for Advanced Models:

• Thanks for noticing this. We will weaken the claim about irrelevance leading to significantly lower accuracies in the conclusion and throughout the paper, since there is only a small, nonsignificant effect for DeepSeek-R1. Regarding accuracy vs. efficiency: As you allude to, it seems like more capable models such as DeepSeek-R1 are not affected much in terms of accuracy, but they still use more tokens than they do for the corresponding base problems (i.e., those without irrelevant axioms). We created a new plot to show that this is indeed the case, which we will add to the appendix and discuss in 5.2. Thus, our findings suggest that more capable models are “distracted” only in the sense that it takes them more tokens to find the answer, but they still do, generally, find the correct answer. These findings are complementary to recent findings on “overthinking” of reasoning models. This was a helpful suggestion; we will add more discussion in the paper.

2. Distinguish Novelty from Prior Work (e.g., GSM-Logic/GSM-NoOp):

• We agree that we can improve the clarity of the methodological contributions as compared to prior work, in particular in relation to Mirzadeh et al. (2025) and Shi et al. (2023). The main innovation in our work as compared to theirs is in our method that generates problems with irrelevance automatically, whereas these papers seem to have added irrelevant statements manually. In addition, while they augmented problems from existing datasets, we created new problems from scratch. Our method thus avoids a potential bias from memorizing the efficient solution seen during training. In addition, we note the following differences to GSM-Symbolic’s No-Op dataset: (i) they seem to only include one irrelevant statement, whereas we may have multiple that could be simultaneously included as premises in the same proof; (ii) they describe irrelevance in an informal manner so the semantics of these irrelevant statements are unclear; (iii) it is hard to know further details about their setup since the details in the paper are scarce and the dataset is still not available (there is currently an open issue about this in their github repo); we will release our datasets and generation code with the final version of the paper.

• We will incorporate the above discussion into the Related Work section.

3. Formalize "Complexity" and "Lexical Overlap" Definitions:

• Thanks, this is a good point. We will revise that section to be more formal and precise. As for the two specific terms you mention, we propose the following: “Lexical overlap” between two atomic formulas can be defined as the type(s) of atom(s), if any, for which the same atom value is present in both atomic formulas. “Complexity” of the irrelevance is about hypergraph connectivity; an irrelevant axiom is one disconnected vertex in the proof, a tree is a component with multiple vertices, and “Multiple Trees” refers to multiple mutually disconnected components, each having multiple vertices. (Recall that a component is a connected subgraph that is not part of any larger connected subgraph.)

4. Provide a Complete Natural Language Problem Example:

• This is a great suggestion. We have actually already added (1) a figure in the introduction which illustrates a proof and a corresponding natural language annotation as well as (2) an example problem in natural language with the ground-truth normal-form proof and a model-generated proof to a new Appendix C.

5. Discuss Scalability of "Most Efficient Proof" for Harder Reasoning:

• It is true that the exact type of analysis we propose is restricted to settings with confluent proof systems where there exists a unique most efficient proof. With that said, many of the notions we discuss do actually carry over to more general settings. We are not sure what you mean by “open-ended reasoning” but if we think of it as a non-confluent proof system where there exist several normal forms, we could evaluate efficiency of solutions to such problems simply by the merit of being in (or close to) some normal form (i.e., a non-reducible proof). Moreover, we could still compare the number of proof steps in the different normal forms and we may be specifically interested in the proof that has the fewest, which could be checked. Indeed, math word problems may not have unique normal forms in general and we agree that it is important to make note of this limitation.

• In cases where there does not exist any normal form proof at all, it is not possible to adapt our evaluation method. In such cases you might have to resort to more crude metrics such as the number of repeated/redundant proof steps or the number of generated tokens.

• Finally, we note that our statement from the introduction that proving all possible facts could be intractable is not contradictory to there being a unique, most-efficient normal form. This statement is about proving all facts implied by the proof system, i.e., not only those relevant to a specific query.

• Thank you for raising these points; we have added a limitations section to the end of the paper and will incorporate the above discussion into that section.

Thank you for the authors' response. I now have a better understanding of the technical details of the paper. I would increase my score if no other severe issues raised by subsequent discussions.

Thank you for the review and useful feedback, and for acclaiming the paper for its novel metric, correctness, and clarity. We respond to your questions below and have made several improvements to the paper based on your feedback.

Significance: can you add statistical tests (confidence intervals or McNemar/paired bootstrap tests) for accuracy and precision to support claims of significant degradation?

Thanks, this is a great suggestion. We performed one-way ANOVA tests for the precision, recall and "precision for non-axioms" scores and found statistically significant F-scores (p < 0.001) for precision and precision for non-axioms, both for data with ground and nonground queries. Thus, we conclude that the means of these scores are different across the types of lexical overlap between irrelevant facts and the query, supporting our claim on degradation in terms of efficiency with more lexical overlap (as measured by precision). We will add this analysis to the paper.

Model diversity: can you include at least one closed‑weight frontier model (e.g. GPT‑4o) via API to check whether scaling or RLHF reduces inefficiency?

We wanted to use open-weight models in this study in order to ensure replicability, improve understanding of the results in relation to, e.g., architectural choices and training, and overall promote a culture of open science. Our frontier model of choice is DeepSeek-R1, which turns out to be less efficient in terms of tokens generated than Llama-3.1-8B-Instruct and Qwen2.5-Math-7B-Instruct (Figure 2). With that said, if you still feel that including a model like GPT-4o to the analysis is worthwhile, we will be happy to do so even if it means paying OpenAI for API access.

Semantic parser reliability: please provide an error analysis of the 5–6% unmatched proof steps; could systematic misses from the parser distort the results?

Thanks, this was a useful suggestion. We performed an analysis on the unmatched proof steps and found that most of them were on container-type predicates (i.e., statements about possession), especially for the Llama model. The majority of them were misclassified because the model gave the correct intermediate numerical answer without the arithmetic equation that implies that answer. We incorporated such cases into the parser which boosted the parsing accuracy to 99.2% for the Llama model and 97.7% for the Qwen model.

[originality] the work deals with arithmetic domain only and relies on an existing GSM generator;

While it is true that we rely on an existing GSM generator (Opedal et al., 2025), we would like to add that adapting their method to our study required some nontrivial extensions. For instance, we need to ensure that the irrelevant axioms can be used in inference rules with each other but not with the relevant ones, which is non-trivial. We have detailed some of these innovations in 4.2 and App. B, but we will make sure to better clarify these technical nuances in the final version.

[significance] the work is limited to short arithmetic proofs

To clarify, the base problems (i.e., excluding irrelevant axioms) may have up to 12 proof steps, i.e., a lot more than 3. (Note that depth is different from the number of proof steps.) Compare, for instance, to GSM8K (Cobbe et al., 2021), which includes problems with 2-8 proof steps. Moreover, the dataset can easily be extended to even longer problems if desired in future studies. To make this clearer, we created a histogram over the number of proof steps which we will add to the appendix and reference in 4.2. We will also make sure to improve the clarity regarding the data distribution more generally in that section.

Lastly, we would like to thank the reviewer for mentioning additional limitations. We have included a Limitations section at the end of the paper and will add these points in the discussion there.

Thank you for your review and feedback. We respond to your questions and reservations below.

While the controlled setup is appreciated, it may be overly simplistic and may not generalise well to real-world reasoning tasks.

Thanks for raising this point. We believe there is a natural trade-off between higher ecological validity on the one hand and a more principled/formal understanding on the other; we chose to prioritize the latter in this study. Besides, our approach has additional advantages such as mitigating data leakage, and the problems, while synthetic, are reminiscent of those found in popular datasets such as GSM8K (Cobbe et al., 2021). We take your point and will rewrite the introduction to better motivate our study.

The negative impact of irrelevant premises is a known issue, even outside rigorously defined proof systems, which may limit the novelty of the conclusions.

We agree that previous papers (Shi et al., 2023, Mirzadeh et al., 2025) have reported that irrelevant information has a negative effect on LM reasoning. Note that we make several contributions beyond these papers: (i) while previous papers analyzed problems with one irrelevant premise, often placed at the same position in the text, we provide more complex problems where there are irrelevant premises at various positions in text that can be used in further deduction; (ii) our study considers not only answer accuracy, but also proof efficiency; (iii) we have a method to automatically generate problems with irrelevant premises of various kinds, which is more scalable; (iv) we formally characterize the notion of irrelevance, which enables a more principled understanding of the findings. Thus, our study can be viewed as refining and extending findings from previous papers, which we acknowledge in the paper, e.g., at l85-7 and and l300-1. With that said, we agree that we can do a better job at this and will incorporate the above discussion into the related work section. Moreover, we would be grateful for any pointers to other related literature we may have missed that made similar contributions!

The claim that LLM proof search follows a DFS-like ordering is interesting, but the experimental evidence supporting it is not entirely convincing.

We are pleased that the reviewer also sees the value in studying search order. We do indeed find that the LM’s search order is closer to DFS than to BFS, but, for the sake of clarity, we would like to add that we additionally find evidence that LMs use a heuristic based on lexical overlap with the query, which yields a more efficient algorithm than basic DFS. That is, we did not intend to claim that they follow DFS and will revise any claims that can be perceived that way.

In Table 2, for Llama-3.1-8B under “w/ Axiom”, why is the accuracy with irrelevant axioms (60.8%) higher than the control (54.0%)? Does this suggest that irrelevant information improves performance, or is it a typo?

Thanks for this question; these numbers deserve a note in section 5.1. It does not suggest that irrelevant information improves performance, since the performance on the dataset with irrelevance is still lower than the performance on the base problems (see leftmost column). (As a reminder, the control problems have the same number of axioms as the corresponding problems with irrelevance, except with all axioms being relevant.) It appears to be an outlier; for all other models and datasets, the control accuracy is higher than the non-control one. We did not find a clear explanation for these numbers after manually looking at some of the model responses. We will clarify this point in the paper.

Could you clarify the results in Table 3? It’s unclear how the experiments demonstrate that LMs are empirically worse at proving ground theorems.

Precision gives the size of the overlap between the LM's reasoning steps and the steps in the efficient ground truth divided by the number of LM steps, while recall gives the overlap divided by the number of steps in the efficient ground truth. Precision therefore gives a score for efficiency, and recall gives a score for correctness in the steps taken. We observe generally lower scores for both precision and recall when the LMs are given ground queries. Therefore, we conclude that they are less efficient and less correct for ground queries as compared to nonground queries. We will spell this out more clearly in the paper.