granite-fstar-lora

Granite 8B Code fine-tuned on F*

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.

Model Details

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.

Model Description

• Base Model: ibm-granite/granite-8b-code-instruct-4k
• Fine-Tuning Dataset: dassarthak18/FStarDataset-V2-Conversation

Evaluation

To examine the tensorboard logs for further training and eval details, use the following commands:

pip install tensorboard
tensorboard --logdir ./logs

Testing Data & Metrics

• Test Loss: 0.8754
• Test Perplexity: 2.40