Grounding Neural Inference with Satisfiability Modulo Theories

For example, a prediction market on whether GPT -4 will be able to consistently solve "easy" Sudoku puzzles from the LA Times has remained open for several months at the time of