Reinforced Large Language Model is a formal theorem prover

Code

• github.com/zhilingluo/theorem_prover
  Officialnone★ 3

Abstract

To take advantage of Large Language Model in theorem formalization and proof, we propose a reinforcement learning framework to iteratively optimize the pretrained LLM by rolling out next tactics and comparing them with the expected ones. The experiment results show that it helps to achieve a higher accuracy compared with directly fine-tuned LLM.

Tasks

Reproductions