TL;DR: A Lean 4 theorem-proving dataset, where these theorems are used to validate the correctness of LLM mathematical reasoning steps, synthesized using Safe.
The official implementation of our paper Safe (Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification) and its associated datasets FormalStep.
Paper
Code
Dataset
If you find our work useful, please consider citing our paper.… See the full description on the dataset page:
https://huggingface.co/datasets/artisdom/FormalStep.
