Interactions between Reinforcement Learning and Mechanical Theorem Proving

本研究项目的目的是考察强化学习技术的理论和使用与机械定理证明技术的理论和使用之间的可能交互。在一个方向上，这可能涉及使用强化学习来改进在机械定理证明过程中提出的逻辑步骤，理想地提高它能够实际解决的问题的类别。在另一个方向，人们可以使用定理证明来正式验证支撑强化学习的理论，并且理想地建立在该阶段可能未被证明但仅在实践中观察到的有用的性质和限制。也可能两组方法之间的一些交互作用可以增强强化学习，可能是通过允许它“相信”其环境的逻辑属性并将逻辑规则应用于它们，或许因此绕过了计算工作和时间--这些信念可以被进一步的强化学习过程所继承，如果适用的话。

The purpose of this research project is to examine possible interactions between the theory and use of reinforcement learning techniques and the theory and use of mechanical theorem proving techniques.Taken in one direction, this could involve using reinforcement learning to improve the logical steps suggested during mechanical theorem proving, ideally enhancing the class of questions it is able to practically tackle.In the other direction, one could use theorem proving to formally verify the theories underpinning reinforcement learning and ideally establish useful properties and limitations which might at this stage be unproven but only observed in practice.It is also possible that some interaction between the two sets of methods could enhance reinforcement learning, possibly by allowing it to "believe" logical properties of its environment and apply logical rules to them, perhaps thus circumventing computational effort and time - these beliefs could be inherited by further reinforcement learning processes where applicable.