[derrak]

My cynical take on this sort of research is that we will never use raw LLMs to solve these kinds of reasoning problems and it’s therefore unclear why we bother to test them on these kinds of benchmarks.

Modern SAT solvers are completely cracked. I think there are a lot of potential synergies between such symbolic solvers and machine learning (and maybe even LLMs). But it doesn’t seem like an LLMs ability to directly solve these tasks with no symbolic tool use is going to predict the quality of these synergies.