# Steamroller Problems: An Evaluation of LLM Reasoning Capability with Automated Theorem Prover Strategies

arXiv: https://arxiv.org/abs/2407.20244 · HTML: https://mlsanity.com/paper/2407.20244/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 20 of its 46 references that are in the map.
- First posted on arXiv 17 Jul 2024.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 20 of 20)

- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [HellaSwag: Can a Machine Really Finish Your Sentence?](https://mlsanity.com/paper/1905.07830/) (2019)
- [On the Opportunities and Risks of Foundation Models](https://mlsanity.com/paper/2108.07258/) (2021)
- [HotpotQA: A Dataset for Diverse, Explainable Multi-hop Question Answering](https://mlsanity.com/paper/1809.09600/) (2018)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [PIQA: Reasoning about Physical Commonsense in Natural Language](https://mlsanity.com/paper/1911.11641/) (2019)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [The LAMBADA dataset: Word prediction requiring a broad discourse context](https://mlsanity.com/paper/1606.06031/) (2016)
- [Gemini: A Family of Highly Capable Multimodal Models](https://mlsanity.com/paper/2312.11805/) (2023)
- [A Comprehensive Overview of Large Language Models](https://mlsanity.com/paper/2307.06435/) (2023)
- [Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://mlsanity.com/paper/2402.00157/) (2024)
- [Language models show human-like content effects on reasoning tasks](https://mlsanity.com/paper/2207.07051/) (2022)
- [Deep Learning Based Text Classification: A Comprehensive Review](https://mlsanity.com/paper/2004.03705/) (2020)
- [DISC-LawLLM: Fine-tuning Large Language Models for Intelligent Legal Services](https://mlsanity.com/paper/2309.11325/) (2023)
- [Unleashing the potential of prompt engineering for large language models](https://mlsanity.com/paper/2310.14735/) (2023)
- [Are Large Language Models Really Good Logical Reasoners? A Comprehensive Evaluation and Beyond](https://mlsanity.com/paper/2306.09841/) (2023)
- [Certified Deductive Reasoning with Language Models](https://mlsanity.com/paper/2306.04031/) (2023)

## Built on by (most cited first, 1 of 1)

- [Large Language Models Imitate Logical Reasoning, but at what Cost?](https://mlsanity.com/paper/2509.12645/) (2025)

## Abstract (arXiv)

This study presents the first examination of the ability of Large Language Models (LLMs) to follow reasoning strategies that are used to guide Automated Theorem Provers (ATPs). We evaluate the performance of GPT4, GPT3.5 Turbo and Google's recent Gemini model on problems from a steamroller domain. In addition to determining accuracy we make use of the Natural Language Processing library spaCy to explore new methods of investigating LLM's reasoning capabilities. This led to one alarming result, the low correlation between correct reasoning and correct answers for any of the tested models. We found that the models' performance when using the ATP reasoning strategies was comparable to one-shot chain of thought and observe that attention to uncertainty in the accuracy results is critical when drawing conclusions about model performance. Consistent with previous speculation we confirm that LLMs have a preference for, and are best able to follow, bottom up reasoning processes. However, the reasoning strategies can still be beneficial for deriving small and relevant sets of formulas for external processing by a trusted inference engine.