A new method stops AI models from making up answers when a problem cannot be solved.
Researchers built a pipeline where a language model translates a problem into a formal specification, then hands it to a symbolic solver for the actual logic work. The catch: if the translation is wrong, the solver dutifully solves a problem nobody asked for. Past systems only flagged translations that crashed, staying silent whenever the program ran but produced nonsense. The new approach instead extracts a minimal unsatisfiable core, the exact bundle of constraints that cannot all hold together, and hands that proof back to the model. Tested on a new 77-problem benchmark with a known correct answer for each case, the translation step held up faithfully on six of seven problem domains, tripping up only on aggregate coverage scheduling.
That one weak spot matters less than the headline number. Feeding a weaker model the minimal core instead of a bare error message cut its rate of fabricated answers to infeasible problems from 79 percent down to 7 percent. Notably, a strong chain-of-thought model without any solver matched the symbolic pipeline's accuracy on its own. The real payoff here is not correctness, it is a system that can show its work and admit when a problem has no answer.
Solvers have always been the trustworthy part of these hybrid setups; the translation step was the weak link nobody audited. This paper is a reminder that bolting a formal solver onto an LLM only helps if the handoff between them is formalized too.