Mixture Of Experts Learning in Automated Theorem Proving

Summary:

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.

Özet:

Otomatik Teorem İspatlama sistemlerinde başlıca zorluk, arama süreçlerini kısaltacak bir yöntem bulmaktır. Arama süreçlerini kısaltmak için, buluşsal yöntemleri kullanmak önemli bir rol oynar. Bu konuda yapılan çalışmaların sonucunda, çesitli buluşsal yöntemlerle başarılı sonuçlar alınmışsa da, tek bir buluşsal yöntemin tüm problem tiplerinin üstesinden gelemediği gösterilmiştir. Her problem tipinin değişik yaklaşım gerektirmesi, evrensel olarak en iyi buluşsal yöntemin bulunmasını imkansızlaştırır. Bir problem için doğru buluşsal yöntemin belirlenmesi, insan uzmanlar için bile çok zordur. Yeni bir buluşsal yöntem geliştirmek için makina öğrenmesi yöntemlerini kullanabiliriz. Bu tezde önerdiğimiz yaklaşım, sıfırdan yeni bir buluşsal yöntem geliştirmek yerine, uzmanların karışımı yöntemini kullanarak, var olan buluşsal yöntemlerin birleşiminden yeni bir buluşsal yöntem geliştirmektir. Her problem yeni bir yaklaşım gerektirdiği için, önerdiğimiz metot benzer problemlerin çözümlerini öğrenme verisi olarak kullanmaktadır. Çalışmamızın sonuçları, birleşik buluşsal yöntemin, karışımda kullanılan tekil buluşsal yöntemlerin her birinden daha iyi olduğunu göstermiştir.