rahul3613/lean_byt5

Lean-ByT5

Lean-ByT5 is a ByT5-small model fine-tuned on the 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}
}