让 E 再次智能

在这项进行中的工作中，我们展示了 ENIGMA 系统的一个新用例。使用梯度提升决策树的 XGBoost 实现的 ENIGMA 系统，已展现出实时学习引导 E 定理证明器推理的强大能力。在此，我们将 E 精简到最基本：我们用恒等关系作为最小可能的排序来替换 KBO 项排序，禁用文字选择，并用子句权重和 FIFO（先进先出）子句评估函数的简单组合来替换演化策略。我们通过实验证明，即使没有这些标准的自动定理证明器功能，ENIGMA 也能像智能的演化策略一样学习引导 E。为此，我们在十几个循环中实验了 XGBoost 的元参数。