Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving

[purplecat]

I mentioned a while back that I was helping to supervise a PhD student who was using various symbolic AI tools to validate the output from LLMs. At the time he was using a version of Prolog, but has since switched to using a theorem proving tool called Isabell.

He recently won best paper award at Empirical Methods in Natural Language Processing (EMNLP) for his paper about this which can be found at https://aclanthology.org/2024.emnlp-main.172

Comments

[vivdunstan]

Mucho thanks!

[a_cubed]

I remember trying Isabelle out early in my PhD before finally deciding that Coq was the right tool for my job. I suspect Larry is now retired from Cambridge, so others must have taken up the baton of keeping Isabelle developing.