Steps towards proof construction using reinforcement learning : environments and models for hypothesis-posing as subtask creation

Despite recent advances in reinforcement learning (RL) that have allowed AI algorithms to master games such as Go from scratch, scant progress has been made on applying RL to one of the first tasks seen as susceptible to automation: theorem proving. I present steps towards training agents to construct proofs through utilizing the ability to pose hypotheses as a way to uncover information and break tasks down into subtasks. To do so, I create a novel bitstring problem that retains many of the challenges posed by proof construction while dispensing with the need to parse grammars. I then assess the performance of well-known RL algorithms on tasks derived from this problem, demonstrating that it is non-trivial. Finally, I alter a model that successfully learns one of the bitstring tasks in order to acquire results on possible mechanisms for theorem-proving prototypes.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2019

Author dc:creator

• Guo, Hairuo.

Advisor dc:contributor.advisor

• Tomaso Poggio.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/124245

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/124245