DY-Star-LLMs
Collection
LLMs for automating Dolev-Yao-Star proof generation.
•
4 items
•
Updated
This model is a LoRA fine-tuned version of IBM's granite-8b-code-instruct-4k. It specializes in generating F* code, including function definitions, lemmas, and formal proofs. In their paper Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming, Saikat Chakraborty et al. (2024) use specialized code models such as StarCoder, among other LLMs, for evaluating their dataset.
The model was fine-tuned on the Singularity HPC Cluster at IIT Gandhinagar using a single 48GB NVIDIA L40S GPU. The fine-tuning scripts and console logs are available at scripts directory.
To examine the tensorboard logs for further training and eval details, use the following commands:
pip install tensorboard
tensorboard --logdir ./logs
Base model
ibm-granite/granite-8b-code-base-4k