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:

bash

pip install tensorboard
tensorboard --logdir ./logs

Testing Data & Metrics

Test Loss: 0.8754
Test Perplexity: 2.40

dassarthak18/granite-fstar-lora

Granite 8B Code fine-tuned on F*

Model Details

Model Description

Evaluation

Testing Data & Metrics

dassarthak18/
granite-fstar-lora