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.
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
LLMs vs the Halting Problem. Why not try LLMs on the first code reasoning task: halting. Turing's undecidability proof showed basic limits. Fun bit: no matter how superintelligent AI becomes, it can never solve this. 1/5
arxiv.org/abs/2601.18987 #AcademicSky #FormalMethods #AIReasoning
arxiv.org/abs/2601.18987 #AcademicSky #FormalMethods #AIReasoning
February 2, 2026 at 1:54 PM
LLMs vs the Halting Problem. Why not try LLMs on the first code reasoning task: halting. Turing's undecidability proof showed basic limits. Fun bit: no matter how superintelligent AI becomes, it can never solve this. 1/5
arxiv.org/abs/2601.18987 #AcademicSky #FormalMethods #AIReasoning
arxiv.org/abs/2601.18987 #AcademicSky #FormalMethods #AIReasoning