Interactions between Reinforcement Learning and Mechanical Theorem Proving

强化学习与力学定理证明之间的相互作用

• 批准号: 2096912
• 金额: --
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2018
• 资助国家: 英国
• 起止时间: 2018 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2096912
• 关键词: Interactions; between; Reinforcement; Learning; Mechanical

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.

本研究项目的目的是研究强化学习技术的理论和使用以及机械定理证明技术的理论和使用之间可能的相互作用。从一个方向来看，这可能涉及使用强化学习来改进机械定理证明过程中建议的逻辑步骤，理想情况下，增强它能够实际解决的问题类别。在另一个方向，人们可以使用定理证明来正式验证支撑强化学习的理论，并理想地建立在这个阶段可能未经证明但仅在实践中观察到的有用属性和限制。这两组方法之间的一些交互也可能增强强化学习，可能通过允许它“相信”其环境的逻辑属性并将逻辑规则应用于它们，从而可能避免计算工作量和时间-这些信念可以在适用的情况下通过进一步的强化学习过程继承。