Generating Domain Specific Natural Language SAT Reasoning Datasets

A key challenge for LLMs lies in their ability to reason. To evaluate an LLMs' reasoning capabilities, there is a need for challenging natural language datasets for reasoning tasks. However, it is hard to manually generate these datasets across all domains, in the scale required by LLMs, as they require expensive effort from subject matter experts. As datasets become public, they become part of the training data of LLMs leading to the need for newer datasets. In this work, we formalize the problem of synthetic generation of SAT reasoning-tasks of variable complexity in natural language that adheres to propositional logic. Then, we present our method, $\texttt{LTGen}$ (Logical Text Generator), to generate custom datasets aligned with our formalism. We test $\texttt{GPT-4O}$ and $\texttt{O3-mini}$ on two auto-generated datasets using $\texttt{LTGen}$ and find that LLMs struggle particularly on hard UNSAT problems and are biased towards predicting that the text is logically consistent.