We had two papers on this topic recently, one using a MCTS approach on formal systems (such as Lean or Metamath): https://
arxiv.org/abs/2205.11491 and one where we combine LLMs with formal provers to verify the generations: https://
arxiv.org/abs/2210.12283

→ View original post on X — @guillaumelample,