# Reinforced Large Language Model is a formal theorem prover

arXiv: https://arxiv.org/abs/2502.08908 · HTML: https://mlsanity.com/paper/2502.08908/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- First posted on arXiv 13 Feb 2025.

## Abstract (arXiv)

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.