src/models/gpt_neo/gptNEO_eval.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "37b416dd",
   "metadata": {},
   "outputs": [],
   "source": [
    "import glob"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "97243d38",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['json_data_0.json', 'json_data__hard_ones.json', 'json_data_1.json']"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "glob.glob(\"*.json\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "da4ab5e8",
   "metadata": {},
   "outputs": [],
   "source": [
    "import json\n",
    "\n",
    "with open('json_data_0.json', 'r') as json_file:\n",
    "    json_list = [json.loads(i) for i in list(json_file)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "a1cb89f2",
   "metadata": {},
   "outputs": [],
   "source": [
    "import json\n",
    "\n",
    "with open('json_data_1.json', 'r') as json_file:\n",
    "    json_list2 = [json.loads(i) for i in list(json_file)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 105,
   "id": "96c299f2",
   "metadata": {},
   "outputs": [],
   "source": [
    "final_data = json_list[0] + json_list2[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 106,
   "id": "aa8c2a9d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "7128"
      ]
     },
     "execution_count": 106,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(final_data)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "4c5055cf",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "7128"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(final_data)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "55f25b6f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'results': ['   subst n\\n',\n",
       "  '   dsimp [cons, vector.cons, list.cons]\\n',\n",
       "  '   rw [list.cons_append, list.cons_erase n]; by_cases n = 0; [ rw [list.cons_erase n, to_list_cons, list.to_list_cons] ]\\n',\n",
       "  '   subst n\\n',\n",
       "  '   subst n\\n',\n",
       "  '   dsimp [list.cons]\\n',\n",
       "  '   dsimp [cons]\\n',\n",
       "  '   dsimp [cons, to_list]\\n',\n",
       "  '   dsimp [to_list]; rw [list.cons_head, cons_nth]\\n',\n",
       "  '   subst n\\n',\n",
       "  '   subst n\\n',\n",
       "  '   dsimp [cons]\\n',\n",
       "  '   dsimp [list.to_list, list.cons]; simp [list.cons, list.to_list, list.nil_cons]\\n',\n",
       "  '   subst n\\n',\n",
       "  '   rw [← list.cons_head]\\n'],\n",
       " 'prompt': 'GOAL α : Type u,\\tn : ℕ,\\ta : α,\\tv : vector α n\\t⊢ (vector.cons a v).to_list = a :: v.to_list\\n PROOFSTEP ',\n",
       " 'completion': ' cases v\\n'}"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "final_data[10]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "813bdd55",
   "metadata": {},
   "outputs": [],
   "source": [
    "each = final_data[2]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "id": "bb4aae67",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'results': [\"   erw [read, array.read', h, array.read', h]\\n\",\n",
       "  '   conv_rhs { rw ←array.read ⟨b_fst, b_snd⟩ }\\n',\n",
       "  \"   dsimp [read']\\n\",\n",
       "  \"   rw [read', array.read_eq_nil_of_ne b_snd h]\\n\",\n",
       "  '   rw [read₂, h]\\n',\n",
       "  '   subst i\\n',\n",
       "  \"   dsimp [read']\\n\",\n",
       "  \"   rw [read', array_read', le_antisymm h]\\n\",\n",
       "  '   subst h\\n',\n",
       "  '   dsimp [array.read]\\n',\n",
       "  '   refl\\n',\n",
       "  \"   simp [read', array, h]\\n\",\n",
       "  '   subst i\\n',\n",
       "  '   subst i\\n',\n",
       "  '   dsimp [read]\\n'],\n",
       " 'prompt': \"GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst : ℕ,\\tb_snd : array b_fst α,\\th : i < buffer.size ⟨b_fst, b_snd⟩\\t⊢ buffer.read ⟨b_fst, b_snd⟩ ⟨i, h⟩ = buffer.read' ⟨b_fst, b_snd⟩ i\\n PROOFSTEP \",\n",
       " 'completion': \" unfold read read'\\n\"}"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "each\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "id": "b376ba85",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'best_match': \"erw [read, array.read', h, array.read', h]\",\n",
       " 'score': 0.0,\n",
       " 'real': \"unfold read read'\",\n",
       " 'all': [\"erw [read, array.read', h, array.read', h]\",\n",
       "  'refl',\n",
       "  'subst i',\n",
       "  'subst h',\n",
       "  \"rw [read', array_read', le_antisymm h]\",\n",
       "  \"dsimp [read']\",\n",
       "  'dsimp [read]',\n",
       "  'conv_rhs { rw ←array.read ⟨b_fst, b_snd⟩ }',\n",
       "  \"rw [read', array.read_eq_nil_of_ne b_snd h]\",\n",
       "  'rw [read₂, h]',\n",
       "  'dsimp [array.read]',\n",
       "  \"simp [read', array, h]\"],\n",
       " 'prompt': \"GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst : ℕ,\\tb_snd : array b_fst α,\\th : i < buffer.size ⟨b_fst, b_snd⟩\\t⊢ buffer.read ⟨b_fst, b_snd⟩ ⟨i, h⟩ = buffer.read' ⟨b_fst, b_snd⟩ i\\n PROOFSTEP \"}"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "each_one(each)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "id": "469050dd",
   "metadata": {},
   "outputs": [],
   "source": [
    "def each_one(each):\n",
    "    resultiii = each[\"results\"]\n",
    "    resii = list(set([j.strip() for i in resultiii for j in i.replace(\"PROOFSTEP\",\"\\n\").replace(';', '\\n').split(\"\\n\") if not(j.isupper() or j.strip()==\"\")]))\n",
    "    result_real = each[\"completion\"].replace(\"PROOFSTEP\",\"\\n\").replace(';', '\\n').split(\"\\n\")[0].split()\n",
    "    length_result = len(result_real) \n",
    "    resi_length = [len(set(i.split()).intersection(result_real)) for i in resii]\n",
    "    maximum =  max(resi_length) if resi_length!=[] else 0\n",
    "    return { \"best_match\": resii[resi_length.index(maximum)] if resi_length!=[] else \"\",    \"score\":maximum/length_result,    \"real\":\" \".join(result_real),  \"all\":resii,  \"prompt\":each[\"prompt\"]}\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "id": "4d37786f",
   "metadata": {},
   "outputs": [],
   "source": [
    "# final_data"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "id": "c5425391",
   "metadata": {},
   "outputs": [],
   "source": [
    "result_neo= [ each_one(i) for i in final_data]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "id": "f9cbc026",
   "metadata": {},
   "outputs": [],
   "source": [
    "result_neo_c= [ each_one(i)[\"score\"] for i in final_data]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "id": "52279afb",
   "metadata": {},
   "outputs": [],
   "source": [
    "import numpy as np"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "id": "1198411c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0.30759333988765086"
      ]
     },
     "execution_count": 80,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "np.mean(result_neo_c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "e90a2817",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'best_match': 'simp [hb]',\n",
       " 'score': 1.0,\n",
       " 'real': 'simp [hb]',\n",
       " 'all': ['subst a',\n",
       "  'aux h',\n",
       "  'rw [mul_comm, mul_left_comm]',\n",
       "  'exact mul_zero (mul_eq_zero.mp hab) (mul_left_cancel hcd)',\n",
       "  'simp [hb]',\n",
       "  'hedral_blur : (b * b / (d * d)) = ((a / b) * c / (c * d))',\n",
       "  'subst hb',\n",
       "  'have hcd1 : ∃ (y : ℕ), c + (d * y) = b',\n",
       "  'rw [mul_div_assoc, hb.eq, mul_zero, int.mul_div_cancel_left]',\n",
       "  'conv {to_rhs, rw ← hb}',\n",
       "  'rw [mul_comm]',\n",
       "  'rw [mul_div_assoc, ← mul_assoc (nat.eq_zero_of_dvd_one hb) b, mul_zero, zero_div]',\n",
       "  'rw [mem_div_iff hb, zero_mul, zero_mul, mul_zero, zero_mul, mul_zero, zero_add, zero_add]',\n",
       "  'hedral_zero_right',\n",
       "  'have h₀ : ite (0 = b * d) 0 = a * c / (b * d)'],\n",
       " 'prompt': 'GOAL a b c d : ℕ,\\thab : b ∣ a,\\thcd : d ∣ c,\\texi1 : ∃ (x : ℕ), a = b * x,\\texi2 : ∃ (y : ℕ), c = d * y,\\thb : b = 0\\t⊢ a / b * (c / d) = a * c / (b * d)\\n PROOFSTEP '}"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{ \"best_match\": resii[resi_length.index(maximum)],    \"score\":maximum/length_result,    \"real\":\" \".join(result_real),  \"all\":resii,  \"prompt\":each[\"prompt\"]}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "9ce8910b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['simp', '[hb]']"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result_real"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "6b3d8a6e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['subst a',\n",
       " 'aux h',\n",
       " 'rw [mul_comm, mul_left_comm]',\n",
       " 'exact mul_zero (mul_eq_zero.mp hab) (mul_left_cancel hcd)',\n",
       " 'simp [hb]',\n",
       " 'hedral_blur : (b * b / (d * d)) = ((a / b) * c / (c * d))',\n",
       " 'subst hb',\n",
       " 'have hcd1 : ∃ (y : ℕ), c + (d * y) = b',\n",
       " 'rw [mul_div_assoc, hb.eq, mul_zero, int.mul_div_cancel_left]',\n",
       " 'conv {to_rhs, rw ← hb}',\n",
       " 'rw [mul_comm]',\n",
       " 'rw [mul_div_assoc, ← mul_assoc (nat.eq_zero_of_dvd_one hb) b, mul_zero, zero_div]',\n",
       " 'rw [mem_div_iff hb, zero_mul, zero_mul, mul_zero, zero_mul, mul_zero, zero_add, zero_add]',\n",
       " 'hedral_zero_right',\n",
       " 'have h₀ : ite (0 = b * d) 0 = a * c / (b * d)']"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "resii"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 82,
   "id": "566c1138",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Reranker\t  gdrive\t     json_data__hard_ones.json\tonstart.sh\r\n",
      "all_gpt-ada.json  gptNEO_eval.ipynb  neo-Copy1.ipynb\t\treranker.ipynb\r\n",
      "class\t\t  json_data_0.json   neo.ipynb\t\t\tresults\r\n",
      "files_upload\t  json_data_1.json   onstart.log\r\n"
     ]
    }
   ],
   "source": [
    "!ls\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 88,
   "id": "d3ee64fb",
   "metadata": {},
   "outputs": [],
   "source": [
    "import json\n",
    "\n",
    "with open('all_gpt-ada.json', 'r') as json_file:\n",
    "    json_ada = [json.loads(i) for i in list(json_file)][0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 123,
   "id": "a3dff8e4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'best_match': 'cases v',\n",
       " 'score': 1.0,\n",
       " 'real': 'cases v',\n",
       " 'all': ['cases v',\n",
       "  'p : list α',\n",
       "  \"⊢ (vector.to_list v).cases_on' (cons a v) (λ i, id) (λ i\",\n",
       "  '_match : ∀ (_a _a_1 : list α), _a.length = _a_',\n",
       "  '_inst_1 : Π (p : Prop), decidable p,\\thv : v.to_list = list.',\n",
       "  'append : v.to_list = v.cons a :: v.to_list',\n",
       "  \"⊢ (vector.to_list v).cases_on' (cons a v) (λ i, by simp)\",\n",
       "  'rw to_list_cons'],\n",
       " 'prompt': 'GOAL α : Type u,\\tn : ℕ,\\ta : α,\\tv : vector α n\\t⊢ (vector.cons a v).to_list = a :: v.to_list\\n PROOFSTEP '}"
      ]
     },
     "execution_count": 123,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "json_ada[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 93,
   "id": "78cb85d2",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{'best_match': 'α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst : ℕ,\\tb',\n",
       "  'score': 0.0,\n",
       "  'real': \"unfold read read'\",\n",
       "  'all': ['α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst : ℕ,\\tb',\n",
       "   'subst i',\n",
       "   'α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :',\n",
       "   'simp',\n",
       "   'assumption',\n",
       "   'rw [← unfold_coes_eq',\n",
       "   'simp [size, h]',\n",
       "   'simp [insert_of_mem, h]',\n",
       "   'refl',\n",
       "   'cases i',\n",
       "   '⊢ d_vars ⟨',\n",
       "   'h'],\n",
       "  'prompt': \"GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst : ℕ,\\tb_snd : array b_fst α,\\th : i < buffer.size ⟨b_fst, b_snd⟩\\t⊢ buffer.read ⟨b_fst, b_snd⟩ ⟨i, h⟩ = buffer.read' ⟨b_fst, b_snd⟩ i\\n PROOFSTEP \"}]"
      ]
     },
     "execution_count": 93,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[ i for i in json_ada if each[\"prompt\"]==i[\"prompt\"]]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 107,
   "id": "b3106baf",
   "metadata": {},
   "outputs": [],
   "source": [
    "modified = []\n",
    "for each in final_data:\n",
    "    f = [ i[\"all\"] for i in json_ada if each[\"prompt\"]==i[\"prompt\"]]\n",
    "    f_flat = [j for i in f for j in i]\n",
    "#     print(len(each[\"results\"]))\n",
    "    each[\"results\"] = list(set(each[\"results\"]+f_flat))\n",
    "#     print(len(each[\"results\"]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 124,
   "id": "4614e895",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'results': ['cases i',\n",
       "  \"apply b.reverse_corec'\",\n",
       "  'apply b.append_right_',\n",
       "  \"   rw [array.read_write', array.write'_write, buffer.write_mem, array.write_mem, h]\\n\",\n",
       "  'apply b',\n",
       "  '   delta read\\n',\n",
       "  'apply fin',\n",
       "  \"   convert b.read'\\n\",\n",
       "  '   dsimp only [read, dsimp] at h\\n',\n",
       "  'apply_instance',\n",
       "  '  \\n',\n",
       "  \"set i := b.reverse_core i with h'\",\n",
       "  'apply b.append_left_inj',\n",
       "  '   dsimp [read]\\n',\n",
       "  '   subst i\\n',\n",
       "  '⊢ b.read',\n",
       "  'rw [size, h]',\n",
       "  'apply mem',\n",
       "  '   convert read_inj b\\n',\n",
       "  'simp [append_right]',\n",
       "  'simp [size, h]',\n",
       "  'rw [←append_right_inj]',\n",
       "  'simp',\n",
       "  '⊢ b.reverse_',\n",
       "  '   dsimp [read] at h\\n',\n",
       "  '   simp! * at *\\n',\n",
       "  'set_of_eq_eq_succ_of_eq',\n",
       "  '   contradiction\\n',\n",
       "  'rw [←append_right_inverse_iff, ←',\n",
       "  \"apply b.read'_eq_of_mem\",\n",
       "  '_match : ∀ (_a _a_1 :append (list α) ⟨i,',\n",
       "  'apply b.append_right',\n",
       "  'apply b.append_left_injective',\n",
       "  '_inst : inhabited α :=',\n",
       "  'apply b.reverse_core_eq',\n",
       "  \"apply b.append_right'\"],\n",
       " 'prompt': \"GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : buffer α,\\ti : ℕ,\\th : i < b.size\\t⊢ b.read ⟨i, h⟩ = b.read' i\\n PROOFSTEP \",\n",
       " 'completion': \" cases b; unfold read read'; simp [array.read_eq_read']\\n\"}"
      ]
     },
     "execution_count": 124,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "final_data[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "id": "9c20b3d8",
   "metadata": {},
   "outputs": [],
   "source": [
    "result_neo_new= [ each_one(i) for i in final_data]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 110,
   "id": "24f23046",
   "metadata": {},
   "outputs": [],
   "source": [
    "result_neo_c_new= [ each_one(i)[\"score\"] for i in final_data]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 112,
   "id": "8246cbf0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0.4592759403677324"
      ]
     },
     "execution_count": 112,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "np.mean(result_neo_c_new)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 117,
   "id": "5f7e4bf4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "18.628226711560046"
      ]
     },
     "execution_count": 117,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "np.mean([len(i[\"all\"]) for i in result_neo_new])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 118,
   "id": "8f35d406",
   "metadata": {},
   "outputs": [],
   "source": [
    "# import json\n",
    "\n",
    "# with open('files_upload/data_test.jsonl', 'r') as json_file:\n",
    "#     json_list = [json.loads(i) for i in list(final_data)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 119,
   "id": "688deda9",
   "metadata": {},
   "outputs": [],
   "source": [
    "with open('all_gpt_combined.json', 'w') as fout:\n",
    "    json.dump(result_neo_new , fout)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 122,
   "id": "62e4917d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "400K\tReranker\n",
      "6.2M\tall_gpt-ada.json\n",
      "11M\tall_gpt_combined.json\n",
      "538M\tclass\n",
      "562M\tfiles_upload\n",
      "7.9M\tgdrive\n",
      "20K\tgptNEO_eval.ipynb\n",
      "1012K\tjson_data_0.json\n",
      "7.9M\tjson_data_1.json\n",
      "4.3M\tjson_data__hard_ones.json\n",
      "740K\tneo-Copy1.ipynb\n",
      "908K\tneo.ipynb\n",
      "0\tonstart.log\n",
      "4.0K\tonstart.sh\n",
      "12K\treranker.ipynb\n",
      "11G\tresults\n"
     ]
    }
   ],
   "source": [
    "!du -sh *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 126,
   "id": "c1453a31",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'best_match': 'convert read_inj b',\n",
       " 'score': 0.5,\n",
       " 'real': 'cases b',\n",
       " 'all': ['contradiction',\n",
       "  'delta read',\n",
       "  'subst i',\n",
       "  'dsimp only [read, dsimp] at h',\n",
       "  \"rw [array.read_write', array.write'_write, buffer.write_mem, array.write_mem, h]\",\n",
       "  'simp! * at *',\n",
       "  'dsimp [read]',\n",
       "  'convert read_inj b',\n",
       "  \"convert b.read'\",\n",
       "  'dsimp [read] at h'],\n",
       " 'prompt': \"GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : buffer α,\\ti : ℕ,\\th : i < b.size\\t⊢ b.read ⟨i, h⟩ = b.read' i\\n PROOFSTEP \"}"
      ]
     },
     "execution_count": 126,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result_neo[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 127,
   "id": "0d36849b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[0m\u001b[01;34mReranker\u001b[0m/              \u001b[01;32mgdrive\u001b[0m*                    onstart.sh\r\n",
      "all_gpt-ada.json       gptNEO_eval.ipynb          reranker-show.ipynb\r\n",
      "all_gpt_combined.json  json_data_0.json           reranker-train.ipynb\r\n",
      "\u001b[01;34mclass\u001b[0m/                 json_data_1.json           \u001b[01;34mresults\u001b[0m/\r\n",
      "\u001b[01;34mdata\u001b[0m/                  json_data__hard_ones.json  test.json\r\n",
      "data.py                neo-Copy1.ipynb            \u001b[01;34mtmp_trainer\u001b[0m/\r\n",
      "data_and_metadata.csv  neo.ipynb\r\n",
      "\u001b[01;34mfiles_upload\u001b[0m/          onstart.log\r\n"
     ]
    }
   ],
   "source": [
    "ls "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 128,
   "id": "c9c06f52",
   "metadata": {},
   "outputs": [],
   "source": [
    "import pandas as pd"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 130,
   "id": "9d26ae59",
   "metadata": {},
   "outputs": [],
   "source": [
    "df = pd.read_csv(\"data_and_metadata.csv\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 141,
   "id": "17b8b110",
   "metadata": {},
   "outputs": [],
   "source": [
    "df2=pd.DataFrame(result_neo_new)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 142,
   "id": "9386b6dd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>best_match</th>\n",
       "      <th>score</th>\n",
       "      <th>real</th>\n",
       "      <th>all</th>\n",
       "      <th>prompt</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>cases i</td>\n",
       "      <td>0.500000</td>\n",
       "      <td>cases b</td>\n",
       "      <td>[cases i, apply b.reverse_corec', apply b.appe...</td>\n",
       "      <td>GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>cases i</td>\n",
       "      <td>0.500000</td>\n",
       "      <td>cases b</td>\n",
       "      <td>[cases i, cases b.read_inj h, apply b.reverse_...</td>\n",
       "      <td>GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>cases i</td>\n",
       "      <td>0.000000</td>\n",
       "      <td>unfold read read'</td>\n",
       "      <td>[cases i, simp [insert_of_mem, h], assumption,...</td>\n",
       "      <td>GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>simp [show ((b_fst, i) - 1) = i + 1, from fune...</td>\n",
       "      <td>0.500000</td>\n",
       "      <td>simp [array.read_eq_read']</td>\n",
       "      <td>[try {refl}, exact rfl, cases b_snd, refl, sub...</td>\n",
       "      <td>GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>cases i</td>\n",
       "      <td>0.500000</td>\n",
       "      <td>cases b</td>\n",
       "      <td>[cases i, apply b.reverse_corec', apply b.appe...</td>\n",
       "      <td>GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7123</th>\n",
       "      <td>simp only [f</td>\n",
       "      <td>0.285714</td>\n",
       "      <td>simp only [B, finset.card_sdiff this, function...</td>\n",
       "      <td>[apply nat, bound, { rw [← C_eq], exact nat.lt...</td>\n",
       "      <td>GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7124</th>\n",
       "      <td>exact</td>\n",
       "      <td>0.166667</td>\n",
       "      <td>exact nat.pred_lt (ne_of_gt (lt_trans nat.zero...</td>\n",
       "      <td>[ik, bound, exact, conv, { rw [card_singleton,...</td>\n",
       "      <td>GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7125</th>\n",
       "      <td>refine lt</td>\n",
       "      <td>0.083333</td>\n",
       "      <td>refine finset.sum_lt_sum (λ i hi, finset.card_...</td>\n",
       "      <td>[rw C, exact, ⊢ finset., refine lt, rw [finset...</td>\n",
       "      <td>GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7126</th>\n",
       "      <td>{ rcases Ai_empty with ⟨i, _⟩, simp only [fins...</td>\n",
       "      <td>0.087719</td>\n",
       "      <td>{ rcases Ai_empty with ⟨i, hi⟩, have : ∑ j in ...</td>\n",
       "      <td>[{, { rcases Ai_empty with ⟨i, _⟩, simp only [...</td>\n",
       "      <td>GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7127</th>\n",
       "      <td>{ intro i, have : (⊥ : finset (α i)).card = n ...</td>\n",
       "      <td>0.181818</td>\n",
       "      <td>{ assume i, have pos : finset.card (A i) ≠ 0, ...</td>\n",
       "      <td>[{ intro i, have : (⊥ : finset (α i)).card = n...</td>\n",
       "      <td>GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>7128 rows × 5 columns</p>\n",
       "</div>"
      ],
      "text/plain": [
       "                                             best_match     score  \\\n",
       "0                                               cases i  0.500000   \n",
       "1                                               cases i  0.500000   \n",
       "2                                               cases i  0.000000   \n",
       "3     simp [show ((b_fst, i) - 1) = i + 1, from fune...  0.500000   \n",
       "4                                               cases i  0.500000   \n",
       "...                                                 ...       ...   \n",
       "7123                                       simp only [f  0.285714   \n",
       "7124                                              exact  0.166667   \n",
       "7125                                          refine lt  0.083333   \n",
       "7126  { rcases Ai_empty with ⟨i, _⟩, simp only [fins...  0.087719   \n",
       "7127  { intro i, have : (⊥ : finset (α i)).card = n ...  0.181818   \n",
       "\n",
       "                                                   real  \\\n",
       "0                                               cases b   \n",
       "1                                               cases b   \n",
       "2                                     unfold read read'   \n",
       "3                            simp [array.read_eq_read']   \n",
       "4                                               cases b   \n",
       "...                                                 ...   \n",
       "7123  simp only [B, finset.card_sdiff this, function...   \n",
       "7124  exact nat.pred_lt (ne_of_gt (lt_trans nat.zero...   \n",
       "7125  refine finset.sum_lt_sum (λ i hi, finset.card_...   \n",
       "7126  { rcases Ai_empty with ⟨i, hi⟩, have : ∑ j in ...   \n",
       "7127  { assume i, have pos : finset.card (A i) ≠ 0, ...   \n",
       "\n",
       "                                                    all  \\\n",
       "0     [cases i, apply b.reverse_corec', apply b.appe...   \n",
       "1     [cases i, cases b.read_inj h, apply b.reverse_...   \n",
       "2     [cases i, simp [insert_of_mem, h], assumption,...   \n",
       "3     [try {refl}, exact rfl, cases b_snd, refl, sub...   \n",
       "4     [cases i, apply b.reverse_corec', apply b.appe...   \n",
       "...                                                 ...   \n",
       "7123  [apply nat, bound, { rw [← C_eq], exact nat.lt...   \n",
       "7124  [ik, bound, exact, conv, { rw [card_singleton,...   \n",
       "7125  [rw C, exact, ⊢ finset., refine lt, rw [finset...   \n",
       "7126  [{, { rcases Ai_empty with ⟨i, _⟩, simp only [...   \n",
       "7127  [{ intro i, have : (⊥ : finset (α i)).card = n...   \n",
       "\n",
       "                                                 prompt  \n",
       "0     GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...  \n",
       "1     GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...  \n",
       "2     GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_...  \n",
       "3     GOAL α : Type u,\\t_inst_1 : inhabited α,\\ti b_...  \n",
       "4     GOAL α : Type u,\\t_inst_1 : inhabited α,\\tb : ...  \n",
       "...                                                 ...  \n",
       "7123  GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...  \n",
       "7124  GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...  \n",
       "7125  GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...  \n",
       "7126  GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...  \n",
       "7127  GOAL R : Type u,\\tι : Type u',\\tM₁ : ι → Type ...  \n",
       "\n",
       "[7128 rows x 5 columns]"
      ]
     },
     "execution_count": 142,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 143,
   "id": "2dafc56b",
   "metadata": {},
   "outputs": [],
   "source": [
    "prompt = [i.replace(\"GOAL\",\"\").replace(\"PROOFSTEP\",\"\").strip() for i in df2[\"prompt\"]]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 144,
   "id": "ec65ee63",
   "metadata": {},
   "outputs": [],
   "source": [
    "df2[\"prompt\"] = prompt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 145,
   "id": "3dc35b66",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Unnamed: 0</th>\n",
       "      <th>goal_pp</th>\n",
       "      <th>decl_name</th>\n",
       "      <th>open_namespaces</th>\n",
       "      <th>filename</th>\n",
       "      <th>line</th>\n",
       "      <th>column</th>\n",
       "      <th>proof_key</th>\n",
       "      <th>human_tactic_code</th>\n",
       "      <th>tactic_class</th>\n",
       "      <th>cleaned_goal</th>\n",
       "      <th>split</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>0</td>\n",
       "      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n",
       "      <td>buffer.read_eq_read'</td>\n",
       "      <td>buffer</td>\n",
       "      <td>lean/library/data/buffer.lean</td>\n",
       "      <td>49</td>\n",
       "      <td>30</td>\n",
       "      <td>lean/library/data/buffer.lean:49:1</td>\n",
       "      <td>cases b; unfold read read'; simp [array.read_e...</td>\n",
       "      <td>semicolon</td>\n",
       "      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>1</td>\n",
       "      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n",
       "      <td>buffer.read_eq_read'</td>\n",
       "      <td>buffer</td>\n",
       "      <td>lean/library/data/buffer.lean</td>\n",
       "      <td>49</td>\n",
       "      <td>11</td>\n",
       "      <td>lean/library/data/buffer.lean:49:1</td>\n",
       "      <td>cases b; unfold read read'</td>\n",
       "      <td>semicolon</td>\n",
       "      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>2</td>\n",
       "      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n",
       "      <td>buffer.read_eq_read'</td>\n",
       "      <td>buffer</td>\n",
       "      <td>lean/library/data/buffer.lean</td>\n",
       "      <td>49</td>\n",
       "      <td>13</td>\n",
       "      <td>lean/library/data/buffer.lean:49:1</td>\n",
       "      <td>unfold read read'</td>\n",
       "      <td>named</td>\n",
       "      <td>α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>3</td>\n",
       "      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n",
       "      <td>buffer.read_eq_read'</td>\n",
       "      <td>buffer</td>\n",
       "      <td>lean/library/data/buffer.lean</td>\n",
       "      <td>49</td>\n",
       "      <td>32</td>\n",
       "      <td>lean/library/data/buffer.lean:49:1</td>\n",
       "      <td>simp [array.read_eq_read']</td>\n",
       "      <td>named</td>\n",
       "      <td>α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>4</td>\n",
       "      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n",
       "      <td>buffer.read_eq_read'</td>\n",
       "      <td>buffer</td>\n",
       "      <td>lean/library/data/buffer.lean</td>\n",
       "      <td>49</td>\n",
       "      <td>4</td>\n",
       "      <td>lean/library/data/buffer.lean:49:1</td>\n",
       "      <td>cases b</td>\n",
       "      <td>named</td>\n",
       "      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>200025</th>\n",
       "      <td>200025</td>\n",
       "      <td>α : Type u_1,\\nβ : Type u_2,\\n_inst_1 : unifor...</td>\n",
       "      <td>uniform_embedding_def'</td>\n",
       "      <td>classical filter topological_space set</td>\n",
       "      <td>mathlib/src/topology/uniform_space/uniform_emb...</td>\n",
       "      <td>78</td>\n",
       "      <td>61</td>\n",
       "      <td>mathlib/src/topology/uniform_space/uniform_emb...</td>\n",
       "      <td>simp only [uniform_embedding_def, uniform_cont...</td>\n",
       "      <td>semicolon</td>\n",
       "      <td>α : Type u_1,\\tβ : Type u_2,\\t_inst_1 : unifor...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>200026</th>\n",
       "      <td>200026</td>\n",
       "      <td>α : Type u_1,\\nβ : Type u_2,\\n_inst_1 : unifor...</td>\n",
       "      <td>uniform_embedding_def'</td>\n",
       "      <td>classical filter topological_space set</td>\n",
       "      <td>mathlib/src/topology/uniform_space/uniform_emb...</td>\n",
       "      <td>78</td>\n",
       "      <td>63</td>\n",
       "      <td>mathlib/src/topology/uniform_space/uniform_emb...</td>\n",
       "      <td>exact ⟨λ ⟨I, H⟩, ⟨I, λ s su, (H _).2 ⟨s, su, λ...</td>\n",
       "      <td>named</td>\n",
       "      <td>α : Type u_1,\\tβ : Type u_2,\\t_inst_1 : unifor...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>200195</th>\n",
       "      <td>200195</td>\n",
       "      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...</td>\n",
       "      <td>topological_vector_bundle.mem_source_trivializ...</td>\n",
       "      <td>topological_vector_bundle bundle topological_v...</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean</td>\n",
       "      <td>124</td>\n",
       "      <td>61</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean:124:1</td>\n",
       "      <td>apply mem_base_set_trivialization_at</td>\n",
       "      <td>named</td>\n",
       "      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>200196</th>\n",
       "      <td>200196</td>\n",
       "      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...</td>\n",
       "      <td>topological_vector_bundle.mem_source_trivializ...</td>\n",
       "      <td>topological_vector_bundle bundle topological_v...</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean</td>\n",
       "      <td>124</td>\n",
       "      <td>6</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean:124:1</td>\n",
       "      <td>rw topological_fiber_bundle.trivialization.mem...</td>\n",
       "      <td>named</td>\n",
       "      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>200197</th>\n",
       "      <td>200197</td>\n",
       "      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...</td>\n",
       "      <td>topological_vector_bundle.mem_source_trivializ...</td>\n",
       "      <td>topological_vector_bundle bundle topological_v...</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean</td>\n",
       "      <td>124</td>\n",
       "      <td>4</td>\n",
       "      <td>mathlib/src/topology/vector_bundle.lean:124:1</td>\n",
       "      <td>{ rw topological_fiber_bundle.trivialization.m...</td>\n",
       "      <td>solve1</td>\n",
       "      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...</td>\n",
       "      <td>test</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>7902 rows × 12 columns</p>\n",
       "</div>"
      ],
      "text/plain": [
       "        Unnamed: 0                                            goal_pp  \\\n",
       "0                0  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "1                1  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "2                2  α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "3                3  α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "4                4  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "...            ...                                                ...   \n",
       "200025      200025  α : Type u_1,\\nβ : Type u_2,\\n_inst_1 : unifor...   \n",
       "200026      200026  α : Type u_1,\\nβ : Type u_2,\\n_inst_1 : unifor...   \n",
       "200195      200195  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...   \n",
       "200196      200196  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...   \n",
       "200197      200197  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\nE...   \n",
       "\n",
       "                                                decl_name  \\\n",
       "0                                    buffer.read_eq_read'   \n",
       "1                                    buffer.read_eq_read'   \n",
       "2                                    buffer.read_eq_read'   \n",
       "3                                    buffer.read_eq_read'   \n",
       "4                                    buffer.read_eq_read'   \n",
       "...                                                   ...   \n",
       "200025                             uniform_embedding_def'   \n",
       "200026                             uniform_embedding_def'   \n",
       "200195  topological_vector_bundle.mem_source_trivializ...   \n",
       "200196  topological_vector_bundle.mem_source_trivializ...   \n",
       "200197  topological_vector_bundle.mem_source_trivializ...   \n",
       "\n",
       "                                          open_namespaces  \\\n",
       "0                                                  buffer   \n",
       "1                                                  buffer   \n",
       "2                                                  buffer   \n",
       "3                                                  buffer   \n",
       "4                                                  buffer   \n",
       "...                                                   ...   \n",
       "200025             classical filter topological_space set   \n",
       "200026             classical filter topological_space set   \n",
       "200195  topological_vector_bundle bundle topological_v...   \n",
       "200196  topological_vector_bundle bundle topological_v...   \n",
       "200197  topological_vector_bundle bundle topological_v...   \n",
       "\n",
       "                                                 filename  line  column  \\\n",
       "0                           lean/library/data/buffer.lean    49      30   \n",
       "1                           lean/library/data/buffer.lean    49      11   \n",
       "2                           lean/library/data/buffer.lean    49      13   \n",
       "3                           lean/library/data/buffer.lean    49      32   \n",
       "4                           lean/library/data/buffer.lean    49       4   \n",
       "...                                                   ...   ...     ...   \n",
       "200025  mathlib/src/topology/uniform_space/uniform_emb...    78      61   \n",
       "200026  mathlib/src/topology/uniform_space/uniform_emb...    78      63   \n",
       "200195            mathlib/src/topology/vector_bundle.lean   124      61   \n",
       "200196            mathlib/src/topology/vector_bundle.lean   124       6   \n",
       "200197            mathlib/src/topology/vector_bundle.lean   124       4   \n",
       "\n",
       "                                                proof_key  \\\n",
       "0                      lean/library/data/buffer.lean:49:1   \n",
       "1                      lean/library/data/buffer.lean:49:1   \n",
       "2                      lean/library/data/buffer.lean:49:1   \n",
       "3                      lean/library/data/buffer.lean:49:1   \n",
       "4                      lean/library/data/buffer.lean:49:1   \n",
       "...                                                   ...   \n",
       "200025  mathlib/src/topology/uniform_space/uniform_emb...   \n",
       "200026  mathlib/src/topology/uniform_space/uniform_emb...   \n",
       "200195      mathlib/src/topology/vector_bundle.lean:124:1   \n",
       "200196      mathlib/src/topology/vector_bundle.lean:124:1   \n",
       "200197      mathlib/src/topology/vector_bundle.lean:124:1   \n",
       "\n",
       "                                        human_tactic_code tactic_class  \\\n",
       "0       cases b; unfold read read'; simp [array.read_e...    semicolon   \n",
       "1                              cases b; unfold read read'    semicolon   \n",
       "2                                       unfold read read'        named   \n",
       "3                              simp [array.read_eq_read']        named   \n",
       "4                                                 cases b        named   \n",
       "...                                                   ...          ...   \n",
       "200025  simp only [uniform_embedding_def, uniform_cont...    semicolon   \n",
       "200026  exact ⟨λ ⟨I, H⟩, ⟨I, λ s su, (H _).2 ⟨s, su, λ...        named   \n",
       "200195               apply mem_base_set_trivialization_at        named   \n",
       "200196  rw topological_fiber_bundle.trivialization.mem...        named   \n",
       "200197  { rw topological_fiber_bundle.trivialization.m...       solve1   \n",
       "\n",
       "                                             cleaned_goal split  \n",
       "0       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...  test  \n",
       "1       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...  test  \n",
       "2       α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...  test  \n",
       "3       α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...  test  \n",
       "4       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...  test  \n",
       "...                                                   ...   ...  \n",
       "200025  α : Type u_1,\\tβ : Type u_2,\\t_inst_1 : unifor...  test  \n",
       "200026  α : Type u_1,\\tβ : Type u_2,\\t_inst_1 : unifor...  test  \n",
       "200195  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...  test  \n",
       "200196  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...  test  \n",
       "200197  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\tE...  test  \n",
       "\n",
       "[7902 rows x 12 columns]"
      ]
     },
     "execution_count": 145,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df = df[df[\"split\"]==\"test\"]\n",
    "df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 146,
   "id": "6ee0b5d1",
   "metadata": {},
   "outputs": [],
   "source": [
    "dfi = df.merge(df2,left_on=\"cleaned_goal\",right_on=\"prompt\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 147,
   "id": "a8ba1733",
   "metadata": {},
   "outputs": [],
   "source": [
    "dfi = dfi[dfi[\"filename\"].str.contains(\"mathlib\")]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 148,
   "id": "0c558dda",
   "metadata": {},
   "outputs": [],
   "source": [
    "dfi[\"topic\"] = [i.split(\"/\")[2] for i in dfi[\"filename\"]]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 149,
   "id": "5f19f7d5",
   "metadata": {},
   "outputs": [],
   "source": [
    "rsiii =dfi.groupby(\"topic\").mean()[\"score\"].sort_values(ascending=False)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 150,
   "id": "8f156186",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "topic\n",
       "control               0.706960\n",
       "tactic                0.651040\n",
       "computability         0.649710\n",
       "testing               0.593750\n",
       "algebra               0.573117\n",
       "category_theory       0.549169\n",
       "algebraic_topology    0.545299\n",
       "logic                 0.527329\n",
       "data                  0.501841\n",
       "set_theory            0.486266\n",
       "algebraic_geometry    0.470193\n",
       "deprecated            0.459829\n",
       "order                 0.435351\n",
       "group_theory          0.431248\n",
       "number_theory         0.429445\n",
       "measure_theory        0.424553\n",
       "analysis              0.420037\n",
       "linear_algebra        0.406642\n",
       "topology              0.406416\n",
       "ring_theory           0.397458\n",
       "geometry              0.390710\n",
       "combinatorics         0.385952\n",
       "field_theory          0.381898\n",
       "system                0.336364\n",
       "probability_theory    0.276866\n",
       "dynamics              0.268600\n",
       "Name: score, dtype: float64"
      ]
     },
     "execution_count": 150,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rsiii"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 151,
   "id": "60745841",
   "metadata": {},
   "outputs": [],
   "source": [
    "rsiii.to_csv(\"gpt_combined.csv\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8cf7a46b",
   "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.8.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}