metadata
license: apache-2.0
language:
- en
base_model:
- google/byt5-small
tags:
- theorem-proving
- lean
- byt5
- mathematics
- code
Lean-ByT5
Lean-ByT5 is a ByT5-small model fine-tuned on the augmented Lean-Mathlib data for Lean theorem proving.
The model performs sequence-to-sequence generation, generating Lean tactics for a given statement goal.
Base Model
- google/byt5-small (Apache License 2.0)
Training
- PyTorch Lightning
Related Paper & Citation
For more details on the training methodology, data augmentation strategy, and dynamic sampling method used for Lean theorem proving, please refer to our paper:
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
Rahul Vishwakarma, Subhankar Mishra
arXiv:2312.14188 (cs.AI, cs.LG, cs.LO)
Paper: https://arxiv.org/abs/2312.14188
If you use this model or build upon this work, please cite:
@article{vishwakarma2023enhancing,
title={Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method},
author={Vishwakarma, Rahul and Mishra, Subhankar},
journal={arXiv preprint arXiv:2312.14188},
year={2023},
primaryClass={cs.AI}
}