Peter O'Hearn
@peterohearn.bsky.social
Researcher at Meta (FAIR) & Prof at UCL.
Working on AI, code and reasoning.
Separation logic, Incorrectness logic, Infer. Gödel Prize. Royal Society.
Working on AI, code and reasoning.
Separation logic, Incorrectness logic, Infer. Gödel Prize. Royal Society.
This was a great team effort with Oren Sultan, Jordi Armengol-Estapé, Pascal Kesseli, @jvanegue.bsky.social , Dafna Shahaf and
Yossi Adi. See the website www.orensultan.com/llms_halting... for more. 5/5
Yossi Adi. See the website www.orensultan.com/llms_halting... for more. 5/5
LLMs versus the Halting Problem: Revisiting Program Termination Prediction
www.orensultan.com
February 2, 2026 at 1:54 PM
This was a great team effort with Oren Sultan, Jordi Armengol-Estapé, Pascal Kesseli, @jvanegue.bsky.social , Dafna Shahaf and
Yossi Adi. See the website www.orensultan.com/llms_halting... for more. 5/5
Yossi Adi. See the website www.orensultan.com/llms_halting... for more. 5/5
Penrose claimed undecidability proved AI impossible (but didn't show humans can solve the undecidable). Turning tables: undecidability is an ideal target for heuristic LLMs. Instead of using "already crushed" problems to show limits, let's look at uncrushed problems where LLMs might help. 4/5
February 2, 2026 at 1:54 PM
Penrose claimed undecidability proved AI impossible (but didn't show humans can solve the undecidable). Turning tables: undecidability is an ideal target for heuristic LLMs. Instead of using "already crushed" problems to show limits, let's look at uncrushed problems where LLMs might help. 4/5
The surprise: LLMs are competitive on halting—where they often trail on "easier" problems. Why? Hypothesis: LLMs are heuristic approximators; in undecidability, heuristic approximation isn't just a workaround—it's often the only way forward. 3/5
February 2, 2026 at 1:54 PM
The surprise: LLMs are competitive on halting—where they often trail on "easier" problems. Why? Hypothesis: LLMs are heuristic approximators; in undecidability, heuristic approximation isn't just a workaround—it's often the only way forward. 3/5
How to approach the problem? Use SVCOMP, the home turf of symbolic reasoning tools for termination. We didn't know what we would find, and were aware of results of @rao2z.bsky.social and others showing that LLMs trail symbolic on "easier" decidable problems (propositional planning, SAT..). 2/5
February 2, 2026 at 1:54 PM
How to approach the problem? Use SVCOMP, the home turf of symbolic reasoning tools for termination. We didn't know what we would find, and were aware of results of @rao2z.bsky.social and others showing that LLMs trail symbolic on "easier" decidable problems (propositional planning, SAT..). 2/5