OpenAI's Reinforcement Fine-Tuning Research Program

Stream: Machine Learning for Theorem Proving

[And Sha]

Next year's Open AI gives us the opportunity to make a fine-tuned for o1 through RL, we can try it for lean in two senses: 1) formulation in human language → formulation in lean language 2) statement in lean → proof in lean. To speed up the process of formalizing mathematics and automatically generating theorems and their proofs. These two things may already be in some form, but maybe they will be more effective on the o1 model. Has anyone applied for these goals already — https://openai.com/form/rft-research-program/ ?

[Alok Singh]

I asked my friend who works there and he says I can join the alpha when it comes out. I should fill out the form too though