Collaborative Automated Reasoning in Shen: Formal Planning, Type-Theoretic Verification, and Symbolic Proof with ChatGPT and THORN

[dr.mt...@gmail.com]

Such is the catchy title of a new paper; but there's a lot there to interest Shenturions.

THORN, as you know, is the hyperfast theorem prover that comes as a Shen download.  It shares the limitation of all uniform-method ATPs which is the tendency to be swamped by the dreaded combinatorial explosion when faced with difficult proofs.

A solution to this is proof planning which drastically cuts search space by using problem decomposition - breaking a hard problem into a series of simpler ones.  The paper shows how to integrate ChatCPT with THORN in a type-secure way using dependent types in Shen to guarantee the plan is type safe (i.e a plan which if it works will secure the original theorem).

The payoffs from proof planning, when it works, are spectacular,  as ChatGPT remarks at the end of the paper.

.... by introducing explicit formal plans — carefully curated sequences of lemmas and controlled construction of the knowledge base ... we were able to collapse proofs that would have required days or millenia of brute-force computation into seconds.

This paper is perhaps a very early example of a co-authored paper paper where one of the co-authors is not human.

Mark