Machine Learning Guidance and Proof Certification for Connection Tableaux

TL;DR

This paper presents optimized connection tableau proof search methods enhanced with machine learning guidance, including proof step reordering and Monte Carlo Tree Search, along with proof certification techniques for interactive theorem provers.

Contribution

It introduces novel machine learning-guided proof search strategies and proof certification methods for connection tableaux calculi, improving efficiency and reliability.

Findings

Optimized functional implementations of proof search.

Effective proof step reordering using Naive Bayesian probabilities.

Proof tree expansion with Monte Carlo Tree Search.

Abstract

Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: First, we show optimised functional implementations of clausal and nonclausal proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probablities, and expansion of a proof search tree with Monte Carlo Tree Search. Finally, we give a translation of connection proofs to LK, enabling proof certification and automatic proof search in interactive theorem provers.