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

[a_cubed]

Conduction? Co-induction?

Ah, yes, Tobias. I'd forgotten about him. Of course having been out of the technical side of this since about 2005 it's not that surprising I don't remember things that well, I suppose.

[purplecat]

Auto-complete just gets worst, unless you watch it like a hawk it just makes stuff up. Anyway, yes, coinduction.

I mean I know I can switch it off, it's just in the moment it never seems worth the effort of figuring out how.