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

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