Formalizing the proof of PFR in Lean4 using Blueprint: a short tour

Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ... by jhanschoo on Wednesday December 06, 2023 @07:24AM (#38542920)

This suffers from the problem of sparse rewards. You need a better reward that gives value to intermediate results or special-case answers, since too few states are correct.

[ Parent | on HN ]

Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ... by t_mann on Thursday December 07, 2023 @12:55PM (#38559487)

It's not about training the model. You just input the error messages together with an appropriate prompt and ask it to fix it. Iterate until it verifies successfully (or stop after you've reached ~1-2x content window length).

Once you have produced examples of correct math that way, you can use those to fine-tune the model.

[ Parent | on HN ]