Finetuning.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "ae1a180e",
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "def install_dependencies():\n",
    "    !pip install -Uqq  git+https://github.com/huggingface/peft.git\n",
    "    !pip install -Uqq transformers datasets accelerate bitsandbytes\n",
    "    !pip install -Uqq wandb\n",
    "    !pip install torch torchvision torchaudio|\n",
    "    !pip install sentencepiece\n",
    "# uncomment the following line to install the required dependencies\n",
    "# install_dependencies()\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ccbe0cb5",
   "metadata": {},
   "outputs": [],
   "source": [
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "1536ac98",
   "metadata": {},
   "outputs": [],
   "source": [
    "import torch\n",
    "from transformers import LlamaTokenizer, LlamaForCausalLM\n",
    "torch.cuda.is_available()\n",
    "\n",
    "\n",
    "model_path = 'openlm-research/open_llama_3b_v2'\n",
    "\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "eff66b81",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "6251f983",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "You are using the default legacy behaviour of the <class 'transformers.models.llama.tokenization_llama.LlamaTokenizer'>. This is expected, and simply means that the `legacy` (previous) behavior will be used so nothing changes for you. If you want to use the new behaviour, set `legacy=False`. This should only be set if you understand what it means, and thouroughly read the reason why this was added as explained in https://github.com/huggingface/transformers/pull/24565\n"
     ]
    }
   ],
   "source": [
    "tokenizer = LlamaTokenizer.from_pretrained(model_path,add_eos_token=True)  \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "d88f000c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "eos_token_id: 32000\n"
     ]
    }
   ],
   "source": [
    "tokenizer.add_special_tokens({'eos_token':'<eos>'})\n",
    "print('eos_token_id:',tokenizer.eos_token_id)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "b5b8d657",
   "metadata": {},
   "outputs": [],
   "source": [
    "def tokenize(prompt, tokenizer):\n",
    "    result= tokenizer(\n",
    "        prompt+\"<eos>\",  # add the end-of-stream token\n",
    "        padding=\"max_length\",\n",
    "        max_length=2048,\n",
    "        truncation=True\n",
    "    )\n",
    "\n",
    "    return {\"input_ids\": result[\"input_ids\"], \"attention_mask\": result[\"attention_mask\"]}\n",
    "    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "54f59635",
   "metadata": {},
   "outputs": [],
   "source": [
    "from datasets import load_dataset\n",
    "data = load_dataset(\"csv\", data_files= \"C:/Users/Kevin Zhang/Documents/GitHub/dafny/dataset.csv\", split='train[:400]')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "367d4a33",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Dataset({\n",
       "    features: ['incorrect_program', 'verifier_output', 'correct_program'],\n",
       "    num_rows: 400\n",
       "})"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "data"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8a6e4e8c",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "bc85e80a",
   "metadata": {},
   "outputs": [],
   "source": [
    "train_val = data.train_test_split(test_size=len(data)//5, shuffle=True, seed=42)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "323bc900",
   "metadata": {},
   "outputs": [],
   "source": [
    "train_data = train_val[\"train\"]\n",
    "test_data = train_val[\"test\"]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "a854190f",
   "metadata": {},
   "outputs": [],
   "source": [
    "def generate_prompt(data_point): \n",
    "    return f\"\"\"Below is an incorrect Dafny program and the corresponding error output from the Dafny verifier. Assume that the program specification is correct, and the program implementation is wrong. Correct the program so that is satisfies the specification and fixes the verifier error.\n",
    "    \n",
    "### Incorrect Dafny Program:\n",
    "{data_point[\"incorrect_program\"]}\n",
    "    \n",
    "### Error output from the verifier:\n",
    "{data_point[\"verifier_output\"]}\n",
    "\n",
    "### Corrected program:\n",
    "{data_point[\"correct_program\"]}\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "fa6706f8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Below is an incorrect Dafny program and the corresponding error output from the Dafny verifier. Assume that the program specification is correct, and the program implementation is wrong. Correct the program so that is satisfies the specification and fixes the verifier error.\n",
      "    \n",
      "### Incorrect Dafny Program:\n",
      "include \"../Wrappers.dfy\"\n",
      "include \"../Functions.dfy\"\n",
      "include \"../Collections/Sequences/Seq.dfy\"\n",
      "include \"Unicode.dfy\"\n",
      "// UnicodeEncodingForm.dfy\n",
      "\n",
      "\n",
      "abstract module {:options \"-functionSyntax:4\"} UnicodeEncodingForm {\n",
      "  function IsMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (b: bool)\n",
      "    ensures b ==> |s| > 0 && forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i])\n",
      "    decreases |s|\n",
      "\n",
      "  function SplitPrefixMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (maybePrefix: Option<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures |s| == 0 ==> maybePrefix.None?\n",
      "    ensures (exists i | 0 < i <= |s| :: IsMinimalWellFormedCodeUnitSubsequence(s[..i])) <==> true && maybePrefix.Some?\n",
      "    ensures maybePrefix.Some? ==> true && var prefix := maybePrefix.Extract(); 0 < |prefix| <= |s| && prefix == s[..|prefix|] && forall i | 0 < i < |prefix| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i])\n",
      "\n",
      "  function EncodeScalarValue(v: Unicode.ScalarValue): (m: MinimalWellFormedCodeUnitSeq)\n",
      "\n",
      "  function DecodeMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq): (v: Unicode.ScalarValue)\n",
      "    ensures EncodeScalarValue(v) == m\n",
      "\n",
      "  lemma LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m: MinimalWellFormedCodeUnitSeq, s: CodeUnitSeq)\n",
      "    ensures SplitPrefixMinimalWellFormedCodeUnitSubsequence(m + s) == Some(m)\n",
      "  {\n",
      "    var ms := m + s;\n",
      "    assert IsMinimalWellFormedCodeUnitSubsequence(ms[..|m|]);\n",
      "    var prefix := SplitPrefixMinimalWellFormedCodeUnitSubsequence(ms).Extract();\n",
      "    calc ==> {\n",
      "      IsMinimalWellFormedCodeUnitSubsequence(m);\n",
      "      |prefix| <= |m|;\n",
      "      prefix == ms[..|prefix|] == m[..|prefix|] == m;\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function PartitionCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeParts: Option<seq<MinimalWellFormedCodeUnitSeq>>)\n",
      "    ensures maybeParts.Some? ==> Seq.Flatten(maybeParts.Extract()) == s\n",
      "    decreases |s|\n",
      "  {\n",
      "    if s == [] then\n",
      "      Some([])\n",
      "    else\n",
      "      var prefix :- SplitPrefixMinimalWellFormedCodeUnitSubsequence(s); var restParts :- PartitionCodeUnitSequenceChecked(s[|prefix|..]); Some([prefix] + restParts)\n",
      "  } by method {\n",
      "    if s == [] {\n",
      "      return Some([]);\n",
      "    }\n",
      "    var result: seq<MinimalWellFormedCodeUnitSeq> := [];\n",
      "    var rest := s;\n",
      "    while |rest| > 0\n",
      "      invariant PartitionCodeUnitSequenceChecked(s).Some? <==> PartitionCodeUnitSequenceChecked(rest).Some?\n",
      "      invariant PartitionCodeUnitSequenceChecked(s).Some? ==> true && PartitionCodeUnitSequenceChecked(s).value == result + PartitionCodeUnitSequenceChecked(rest).value\n",
      "    {\n",
      "      var prefix :- SplitPrefixMinimalWellFormedCodeUnitSubsequence(rest);\n",
      "      result := result + [prefix];\n",
      "      rest := rest[|prefix|..];\n",
      "    }\n",
      "    assert result + [] == result;\n",
      "    return Some(result);\n",
      "  }\n",
      "\n",
      "  function PartitionCodeUnitSequence(s: WellFormedCodeUnitSeq): (parts: seq<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures Seq.Flatten(parts) == s\n",
      "  {\n",
      "    PartitionCodeUnitSequenceChecked(s).Extract()\n",
      "  }\n",
      "\n",
      "  lemma LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq)\n",
      "    ensures PartitionCodeUnitSequenceChecked(m) == Some([m])\n",
      "  {\n",
      "    LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m, []);\n",
      "    calc == {\n",
      "      Some(m);\n",
      "      SplitPrefixMinimalWellFormedCodeUnitSubsequence(m + []);\n",
      "      {\n",
      "        assert m + [] == m;\n",
      "      }\n",
      "      SplitPrefixMinimalWellFormedCodeUnitSubsequence(m);\n",
      "    }\n",
      "    calc == {\n",
      "      PartitionCodeUnitSequenceChecked(m);\n",
      "      Some([m] + []);\n",
      "      {\n",
      "        assert [m] + [] == [m];\n",
      "      }\n",
      "      Some([m]);\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function IsWellFormedCodeUnitSequence(s: CodeUnitSeq): (b: bool)\n",
      "  {\n",
      "    PartitionCodeUnitSequenceChecked(s).Some?\n",
      "  }\n",
      "\n",
      "  lemma LemmaMinimalWellFormedCodeUnitSubsequenceIsWellFormedSequence(m: MinimalWellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(m)\n",
      "  {\n",
      "    LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m);\n",
      "  }\n",
      "\n",
      "  lemma LemmaPrependMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq, s: WellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(m + s)\n",
      "  {\n",
      "    LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m);\n",
      "    LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m, s);\n",
      "    assert PartitionCodeUnitSequenceChecked(m + s).Some?;\n",
      "  }\n",
      "\n",
      "  lemma LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms: seq<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures IsWellFormedCodeUnitSequence(Seq.Flatten(ms))\n",
      "  {\n",
      "    if |ms| == 0 {\n",
      "      assert IsWellFormedCodeUnitSequence(Seq.Flatten(ms));\n",
      "    } else {\n",
      "      var head := ms[0];\n",
      "      var tail := ms[1..];\n",
      "      LemmaFlattenMinimalWellFormedCodeUnitSubsequences(tail);\n",
      "      var flatTail := Seq.Flatten(tail);\n",
      "      LemmaPrependMinimalWellFormedCodeUnitSubsequence(head, flatTail);\n",
      "      assert IsWellFormedCodeUnitSequence(head + flatTail);\n",
      "    }\n",
      "  }\n",
      "\n",
      "  lemma LemmaConcatWellFormedCodeUnitSubsequences(s: WellFormedCodeUnitSeq, t: WellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(s + t)\n",
      "  {\n",
      "  }\n",
      "\n",
      "  function EncodeScalarSequence(vs: seq<Unicode.ScalarValue>): (s: WellFormedCodeUnitSeq)\n",
      "  {\n",
      "    var ms := Seq.Map(EncodeScalarValue, vs);\n",
      "    LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms);\n",
      "    Seq.Flatten(ms)\n",
      "  } by method {\n",
      "    s := [];\n",
      "    ghost var unflattened: seq<MinimalWellFormedCodeUnitSeq> := [];\n",
      "    for i := |vs| downto 0\n",
      "      invariant unflattened == Seq.Map(EncodeScalarValue, vs[i..])\n",
      "      invariant s == Seq.Flatten(unflattened)\n",
      "    {\n",
      "      var next: MinimalWellFormedCodeUnitSeq := EncodeScalarValue(vs[i]);\n",
      "      unflattened := [next] + unflattened;\n",
      "      LemmaPrependMinimalWellFormedCodeUnitSubsequence(next, s);\n",
      "      s := next + s;\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function DecodeCodeUnitSequence(s: WellFormedCodeUnitSeq): (vs: seq<Unicode.ScalarValue>)\n",
      "    ensures EncodeScalarSequence(vs) == s\n",
      "  {\n",
      "    var parts := PartitionCodeUnitSequence(s);\n",
      "    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);\n",
      "    calc == {\n",
      "      s;\n",
      "      Seq.Flatten(parts);\n",
      "      {\n",
      "        assert parts == Seq.Map(EncodeScalarValue, vs);\n",
      "      }\n",
      "      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));\n",
      "      EncodeScalarSequence(vs);\n",
      "    }\n",
      "    vs\n",
      "  }\n",
      "\n",
      "  function DecodeCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeVs: Option<seq<Unicode.ScalarValue>>)\n",
      "    ensures IsWellFormedCodeUnitSequence(s) ==> maybeVs.Some? && maybeVs.Extract() == DecodeCodeUnitSequence(s)\n",
      "    ensures !IsWellFormedCodeUnitSequence(s) ==> true && maybeVs.None?\n",
      "  {\n",
      "    if IsWellFormedCodeUnitSequence(s) then\n",
      "      Some(DecodeCodeUnitSequence(s))\n",
      "    else\n",
      "      None\n",
      "  } by method {\n",
      "    var maybeParts := PartitionCodeUnitSequenceChecked(s);\n",
      "    if maybeParts.None? {\n",
      "      return None;\n",
      "    }\n",
      "    var parts := maybeParts.value;\n",
      "    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);\n",
      "    calc == {\n",
      "      s;\n",
      "      Seq.Flatten(parts);\n",
      "      {\n",
      "        assert parts == Seq.Map(EncodeScalarValue, vs);\n",
      "      }\n",
      "      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));\n",
      "      EncodeScalarSequence(vs);\n",
      "    }\n",
      "    return Some(vs);\n",
      "  }\n",
      "\n",
      "  import opened Wrappers\n",
      "\n",
      "  import Functions\n",
      "\n",
      "  import Seq\n",
      "\n",
      "  import Unicode\n",
      "\n",
      "  type CodeUnitSeq = seq<CodeUnit>\n",
      "\n",
      "  type WellFormedCodeUnitSeq = s: CodeUnitSeq\n",
      "    | IsWellFormedCodeUnitSequence(s)\n",
      "    witness []\n",
      "\n",
      "  type MinimalWellFormedCodeUnitSeq = s: CodeUnitSeq\n",
      "    | IsMinimalWellFormedCodeUnitSubsequence(s)\n",
      "    witness *\n",
      "\n",
      "  type CodeUnit\n",
      "}\n",
      "\n",
      "    \n",
      "### Error output from the verifier:\n",
      "datset/Unicode/_UnicodeEncodingForm_28.dfy(126,2): Error: a postcondition could not be proved on this return path\n",
      "    |\n",
      "126 |   {\n",
      "    |   ^\n",
      "\n",
      "datset/Unicode/_UnicodeEncodingForm_28.dfy(125,12): Related location: this is the postcondition that could not be proved\n",
      "    |\n",
      "125 |     ensures IsWellFormedCodeUnitSequence(s + t)\n",
      "    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n",
      "\n",
      "datset/Unicode/_UnicodeEncodingForm_28.dfy(92,4): Related location\n",
      "   |\n",
      "92 |     PartitionCodeUnitSequenceChecked(s).Some?\n",
      "   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n",
      "\n",
      "\n",
      "Dafny program verifier finished with 17 verified, 1 error\n",
      "\n",
      "\n",
      "### Corrected program:\n",
      "include \"../Wrappers.dfy\"\n",
      "include \"../Functions.dfy\"\n",
      "include \"../Collections/Sequences/Seq.dfy\"\n",
      "include \"Unicode.dfy\"\n",
      "// dafny 4.3.0.0\n",
      "// Command Line Options: /compile:0 /perturb /quiet datset/Unicode/UnicodeEncodingForm.dfy\n",
      "// UnicodeEncodingForm.dfy\n",
      "\n",
      "\n",
      "abstract module {:options \"-functionSyntax:4\"} UnicodeEncodingForm {\n",
      "  function IsMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (b: bool)\n",
      "    ensures b ==> |s| > 0 && forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i])\n",
      "    decreases |s|\n",
      "\n",
      "  function SplitPrefixMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (maybePrefix: Option<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures |s| == 0 ==> maybePrefix.None?\n",
      "    ensures (exists i | 0 < i <= |s| :: IsMinimalWellFormedCodeUnitSubsequence(s[..i])) <==> true && maybePrefix.Some?\n",
      "    ensures maybePrefix.Some? ==> true && var prefix := maybePrefix.Extract(); 0 < |prefix| <= |s| && prefix == s[..|prefix|] && forall i | 0 < i < |prefix| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i])\n",
      "\n",
      "  function EncodeScalarValue(v: Unicode.ScalarValue): (m: MinimalWellFormedCodeUnitSeq)\n",
      "\n",
      "  function DecodeMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq): (v: Unicode.ScalarValue)\n",
      "    ensures EncodeScalarValue(v) == m\n",
      "\n",
      "  lemma LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m: MinimalWellFormedCodeUnitSeq, s: CodeUnitSeq)\n",
      "    ensures SplitPrefixMinimalWellFormedCodeUnitSubsequence(m + s) == Some(m)\n",
      "  {\n",
      "    var ms := m + s;\n",
      "    assert IsMinimalWellFormedCodeUnitSubsequence(ms[..|m|]);\n",
      "    var prefix := SplitPrefixMinimalWellFormedCodeUnitSubsequence(ms).Extract();\n",
      "    calc ==> {\n",
      "      IsMinimalWellFormedCodeUnitSubsequence(m);\n",
      "      |prefix| <= |m|;\n",
      "      prefix == ms[..|prefix|] == m[..|prefix|] == m;\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function PartitionCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeParts: Option<seq<MinimalWellFormedCodeUnitSeq>>)\n",
      "    ensures maybeParts.Some? ==> Seq.Flatten(maybeParts.Extract()) == s\n",
      "    decreases |s|\n",
      "  {\n",
      "    if s == [] then\n",
      "      Some([])\n",
      "    else\n",
      "      var prefix :- SplitPrefixMinimalWellFormedCodeUnitSubsequence(s); var restParts :- PartitionCodeUnitSequenceChecked(s[|prefix|..]); Some([prefix] + restParts)\n",
      "  } by method {\n",
      "    if s == [] {\n",
      "      return Some([]);\n",
      "    }\n",
      "    var result: seq<MinimalWellFormedCodeUnitSeq> := [];\n",
      "    var rest := s;\n",
      "    while |rest| > 0\n",
      "      invariant PartitionCodeUnitSequenceChecked(s).Some? <==> PartitionCodeUnitSequenceChecked(rest).Some?\n",
      "      invariant PartitionCodeUnitSequenceChecked(s).Some? ==> true && PartitionCodeUnitSequenceChecked(s).value == result + PartitionCodeUnitSequenceChecked(rest).value\n",
      "    {\n",
      "      var prefix :- SplitPrefixMinimalWellFormedCodeUnitSubsequence(rest);\n",
      "      result := result + [prefix];\n",
      "      rest := rest[|prefix|..];\n",
      "    }\n",
      "    assert result + [] == result;\n",
      "    return Some(result);\n",
      "  }\n",
      "\n",
      "  function PartitionCodeUnitSequence(s: WellFormedCodeUnitSeq): (parts: seq<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures Seq.Flatten(parts) == s\n",
      "  {\n",
      "    PartitionCodeUnitSequenceChecked(s).Extract()\n",
      "  }\n",
      "\n",
      "  lemma LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq)\n",
      "    ensures PartitionCodeUnitSequenceChecked(m) == Some([m])\n",
      "  {\n",
      "    LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m, []);\n",
      "    calc == {\n",
      "      Some(m);\n",
      "      SplitPrefixMinimalWellFormedCodeUnitSubsequence(m + []);\n",
      "      {\n",
      "        assert m + [] == m;\n",
      "      }\n",
      "      SplitPrefixMinimalWellFormedCodeUnitSubsequence(m);\n",
      "    }\n",
      "    calc == {\n",
      "      PartitionCodeUnitSequenceChecked(m);\n",
      "      Some([m] + []);\n",
      "      {\n",
      "        assert [m] + [] == [m];\n",
      "      }\n",
      "      Some([m]);\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function IsWellFormedCodeUnitSequence(s: CodeUnitSeq): (b: bool)\n",
      "  {\n",
      "    PartitionCodeUnitSequenceChecked(s).Some?\n",
      "  }\n",
      "\n",
      "  lemma LemmaMinimalWellFormedCodeUnitSubsequenceIsWellFormedSequence(m: MinimalWellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(m)\n",
      "  {\n",
      "    LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m);\n",
      "  }\n",
      "\n",
      "  lemma LemmaPrependMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq, s: WellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(m + s)\n",
      "  {\n",
      "    LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m);\n",
      "    LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m, s);\n",
      "    assert PartitionCodeUnitSequenceChecked(m + s).Some?;\n",
      "  }\n",
      "\n",
      "  lemma LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms: seq<MinimalWellFormedCodeUnitSeq>)\n",
      "    ensures IsWellFormedCodeUnitSequence(Seq.Flatten(ms))\n",
      "  {\n",
      "    if |ms| == 0 {\n",
      "      assert IsWellFormedCodeUnitSequence(Seq.Flatten(ms));\n",
      "    } else {\n",
      "      var head := ms[0];\n",
      "      var tail := ms[1..];\n",
      "      LemmaFlattenMinimalWellFormedCodeUnitSubsequences(tail);\n",
      "      var flatTail := Seq.Flatten(tail);\n",
      "      LemmaPrependMinimalWellFormedCodeUnitSubsequence(head, flatTail);\n",
      "      assert IsWellFormedCodeUnitSequence(head + flatTail);\n",
      "    }\n",
      "  }\n",
      "\n",
      "  lemma LemmaConcatWellFormedCodeUnitSubsequences(s: WellFormedCodeUnitSeq, t: WellFormedCodeUnitSeq)\n",
      "    ensures IsWellFormedCodeUnitSequence(s + t)\n",
      "  {\n",
      "    var partsS := PartitionCodeUnitSequence(s);\n",
      "    var partsT := PartitionCodeUnitSequence(t);\n",
      "    var partsST := partsS + partsT;\n",
      "    Seq.LemmaFlattenConcat(partsS, partsT);\n",
      "    assert s + t == Seq.Flatten(partsST);\n",
      "    assert forall part | part in partsST :: |part| > 0 && IsMinimalWellFormedCodeUnitSubsequence(part);\n",
      "    LemmaFlattenMinimalWellFormedCodeUnitSubsequences(partsST);\n",
      "  }\n",
      "\n",
      "  function EncodeScalarSequence(vs: seq<Unicode.ScalarValue>): (s: WellFormedCodeUnitSeq)\n",
      "  {\n",
      "    var ms := Seq.Map(EncodeScalarValue, vs);\n",
      "    LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms);\n",
      "    Seq.Flatten(ms)\n",
      "  } by method {\n",
      "    s := [];\n",
      "    ghost var unflattened: seq<MinimalWellFormedCodeUnitSeq> := [];\n",
      "    for i := |vs| downto 0\n",
      "      invariant unflattened == Seq.Map(EncodeScalarValue, vs[i..])\n",
      "      invariant s == Seq.Flatten(unflattened)\n",
      "    {\n",
      "      var next: MinimalWellFormedCodeUnitSeq := EncodeScalarValue(vs[i]);\n",
      "      unflattened := [next] + unflattened;\n",
      "      LemmaPrependMinimalWellFormedCodeUnitSubsequence(next, s);\n",
      "      s := next + s;\n",
      "    }\n",
      "  }\n",
      "\n",
      "  function DecodeCodeUnitSequence(s: WellFormedCodeUnitSeq): (vs: seq<Unicode.ScalarValue>)\n",
      "    ensures EncodeScalarSequence(vs) == s\n",
      "  {\n",
      "    var parts := PartitionCodeUnitSequence(s);\n",
      "    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);\n",
      "    calc == {\n",
      "      s;\n",
      "      Seq.Flatten(parts);\n",
      "      {\n",
      "        assert parts == Seq.Map(EncodeScalarValue, vs);\n",
      "      }\n",
      "      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));\n",
      "      EncodeScalarSequence(vs);\n",
      "    }\n",
      "    vs\n",
      "  }\n",
      "\n",
      "  function DecodeCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeVs: Option<seq<Unicode.ScalarValue>>)\n",
      "    ensures IsWellFormedCodeUnitSequence(s) ==> maybeVs.Some? && maybeVs.Extract() == DecodeCodeUnitSequence(s)\n",
      "    ensures !IsWellFormedCodeUnitSequence(s) ==> true && maybeVs.None?\n",
      "  {\n",
      "    if IsWellFormedCodeUnitSequence(s) then\n",
      "      Some(DecodeCodeUnitSequence(s))\n",
      "    else\n",
      "      None\n",
      "  } by method {\n",
      "    var maybeParts := PartitionCodeUnitSequenceChecked(s);\n",
      "    if maybeParts.None? {\n",
      "      return None;\n",
      "    }\n",
      "    var parts := maybeParts.value;\n",
      "    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);\n",
      "    calc == {\n",
      "      s;\n",
      "      Seq.Flatten(parts);\n",
      "      {\n",
      "        assert parts == Seq.Map(EncodeScalarValue, vs);\n",
      "      }\n",
      "      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));\n",
      "      EncodeScalarSequence(vs);\n",
      "    }\n",
      "    return Some(vs);\n",
      "  }\n",
      "\n",
      "  import opened Wrappers\n",
      "\n",
      "  import Functions\n",
      "\n",
      "  import Seq\n",
      "\n",
      "  import Unicode\n",
      "\n",
      "  type CodeUnitSeq = seq<CodeUnit>\n",
      "\n",
      "  type WellFormedCodeUnitSeq = s: CodeUnitSeq\n",
      "    | IsWellFormedCodeUnitSequence(s)\n",
      "    witness []\n",
      "\n",
      "  type MinimalWellFormedCodeUnitSeq = s: CodeUnitSeq\n",
      "    | IsMinimalWellFormedCodeUnitSubsequence(s)\n",
      "    witness *\n",
      "\n",
      "  type CodeUnit\n",
      "}\n",
      "\n"
     ]
    }
   ],
   "source": [
    "print(generate_prompt(data[5]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "e91b495e",
   "metadata": {},
   "outputs": [],
   "source": [
    "train_data = train_data.map(lambda x: ({\"text\": generate_prompt(x) +\"<eos>\" }))\n",
    "test_data = test_data.map(lambda x: ({\"text\": generate_prompt(x) +\"<eos>\"}))\n",
    "\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "1166b777",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "bin c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\bitsandbytes\\libbitsandbytes_cuda121.dll\n"
     ]
    }
   ],
   "source": [
    "from transformers import AutoModelForCausalLM\n",
    "import bitsandbytes as bnb\n",
    "from transformers import BitsAndBytesConfig\n",
    "config = BitsAndBytesConfig(load_in_4bit=True, bnb_4bit_quant_type=\"nf4\", bnb_4bit_use_double_quant=True, bnb_4bit_compute_dtype=torch.bfloat16)\n",
    "model = LlamaForCausalLM.from_pretrained(\n",
    "    model_path,\n",
    "    device_map={\"\":0},\n",
    "    quantization_config=config\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "58b1fccf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "LlamaForCausalLM(\n",
      "  (model): LlamaModel(\n",
      "    (embed_tokens): Embedding(32000, 3200, padding_idx=0)\n",
      "    (layers): ModuleList(\n",
      "      (0-25): 26 x LlamaDecoderLayer(\n",
      "        (self_attn): LlamaAttention(\n",
      "          (q_proj): Linear4bit(in_features=3200, out_features=3200, bias=False)\n",
      "          (k_proj): Linear4bit(in_features=3200, out_features=3200, bias=False)\n",
      "          (v_proj): Linear4bit(in_features=3200, out_features=3200, bias=False)\n",
      "          (o_proj): Linear4bit(in_features=3200, out_features=3200, bias=False)\n",
      "          (rotary_emb): LlamaRotaryEmbedding()\n",
      "        )\n",
      "        (mlp): LlamaMLP(\n",
      "          (gate_proj): Linear4bit(in_features=3200, out_features=8640, bias=False)\n",
      "          (up_proj): Linear4bit(in_features=3200, out_features=8640, bias=False)\n",
      "          (down_proj): Linear4bit(in_features=8640, out_features=3200, bias=False)\n",
      "          (act_fn): SiLUActivation()\n",
      "        )\n",
      "        (input_layernorm): LlamaRMSNorm()\n",
      "        (post_attention_layernorm): LlamaRMSNorm()\n",
      "      )\n",
      "    )\n",
      "    (norm): LlamaRMSNorm()\n",
      "  )\n",
      "  (lm_head): Linear(in_features=3200, out_features=32000, bias=False)\n",
      ")\n"
     ]
    }
   ],
   "source": [
    "from peft import LoraConfig, get_peft_model, prepare_model_for_kbit_training, TaskType\n",
    "print(model)\n",
    "lora_config = LoraConfig(\n",
    " r= 8, \n",
    " lora_alpha=8,\n",
    " target_modules=[ \"q_proj\",\n",
    "    \"o_proj\",\n",
    "    \"k_proj\",\n",
    "    \"v_proj\",\n",
    "    \"gate_proj\",\n",
    "    \"down_proj\",\n",
    "    \"up_proj\",\n",
    "    \"lm_head\"],\n",
    " lora_dropout=0.05,\n",
    " bias=\"none\",\n",
    " task_type=TaskType.CAUSAL_LM\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "9a0389e9",
   "metadata": {},
   "outputs": [],
   "source": [
    "model = prepare_model_for_kbit_training(model)\n",
    "\n",
    "# add LoRA adaptor\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "4f155843",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\trl\\trainer\\ppo_config.py:141: UserWarning: The `optimize_cuda_cache` arguement will be deprecated soon, please use `optimize_device_cache` instead.\n",
      "  warnings.warn(\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\trl\\trainer\\sft_trainer.py:194: UserWarning: You didn't pass a `max_seq_length` argument to the SFTTrainer, this will default to 1024\n",
      "  warnings.warn(\n"
     ]
    },
    {
     "data": {
      "application/vnd.jupyter.widget-view+json": {
       "model_id": "3e11f020bc8b411fa56bfbcfe6f82075",
       "version_major": 2,
       "version_minor": 0
      },
      "text/plain": [
       "Map:   0%|          | 0/320 [00:00<?, ? examples/s]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "application/vnd.jupyter.widget-view+json": {
       "model_id": "4bce705b48194f1e99fd64cf48fa3853",
       "version_major": 2,
       "version_minor": 0
      },
      "text/plain": [
       "Map:   0%|          | 0/80 [00:00<?, ? examples/s]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\trl\\trainer\\sft_trainer.py:247: UserWarning: You passed a tokenizer with `padding_side` not equal to `right` to the SFTTrainer. This might lead to some unexpected behaviour due to overflow issues when training a model in half-precision. You might consider adding `tokenizer.padding_side = 'right'` to your code.\n",
      "  warnings.warn(\n"
     ]
    }
   ],
   "source": [
    "\n",
    "from trl import SFTTrainer\n",
    "import transformers\n",
    "eval_steps = 10\n",
    "save_steps = 10\n",
    "logging_steps = 10\n",
    "output_dir = \"C:/Users/Kevin Zhang/Documents/GitHub/dafny/trainingout\"\n",
    "\n",
    "trainer = SFTTrainer(\n",
    "    model=model,\n",
    "    train_dataset=train_data,\n",
    "    eval_dataset=test_data,\n",
    "    dataset_text_field=\"text\",\n",
    "    args=transformers.TrainingArguments(\n",
    "        num_train_epochs=1,\n",
    "        learning_rate=3e-4,\n",
    "        logging_steps=logging_steps,\n",
    "        evaluation_strategy=\"steps\",\n",
    "        save_strategy=\"steps\",\n",
    "        eval_steps=eval_steps,\n",
    "        save_steps=save_steps,\n",
    "        output_dir=output_dir,\n",
    "        save_total_limit=3,\n",
    "        load_best_model_at_end=True,\n",
    "        push_to_hub=False,\n",
    "        auto_find_batch_size=True\n",
    "    ),\n",
    "    peft_config=lora_config\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "5ed1958a",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[34m\u001b[1mwandb\u001b[0m: Currently logged in as: \u001b[33mklebn\u001b[0m. Use \u001b[1m`wandb login --relogin`\u001b[0m to force relogin\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "Tracking run with wandb version 0.16.1"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Run data is saved locally in <code>C:\\Users\\Kevin Zhang\\Documents\\GitHub\\dafny\\wandb\\run-20231210_233447-cg0s7t5t</code>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Syncing run <strong><a href='https://wandb.ai/klebn/huggingface/runs/cg0s7t5t' target=\"_blank\">fragrant-music-18</a></strong> to <a href='https://wandb.ai/klebn/huggingface' target=\"_blank\">Weights & Biases</a> (<a href='https://wandb.me/run' target=\"_blank\">docs</a>)<br/>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       " View project at <a href='https://wandb.ai/klebn/huggingface' target=\"_blank\">https://wandb.ai/klebn/huggingface</a>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       " View run at <a href='https://wandb.ai/klebn/huggingface/runs/cg0s7t5t' target=\"_blank\">https://wandb.ai/klebn/huggingface/runs/cg0s7t5t</a>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "You're using a LlamaTokenizerFast tokenizer. Please note that with a fast tokenizer, using the `__call__` method is faster than using a method to encode the text followed by a call to the `pad` method to get a padded encoding.\n",
      "`use_cache=True` is incompatible with gradient checkpointing. Setting `use_cache=False`...\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\torch\\utils\\checkpoint.py:429: UserWarning: torch.utils.checkpoint: please pass in use_reentrant=True or use_reentrant=False explicitly. The default value of use_reentrant will be updated to be False in the future. To maintain current behavior, pass use_reentrant=True. It is recommended that you use use_reentrant=False. Refer to docs for more details on the differences between the two variants.\n",
      "  warnings.warn(\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "\n",
       "    <div>\n",
       "      \n",
       "      <progress value='40' max='40' style='width:300px; height:20px; vertical-align: middle;'></progress>\n",
       "      [40/40 14:52:30, Epoch 1/1]\n",
       "    </div>\n",
       "    <table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       " <tr style=\"text-align: left;\">\n",
       "      <th>Step</th>\n",
       "      <th>Training Loss</th>\n",
       "      <th>Validation Loss</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <td>10</td>\n",
       "      <td>0.719900</td>\n",
       "      <td>0.509201</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <td>20</td>\n",
       "      <td>0.406600</td>\n",
       "      <td>0.330660</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <td>30</td>\n",
       "      <td>0.242700</td>\n",
       "      <td>0.257715</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <td>40</td>\n",
       "      <td>0.219400</td>\n",
       "      <td>0.236480</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table><p>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\peft\\utils\\save_and_load.py:131: UserWarning: Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\n",
      "  warnings.warn(\"Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\")\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\peft\\utils\\save_and_load.py:131: UserWarning: Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\n",
      "  warnings.warn(\"Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\")\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\torch\\utils\\checkpoint.py:429: UserWarning: torch.utils.checkpoint: please pass in use_reentrant=True or use_reentrant=False explicitly. The default value of use_reentrant will be updated to be False in the future. To maintain current behavior, pass use_reentrant=True. It is recommended that you use use_reentrant=False. Refer to docs for more details on the differences between the two variants.\n",
      "  warnings.warn(\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\peft\\utils\\save_and_load.py:131: UserWarning: Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\n",
      "  warnings.warn(\"Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\")\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\torch\\utils\\checkpoint.py:429: UserWarning: torch.utils.checkpoint: please pass in use_reentrant=True or use_reentrant=False explicitly. The default value of use_reentrant will be updated to be False in the future. To maintain current behavior, pass use_reentrant=True. It is recommended that you use use_reentrant=False. Refer to docs for more details on the differences between the two variants.\n",
      "  warnings.warn(\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\peft\\utils\\save_and_load.py:131: UserWarning: Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\n",
      "  warnings.warn(\"Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\")\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\torch\\utils\\checkpoint.py:429: UserWarning: torch.utils.checkpoint: please pass in use_reentrant=True or use_reentrant=False explicitly. The default value of use_reentrant will be updated to be False in the future. To maintain current behavior, pass use_reentrant=True. It is recommended that you use use_reentrant=False. Refer to docs for more details on the differences between the two variants.\n",
      "  warnings.warn(\n",
      "c:\\users\\kevin zhang\\appdata\\local\\programs\\python\\python39\\lib\\site-packages\\peft\\utils\\save_and_load.py:131: UserWarning: Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\n",
      "  warnings.warn(\"Setting `save_embedding_layers` to `True` as embedding layers found in `target_modules`.\")\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "TrainOutput(global_step=40, training_loss=0.3971314251422882, metrics={'train_runtime': 54477.2952, 'train_samples_per_second': 0.006, 'train_steps_per_second': 0.001, 'total_flos': 6560942968012800.0, 'train_loss': 0.3971314251422882, 'epoch': 1.0})"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "trainer.train()\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "e2b8ca53",
   "metadata": {},
   "outputs": [],
   "source": [
    "trainer.save_model(\"openllama-3b-int4-dafny-3\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "894454a0-0700-44ac-ba9d-8901cb527082",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('openllama-3b-int4-dafny-3\\\\tokenizer_config.json',\n",
       " 'openllama-3b-int4-dafny-3\\\\special_tokens_map.json',\n",
       " 'openllama-3b-int4-dafny-3\\\\tokenizer.model',\n",
       " 'openllama-3b-int4-dafny-3\\\\added_tokens.json',\n",
       " 'openllama-3b-int4-dafny-3\\\\tokenizer.json')"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "trainer.tokenizer.save_pretrained(\"openllama-3b-int4-dafny-3\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "41015dfe-933e-4095-9a20-46f0e405d00d",
   "metadata": {},
   "outputs": [],
   "source": [
    "trainer.model.config.to_json_file(\"openllama-3b-int4-dafny-3/config.json\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2c9a5079-5817-4fc8-87f6-ce048dfe941a",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8d7d4d16-f3ee-488b-8308-e6174ca183b1",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}