{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/124245"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/124245","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Steps towards proof construction using reinforcement learning : environments and models for hypothesis-posing as subtask creation","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Guo, Hairuo."],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Tomaso Poggio."],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019","date_published":"2019","updated_at":"2026-07-22T22:20:51Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"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."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/124245","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Tomaso Poggio."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Guo, Hairuo."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2020-03-24T15:36:07Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2020-03-24T15:36:07Z"]},{"key":"dc:date.issued","label":"Date","values":["2019"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/124245"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 37-38)."]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Steps towards proof construction using reinforcement learning : environments and models for hypothesis-posing as subtask creation"]}]}],"canonical_facts":{"dc:contributor.advisor":["Tomaso Poggio."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Guo, Hairuo."],"dc:date.accessioned":["2020-03-24T15:36:07Z"],"dc:date.available":["2020-03-24T15:36:07Z"],"dc:date.issued":["2019"],"dc:description":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 37-38)."],"dc:description.abstract":["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."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/124245"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"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."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Steps towards proof construction using reinforcement learning : environments and models for hypothesis-posing as subtask creation"],"dc:type":["Thesis"],"thesis:degree_name":["Master"]},"updated_at":"2026-07-22T22:20:51Z"}