Partial Label Learning for Automated Theorem Proving
This work addresses the challenge of improving theorem proving efficiency for AI and formal verification researchers, but it appears incremental as it applies existing methods to a new domain.
The paper tackles the problem of learning guided Automated Theorem Proving by formulating it as Partial Label Learning, providing a theoretical framework for handling alternative proofs, and demonstrates that using methods from Partial Label Learning tends to increase performance in learning assisted theorem provers, though no concrete numbers are provided.
We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework for dealing with alternative proofs during learning. We use the plCoP theorem prover to demonstrate that methods from the Partial Label Learning literature tend to increase the performance of learning assisted theorem provers.