InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918164827209728 |
|---|---|
| author | Wu, Zijian Huang, Suozhi Zhou, Zhejian Ying, Huaiyuan Yuan, Zheng Zhang, Wenwei Lin, Dahua Chen, Kai |
| author_facet | Wu, Zijian Huang, Suozhi Zhou, Zhejian Ying, Huaiyuan Yuan, Zheng Zhang, Wenwei Lin, Dahua Chen, Kai |
| contents | Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_15700 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search Wu, Zijian Huang, Suozhi Zhou, Zhejian Ying, Huaiyuan Yuan, Zheng Zhang, Wenwei Lin, Dahua Chen, Kai Artificial Intelligence Computation and Language Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook. |
| title | InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search |
| topic | Artificial Intelligence Computation and Language |
| url | https://arxiv.org/abs/2410.15700 |