ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3

We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…