Abstract

Deployment of neural networks in general is well-studied, but theorem proving has its idiosyncrasies and domain-specific requirements. Various performance metrics and constraints must be considered. Failure to do so means the next generation of theorem provers will continue to be beaten by the incumbent systems. Luckily, I have a bag of tricks for you…