Verifying LLM Answers with ShZZaM and ATP

A Chat with Bard

LLM vs. ATP

ShZZaM

• The ShZZaM ZigZag Loops
• ShZZaM in Action
• The Implementation
• Testing with various examples ... TPTP, SUMO, MATP, PWC, FOLIO, ...

Observations and Questions

• Can ShZZaM be trusted? Maybe not!
• Can ATP be trusted?
• The Cycle of Trust
• Natural and Useful Proofs