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.

[vivdunstan]

I think Larry is retiring now. I’m friends on Facebook with his wife Elena, and she posted pics recently from a leaving do. Though whether he retires fully is another matter.

[purplecat]

Yes, I'm Facebook friends with Larry and he definitely posted about retiring in the last couple of months.

[a_cubed]

Larry actually has a Wikipedia page. He's now 68 so is in the retirement bracket. Yes, he may well stay emeritus and keep doing research and some supervision.

[purplecat]

I also experimented with Isabelle since it had a formalisation of conduction. The interface has improved massively since then, with a much more intuitive "assuming X then Y follows by Z" kind of syntax which Xin was exploiting (I don't honestly think he had much understanding of the details of Isabelle - Z was generally blast (one of the built-in automated reasoning algorithms).

Larry handed over most of the development of Isabelle to Tobias Nipkow while I was still in Edinburgh (or possibly Tobias just gradually took it on - certainly by the turn of the century I'd say Tobias was clearly driving much of the development). I'm not sure who is running it now, digging around the details of Isabelle 2024, suggests Larry and Tobias are still overall in charge but most of the development work is being done by others and there is some organisation called Isabelle CTO that seems to coordinate this in some way.

[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.