论文标题
对抗性学习以任意逻辑推理
Adversarial Learning to Reason in an Arbitrary Logic
论文作者
论文摘要
现有的学习方法证明定理专注于特定的逻辑和数据集。在这项工作中，我们提出了可以在没有任何人类知识或一系列问题的情况下使用的强化学习来指导的蒙特卡洛模拟。由于该算法不需要任何培训数据集，因此即使没有可用的证据甚至猜想，它也能够学习与任何逻辑基础一起工作。我们实际上证明了该方法在多个逻辑系统中的可行性。该方法比在随机生成的数据上进行训练要强，但比在量身定制的公理和猜想集中训练的方法要弱。但是，它使我们能够将机器学习应用于自动化定理，以证明许多逻辑，在此期间没有尝试约会此类尝试，例如直觉逻辑或线性逻辑。
Existing approaches to learning to prove theorems focus on particular logics and datasets. In this work, we propose Monte-Carlo simulations guided by reinforcement learning that can work in an arbitrarily specified logic, without any human knowledge or set of problems. Since the algorithm does not need any training dataset, it is able to learn to work with any logical foundation, even when there is no body of proofs or even conjectures available. We practically demonstrate the feasibility of the approach in multiple logical systems. The approach is stronger than training on randomly generated data but weaker than the approaches trained on tailored axiom and conjecture sets. It however allows us to apply machine learning to automated theorem proving for many logics, where no such attempts have been tried to date, such as intuitionistic logic or linear logic.
