Language Models Are Inefficient Reasoners: An Analysis on Arithmetic Proof Search
Andreas Opedal, Yanick Zengaffinen, Haruki Shirakami, Clemente Pasti, Mrinmaya Sachan, Abulhair Saparov, Ryan Cotterell, Bernhard Schölkopf
Much recent work has focused on how language models can be adapted to solve reasoning problems through search methods. To solve a task in a realistic setting, an agent often needs to search over many facts, many of which are irrelevant to said task, and do so in an efficient manner. In this paper, we investigate how language models perform in such a setting, focusing on whether they can successfully prove theorems, if they take unnecessary proof steps, and which form of search algorithm they employ. We consider a proof system for GSM-like arithmetic reasoning problems and evaluate language models on problems with a large space of arithmetic facts that are irrelevant to the task. Beyond answer accuracy, we also verify the full proof generated by the language model. This is done by measuring how well the language model output matches the most efficient ground-truth proof, which is a provably unique normal form under the proof system. We find that both standard and reasoning-oriented models perform worse on problems that have been augmented with irrelevant facts of different types. Even when they correctly prove the goal theorem, they are often inefficient, using more test-time compute than necessary. Our analysis suggests that their algorithm is closer to depth-first than to breadth-first search, and that they use information from the query as a heuristic, but that this heuristic still sometimes leads them down irrelevant paths.