论文标题
再次使E聪明
Make E Smart Again
论文作者
论文摘要
在进行的这项工作中，我们为谜团展示了一个新的用例。使用XGBOOST实施的渐变决策树的谜团系统表明，可以实时指导EREM定理的推论。在这里，我们将E剥离到裸露的骨头：我们将KBO术语排序替换为身份关系，作为最小可能的排序，禁用文字选择，并以条款重量和FIFO的简单组合（首先是首先出现）条款评估功能替换演变的策略。我们通过实验表明，即使没有这些标准的自动定理私有功能，谜也可以学会指导E以及智能，进化的策略。为此，我们在十几个循环中尝试了XGBoost的元参数。
In this work in progress, we demonstrate a new use-case for the ENIGMA system. The ENIGMA system using the XGBoost implementation of gradient boosted decision trees has demonstrated high capability to learn to guide the E theorem prover's inferences in real-time. Here, we strip E to the bare bones: we replace the KBO term ordering with an identity relation as the minimal possible ordering, disable literal selection, and replace evolved strategies with a simple combination of the clause weight and FIFO (first in first out) clause evaluation functions. We experimentally demonstrate that ENIGMA can learn to guide E as well as the smart, evolved strategies even without these standard automated theorem prover functionalities. To this end, we experiment with XGBoost's meta-parameters over a dozen loops.
