Implementing Vibe Proving with Reinforcement Learning

An approach is detailed for training a Large Language Model (LLM) to generate verifiable, step-by-step mathematical proofs. The core method utilizes a reinforcement learning (RL) loop where a custom-built proof checker verifies the LLM's output and provides a binary reward signal. This process involves bootstrapping a dataset, fine-tuning an open-source model using LoRA, and running the training on the Tinker platform. While the fine-tuned models show success on many examples, they still struggle with more complex textbook proofs. The modular nature of the system allows for future improvements in areas like model choice, prompt optimization, and dataset curation.