Neural guidance improves theorem prover performance within specific domains
Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Logic in Computer Science
Summary
The paper studies using AI to help a computer program called Vampire that proves math and logic statements. They find that AI helps Vampire do better on similar kinds of problems but struggles when used across different problem types. Training a single AI model on all problem types at once allows Vampire to perform well on all of them. Combining AI guidance with other methods still helps, but the improvements become smaller.
What this means in practice
- •For software verification engineers: Improve automated proof tools to verify software correctness more reliably within specific problem domains.
- •For formal methods tool developers: Build theorem proving tools that adapt AI guidance models trained on diverse datasets to maintain performance across multiple problem areas.
Authors
Karel Chvalovský, Martin Suda, Josef Urban
Abstract
A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies. We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. This can be remedied by training a single model on all datasets at once. Such a model, although more expensive to obtain, helps Vampire almost catch up in performance across all datasets. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.