Interactions between Reinforcement Learning and Mechanical Theorem Proving
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
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.
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.
Organisations
People |
ORCID iD |
Jacques Fleuriot (Primary Supervisor) | |
Mark Chevallier (Student) |
Studentship Projects
Project Reference | Relationship | Related To | Start | End | Student Name |
---|---|---|---|---|---|
EP/N509644/1 | 30/09/2016 | 29/09/2021 | |||
2096912 | Studentship | EP/N509644/1 | 31/08/2018 | 30/05/2022 | Mark Chevallier |
EP/R513209/1 | 30/09/2018 | 29/09/2023 | |||
2096912 | Studentship | EP/R513209/1 | 31/08/2018 | 30/05/2022 | Mark Chevallier |