Learning Formal Mathematics From Intrinsic Motivation

arxiv:2407.00695

Original source · Paper JSON

Agents, open-endedness, AGI · 2024-06-30

Cites (0) · Cited by (1)

Complete cleaned Markdown · Source Markdown including bibliography

Read in parts

1. Part 1
2. Part 2
3. Part 3
4. Part 4
5. Part 5

Contents

• Learning Formal Mathematics From Intrinsic Motivation
• Abstract
• 1 Introduction
• 2 Related Work
• Mathematical conjecturing.
• Learning to prove theorems from human data.
• Learning to prove theorems from synthetic data.
• Intrinsic motivation
• Self-improvement of language models
• 3 Minimo
• 3.1 Conjecturing
• 3.2 Proof Search
• 3.3 Hindsight Relabeling
• 3.4 Training loop
• 4 Experiments
• 4.1 Learning dynamics
• Difficulty increases as training progresses (RQ1).
• Proof policy improves as training progresses (RQ2).
• Hindsight relabeling is necessary for joint self-improvement (RQ3).
• 4.2 Proving human-written theorems (RQ4)
• 5 Limitations and Conclusion
• Acknowledgments
• Appendix A Training details
• Appendix B Proof log-likelihood and MCTS Expansions
• Appendix C Fraction of provable conjectures across iterations
• Appendix D Axioms
• D.1 Arithmetic
• D.2 Propositional Logic
• D.3 Groups
• Appendix E Extrinsic evaluation problems
• E.1 Arithmetic
• E.2 Propositional Logic
• Appendix F Discussion: extension to other proof assistants
• NeurIPS Paper Checklist
• Instructions for reporting errors