[hackinthebochs]

SAT solvers are programs designed such that their execution corresponds to the reasoning process of satisfying some given constraints. But they do not contain the reasoning process, rather they embody it.

LLMs are different in that they operate on semantic features of program state. Embedding vectors assign semantic features to syntactical structures of the vector space. Operations on these syntactical structures allow the LLM to engage with semantic features of program state directly. Here the reasoning process is contained within as an object of manipulation. An LLM sensitive to the semantic features of the input sequence and that examines the logically permissible moves to derive a new sequence closer to the intended sequence (some statement to prove) just is engaging in reasoning.