Summary of Formal Theorem Proving by Rewarding Llms to Decompose Proofs Hierarchically, By Kefan Dong et al.
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
by Kefan Dong, Arvind Mahankali, Tengyu Ma
First submitted to arxiv on: 4 Nov 2024
Categories
- Main: Machine Learning (cs.LG)
- Secondary: None
GrooveSquid.com Paper Summaries
GrooveSquid.com’s goal is to make artificial intelligence research accessible by summarizing AI papers in simpler terms. Each summary below covers the same AI paper, written at different levels of difficulty. The medium difficulty and low difficulty versions are original summaries written by GrooveSquid.com, while the high difficulty version is the paper’s original abstract. Feel free to learn from the version that suits you best!
| Summary difficulty | Written by | Summary |
|---|---|---|
| High | Paper authors | High Difficulty Summary Read the original abstract here |
| Medium | GrooveSquid.com (original content) | Medium Difficulty Summary This paper explores the ability of large language models (LLMs) to write proofs in formal languages that can be verified by automated proof evaluation. Unlike previous approaches, this work trains LLMs to decompose theorems into lemmas and prove them without providing pre-written lemmas as input. The authors design a reinforcement learning-based training algorithm that encourages the model to propose novel lemmas and prove them, even if the theorem is too challenging at the moment. The reward mechanism is inspired by how mathematicians train themselves, giving credit for proposing correct and novel lemmas. During training, the model proposes and proves new lemmas that are not in the training dataset, with 37.7% of the training replay buffer consisting of newly-proposed correct lemmas extracted from Archive of Formal Proofs (AFP). The RL-trained model outperforms supervised finetuning, achieving a pass rate of 45.5% on the AFP test set and 39.5% on an out-of-distribution test set. |
| Low | GrooveSquid.com (original content) | Low Difficulty Summary This paper is about helping computers learn to write math proofs in a way that people can check if they’re correct. Right now, most computer programs just give the computer pre-written answers, but this isn’t very challenging or realistic. Instead, researchers are training computers to break down problems into smaller parts and prove each part step by step. The new method is inspired by how humans learn math, giving credit for making progress even if the final answer isn’t reached yet. The trained computer can propose new ideas and prove them, with many of these new ideas being correct. This shows that computers are getting better at doing math on their own. |
Keywords
» Artificial intelligence » Reinforcement learning » Supervised
