Mixture of experts learning in automated theorem proving

Abstract

The main challenge of automated theorem proving is to find a way to shorten the search process. Therefore using a good heuristic method is essential. Although there are several heuristics that improve the search techniques, studies show that a single heuristic cannot cope with all type of problems. The nature of theorem proving problems makes it impossible to find the best universal heuristic, since each problem requires a different search approach. Choosing the right heuristic for a given problem is a difficult task even for an human expert. Machine learning techniques were applied successfully to construct a heuristic in several studies. Instead of constructing a heuristic from scratch, we propose to use the mixture of experts technique to combine the existing heuristics and construct a heuristic. Since each problem requires a different approach, our method uses the output data of a similar problem while learning the heuristic for each new problem. The results show that the combined heuristic is better than each individual heuristic used in combination.