Saved in:
Bibliographic Details
Main Author: Luo, Zhiling
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2502.08908
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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.