purplecat: An open book with a quill pen and a lamp. (General:Academia)
purplecat ([personal profile] purplecat) wrote2024-11-27 07:05 pm

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

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
vivdunstan: Part of own photo taken in local university botanic gardens. Tree trunks rise atmospherically, throwing shadows from the sun on the ground. (Default)

[personal profile] vivdunstan 2024-11-27 10:58 pm (UTC)(link)
Mucho thanks!
a_cubed: caricature (Default)

[personal profile] a_cubed 2024-11-28 12:52 am (UTC)(link)
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.