{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Language cascades | part 2: Draft, Sketch, Prove\n",
"Tutorial on neural theorem proving\\\n",
"Author: Sean Welleck\n",
"\n",
"----------------\n",
"\n",
"### High-level goal\n",
"\n",
"This notebook will implement a prototype version of [Draft, Sketch, Prove [Jiang et al ICLR 2023]](https://arxiv.org/pdf/2210.12283.pdf):\n",
"\n",
"<img src=\"images/dsp.png\" width=\"800\" />\n",
"\n",
"As pictured above, Draft, Sketch, Prove frames theorem proving as the following procedure. \\\n",
"Given an informal (i.e., Latex) theorem statement $x_I$ and formal theorem statement $x_F$:\n",
"\n",
"1. Generate an *informal* proof $y_{I}\\sim p(\\cdot|x_I,P_{\\text{draft}})$, called a *draft*\n",
"2. Generate a *formal sketch* $z_{F}\\sim p(\\cdot|y_{I}, x_I, x_F, P_{\\text{sketch}})$\n",
"3. Prove the remaining conjectures in the sketch, $y_{F}=f(x_F,z_F)$.\n",
"\n",
"If step $3$ is successful, we will have a verified formal proof of $x_F$. Otherwise we try again. \\\n",
"Conceptually, these steps can be viewed as the following program:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"def dsp(xi, xf, f_draft, f_sketch, f_proof):\n",
" yi = f_draft(xi)\n",
" zf = f_sketch(yi, xi, xf)\n",
" yf = f_proof(xf, zf)\n",
" return yf"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Next, we will discuss how to implement these three modules.\n",
"\n",
"We start by introducing the [Isabelle proof assistant](https://isabelle.in.tum.de/), since it is relevant to the implementation.\n",
"\n",
"\n",
"### Isabelle proof assistant\n",
"\n",
"Draft, Sketch, Prove was originally proposed using a proof assistant called [**Isabelle**](https://isabelle.in.tum.de/).\n",
"\n",
"Isabelle has two relevant properties that are helpful to introduce.\n",
"\n",
"#### 1. Declarative proofs\n",
"First, many Isabelle proofs are structured as a sequence of intermediate conjectures (referred to as a *declarative proof*).\n",
"For example, consider the proof below:\n",
"\n",
"\n",
"<img src=\"images/prove.png\" width=\"500\" />"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In <span style=\"color:blue\">**blue**</span> are the intermediate steps, which include two conjectures:\n",
"1. `c1`, which says that $1*28=n*4$\n",
"2. `c2`, which says that $n=1*28/4$\n",
"\n",
"The final step `then show ?thesis` can be thought of as \"the result follows\".\\\n",
"Intuitively, intermediate conjectures can resemble steps in an informal (latex) proof. \n",
"\n",
"\n",
"Isabelle requires a proof of each step, shown in <span style=\"color:green\">**green**</span>. These often involve lower-level premises or calls to external automation.\\\n",
"To obtain these proofs we can use Sledgehammer:"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### 2. Sledgehammer\n",
"\n",
"Isabelle has a powerful automation tool called **[Sledgehammer](https://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html)** for producing proofs similar to those shown in green.\n",
"\n",
"In practice, a user would write an intermediate conjecture, e.g. `have c1: \"...`, then call Sledgehammer to find a proof of the conjecture:\n",
"\n",
"<img src=\"images/sledgehammer.png\" width=\"800\" />\n",
"\n",
"\n",
"Under the covers, Sledgehammer calls out to classical provers that excel at short, low-level proofs. However, fully proving complex theorems with Sledgehammer is typically intractable due to the large search space (for instance, Sledgehammer wouldn't produce the `have c1` *statement*, even though it can prove the statement).\n",
"\n",
"Our use of Sledgehammer is implemented in the `Checker` class in `dsp_utils.py`. Please see [isabelle_setup.md](../isabelle_setup.md) to set up the proof checker, and modify the `working_dir`, `isa_path`, and `theory_file` paths below accordingly.\n",
"\n",
"Below, we initialize an Isabelle proof checker that can run Sledgehammer:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"import sys\n",
"import os\n",
"sys.path.append('../')\n",
"os.environ['PISA_PATH'] = '/home/seanw/Portal-to-ISAbelle/src/main/python'\n",
"\n",
"import dsp_utils\n",
"\n",
"checker = dsp_utils.Checker(\n",
" working_dir='/home/seanw/Isabelle2022/src/HOL/Examples',\n",
" isa_path='/home/seanw/Isabelle2022',\n",
" theory_file='/home/seanw/Isabelle2022/src/HOL/Examples/Interactive.thy',\n",
" port=9000\n",
")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we send the theorem and proof to the checker. If sledgehammer succeeds at a given step, the result of sledgehammer is added to the proof, and checking proceeds to the next step.\n",
"\n",
"At the end, we get a completed proof:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"----------Path to Isabelle source----------\n",
"/home/seanw/Isabelle2022\n",
"----------Path to Isabelle working directory----------\n",
"/home/seanw/Isabelle2022/src/HOL/Examples\n",
"----------Path to Isabelle theory file----------\n",
"/home/seanw/Isabelle2022/src/HOL/Examples/Interactive.thy\n",
"\n",
"==== Success: True\n",
"--- Complete proof:\n",
"theorem gcd_lcm:\n",
" assumes \"gcd (n :: nat) 4 = 1\" \n",
" and \"lcm (n :: nat) 4 = 28\"\n",
" shows \"n = 7\"\n",
"proof -\n",
"have c1: \"1*28 = n*4\"\n",
"using assms\n",
"by (metis prod_gcd_lcm_nat)\n",
"then\n",
"have c2: \"n = 1*28/4\"\n",
"by auto\n",
"then\n",
"show ?thesis\n",
"by auto\n",
"qed\n"
]
}
],
"source": [
"theorem_and_sledgehammer_proof = \"\"\"theorem gcd_lcm:\n",
" assumes \"gcd (n :: nat) 4 = 1\" \n",
" and \"lcm (n :: nat) 4 = 28\"\n",
" shows \"n = 7\"\n",
"proof -\n",
" have c1: \"1*28 = n*4\" using assms\n",
" sledgehammer\n",
" then have c2: \"n = 1*28/4\"\n",
" sledgehammer\n",
" then show ?thesis\n",
" sledgehammer\n",
"qed\"\"\"\n",
"\n",
"result = checker.check(theorem_and_sledgehammer_proof)\n",
"\n",
"print(\"\\n==== Success: %s\" % result['success'])\n",
"print(\"--- Complete proof:\\n%s\" % result['theorem_and_proof'])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notice that the `sledgehammer` steps are now filled in (e.g. `by (metis prod_gcd_lcm_nat)`)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Cascade\n",
"\n",
"The declarative steps (in blue) and the lower-level proofs of those steps (in green) lead to a nice opportunity for a language model cascade.\n",
"\n",
"Namely, Draft, Sketch, Prove uses a neural language model to \"draft\" an informal proof, \"sketch\" the declarative steps based on the informal proof, then attempts to \"close the gaps\" with Sledgehammer (i.e., prove each step). If the gaps are closed, the steps together with their proofs constitute a verified proof of the original theorem (and of course, this is checked by Isabelle).\n",
"\n",
"\n",
"## Draft and Sketch examples\n",
"To implement the drafting and sketching steps, we provide a few examples in the prompt.\n",
"\n",
"We will derive these examples from ones used in the paper:"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {},
"outputs": [],
"source": [
"import sys\n",
"sys.path.append('../')\n",
"import dsp_utils\n",
"\n",
"import json\n",
"examples = [\n",
" {\"tag\": \"aimeI_2000_p7\", \"category\": \"algebra\", \"metadata\": {}, \"prompt\": \"Informal:\\n(*### Problem\\n\\nSuppose that $x,$ $y,$ and $z$ are three positive numbers that satisfy the equations $xyz = 1,$ $x + \\\\frac {1}{z} = 5,$ and $y + \\\\frac {1}{x} = 29.$ Then $z + \\\\frac {1}{y} = \\\\frac {m}{n},$ where $m$ and $n$ are [[relatively prime]] positive integers. Find $m + n$. Show that it is 5.\\n\\n\\nnote: this is the type of problem that makes you think symmetry, but actually can be solved easily with substitution, and other normal technniques\\n\\n### Solution\\n\\nWe can rewrite $xyz=1$ as $\\\\frac{1}{z}=xy$.\\n\\nSubstituting into one of the given equations, we have \\n$x+xy=5$\\n$x(1+y)=5$\\n$\\\\frac{1}{x}=\\\\frac{1+y}{5}.$\\n\\nWe can substitute back into $y+\\\\frac{1}{x}=29$ to obtain\\n$y+\\\\frac{1+y}{5}=29$\\n$5y+1+y=145$\\n$y=24.$\\n\\nWe can then substitute once again to get\\n$x=\\\\frac15$\\n$z=\\\\frac{5}{24}.$\\nThus, $z+\\\\frac1y=\\\\frac{5}{24}+\\\\frac{1}{24}=\\\\frac{1}{4}$, so $m+n=005$.*)\\n\\nFormal:\\ntheorem\\n fixes x y z :: real\\n and p :: rat\\n assumes \\\"0 < x \\\\<and> 0 < y \\\\<and> 0 < z\\\"\\n and \\\"x * y * z = 1\\\"\\n and \\\"x + 1 / z = 5\\\"\\n and \\\"y + 1 / x = 29\\\"\\n and \\\"z + 1 / y = p\\\"\\n and \\\"0 < p\\\" \\n shows \\\"let (m,n) = quotient_of p in m + n = 5\\\"\\nproof -\\n (* We can rewrite $xyz=1$ as $\\\\frac{1}{z}=xy$. *)\\n have c0: \\\"z = 1 / (x*y)\\\"\\n sledgehammer\\n (* Substituting into one of the given equations, we have \\n $x+xy=5$\\n $x(1+y)=5$\\n $\\\\frac{1}{x}=\\\\frac{1+y}{5}.$ *)\\n have c1: \\\"1 / x = (1+y) / 5\\\" \\n proof -\\n have \\\"x + x * y = 5\\\" using assms(3) unfolding c0\\n sledgehammer\\n then have \\\"x * (1 + y) = 5\\\"\\n sledgehammer\\n then have t1: \\\"x = 5 / (1+y)\\\"\\n sledgehammer\\n then show ?thesis\\n sledgehammer\\n qed\\n (* We can substitute back into $y+\\\\frac{1}{x}=29$ to obtain\\n $y+\\\\frac{1+y}{5}=29$\\n $5y+1+y=145$\\n $y=24.$ *)\\n have \\\"y + (1+y)/5 = 29\\\" using assms(4) unfolding c1 sledgehammer\\n then have \\\"5* (y + (1+y)/5) = 5 * 29\\\" sledgehammer\\n also have \\\"... = 145\\\" sledgehammer\\n finally have c2_1: \\\"5* (y + (1+y)/5) = 145\\\" sledgehammer\\n have \\\"5* (y + (1+y)/5) = 5*y + (1+y)\\\" sledgehammer\\n also have \\\"... = 6*y + 1\\\" sledgehammer\\n finally have c2_2: \\\"5* (y + (1+y)/5) = 6*y + 1\\\" sledgehammer\\n have \\\"6*y + 1 = 145\\\" using c2_1 c2_2 sledgehammer\\n then have c2: \\\"y = 24\\\" sledgehammer\\n (* We can then substitute once again to get\\n $x=\\\\frac15$\\n $z=\\\\frac{5}{24}.$ *)\\n have \\\"1/x = 5\\\" using c1 unfolding c2 sledgehammer\\n then have c3: \\\"x = 1/5\\\"\\n sledgehammer\\n then have c4: \\\"z = 5/24\\\"\\n sledgehammer\\n (* Thus, $z+\\\\frac1y=\\\\frac{5}{24}+\\\\frac{1}{24}=\\\\frac{1}{4}$, so $m+n=005$. *)\\n have \\\"p = z + 1/y\\\" using assms(5) sledgehammer\\n also have \\\"... = 5/24 + 1/24\\\" unfolding c2 c4 sledgehammer\\n also have \\\"... = 1/4\\\" sledgehammer\\n finally have c5: \\\"p = 1/4\\\"\\n sledgehammer\\n have \\\"quotient_of p = (1, 4)\\\" unfolding c5 sledgehammer\\n then show ?thesis sledgehammer\\nqed\"},\n",
" {\"tag\": \"algebra_2rootsintpoly_am10tap11eqasqpam110\", \"category\": \"algebra\", \"metadata\": {}, \"prompt\": \"Informal:\\n(*### Problem\\n\\nShow that for any complex number a, $(a-10)(a+11) = a^2 + a - 110$.\\n\\n### Solution\\n\\nWe first expand all terms of the left hand side to get $a^2 - 10a + 11a - 10*11$.\\nThis equals $a^2 + a - 10*11 = a^2 + a - 110$.*)\\n\\nFormal:\\ntheorem\\n fixes a :: complex\\n shows \\\"(a-10) * (a+11) = a^2 + a -110\\\"\\nproof -\\n (* We first expand all terms of the left hand side to get $a^2 - 10a + 11a - 10*11$. *)\\n have \\\"(a-10) * (a+11) = a^2 - 10*a + 11*a - 10 *11\\\"\\n sledgehammer\\n (* This equals $a^2 + a - 10*11 = a^2 + a - 110$. *)\\n also have \\\"\\\\<dots> = a^2 + a - 10 * 11\\\"\\n sledgehammer\\n also have \\\"\\\\<dots> = a^2 + a - 110\\\"\\n sledgehammer\\n finally show ?thesis\\n sledgehammer\\nqed\"},\n",
" {\"tag\": \"mathd_numbertheory_335\", \"category\": \"number_theory\", \"metadata\": {}, \"prompt\": \"Informal:\\n(*### Problem\\n\\nWhen Rachel divides her favorite number by 7, she gets a remainder of 5. What will the remainder be if she multiplies her favorite number by 5 and then divides by 7? Show that it is 4.\\n\\n### Solution\\n\\nLet $n$ be Rachel's favorite number. \\nThen $n \\\\equiv 5 \\\\pmod{7}$, so $5n \\\\equiv 5 \\\\cdot 5 \\\\equiv 25 \\\\equiv 4 \\\\pmod{7}$.\\n*)\\n\\nFormal:\\ntheorem\\n fixes n :: nat\\n assumes h0 : \\\"n mod 7 = 5\\\"\\n shows \\\"(5 * n) mod 7 = 4\\\"\\nproof -\\n (* Then $n \\\\equiv 5 \\\\pmod{7}$, so $5n \\\\equiv 5 \\\\cdot 5 \\\\equiv 25 \\\\equiv 4 \\\\pmod{7}$. *)\\n have c0:\\\"(5 * n) mod 7 = (5 * 5) mod 7\\\" using h0\\n sledgehammer\\n then have \\\"\\\\<dots> = 4\\\" sledgehammer\\n then have \\\"(5 * n) mod 7 = 4\\\" using c0 sledgehammer\\n then show ?thesis sledgehammer\\nqed\"}\n",
"]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Draft\n",
"\n",
"This function generates an *informal* proof $y_{I}\\sim p(\\cdot|x_I,P_{\\text{draft}})$, called a *draft*.\n",
"\n",
"Here, $P_{\\text{draft}}$ is a prompt containing examples of mapping the informal theorem statement $x_I$ to an informal proof $y_I$:\n"
]
},
{
"cell_type": "code",
"execution_count": 51,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Draft an informal solution similar to below. \n",
"The informal solution will be used to sketch a formal Isabelle proof.\n",
"Here are some examples:\n",
"Example:\n",
"Informal:\n",
"(*### Problem\n",
"\n",
"Suppose that $x,$ $y,$ and $z$ are three positive numbers that satisfy the equations $xyz = 1,$ $x + \\frac {1}{z} = 5,$ and $y + \\frac {1}{x} = 29.$ Then $z + \\frac {1}{y} = \\frac {m}{n},$ where $m$ and $n$ are [[relatively prime]] positive integers. Find $m + n$. Show that it is 5.\n",
"\n",
"\n",
"note: this is the type of problem that makes you think symmetry, but actually can be solved easily with substitution, and other normal technniques\n",
"\n",
"### Solution\n",
"\n",
"We can rewrite $xyz=1$ as $\\frac{1}{z}=xy$.\n",
"\n",
"Substituting into one of the given equations, we have \n",
"$x+xy=5$\n",
"$x(1+y)=5$\n",
"$\\frac{1}{x}=\\frac{1+y}{5}.$\n",
"\n",
"We can substitute back into $y+\\frac{1}{x}=29$ to obtain\n",
"$y+\\frac{1+y}{5}=29$\n",
"$5y+1+y=145$\n",
"$y=24.$\n",
"\n",
"We can then substitute once again to get\n",
"$x=\\frac15$\n",
"$z=\\frac{5}{24}.$\n",
"Thus, $z+\\frac1y=\\frac{5}{24}+\\frac{1}{24}=\\frac{1}{4}$, so $m+n=005$.*)\n",
"\n",
"\n",
"\n",
"Example:\n",
"Informal:\n",
"(*### Problem\n",
"\n",
"Show that for any complex number a, $(a-10)(a+11) = a^2 + a - 110$.\n",
"\n",
"### Solution\n",
"\n",
"We first expand all terms of the left hand side to get $a^2 - 10a + 11a - 10*11$.\n",
"This equals $a^2 + a - 10*11 = a^2 + a - 110$.*)\n",
"\n",
"\n",
"\n",
"Example:\n",
"Informal:\n",
"(*### Problem\n",
"\n",
"When Rachel divides her favorite number by 7, she gets a remainder of 5. What will the remainder be if she multiplies her favorite number by 5 and then divides by 7? Show that it is 4.\n",
"\n",
"### Solution\n",
"\n",
"Let $n$ be Rachel's favorite number. \n",
"Then $n \\equiv 5 \\pmod{7}$, so $5n \\equiv 5 \\cdot 5 \\equiv 25 \\equiv 4 \\pmod{7}$.\n",
"*)\n",
"\n",
"\n",
"\n",
"Informal:\n",
"(*### Problem\n",
"\n",
"\n"
]
}
],
"source": [
"prompt = \"\"\"Draft an informal solution similar to below. \n",
"The informal solution will be used to sketch a formal Isabelle proof.\n",
"Here are some examples:\n",
"\"\"\"\n",
"for x in examples:\n",
" prompt += (\"Example:\\n\" + x['prompt'][:x['prompt'].find('Formal:')] + \"\\n\\n\")\n",
"prompt += \"\"\"Informal:\n",
"(*### Problem\n",
"\n",
"\"\"\"\n",
"\n",
"print(prompt)"
]
},
{
"cell_type": "code",
"execution_count": 44,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"### Solution\n",
"\n",
"If x is even, then it can be represented as 2n where n is some integer.\n",
"So x + 5 equals 2n + 5.\n",
"We can rewrite 2n + 5 as 2(n + 2) + 1, which is in the form of 2k + 1 where k is an integer (in this case, n + 2). Thus, x + 5 is odd.\n"
]
}
],
"source": [
"p = dsp_utils.LMFunction('gpt-4')\n",
"xi = 'Show that if x is even, then x+5 is odd'\n",
"yi = p.f(prompt, xi)\n",
"print(yi)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Sketch\n",
"\n",
"Generate a *formal sketch* $z_{F}\\sim p(\\cdot|y_{I}, x_I, x_F, P_{\\text{sketch}})$\n",
"\n",
"Here, $P_{\\text{sketch}}$ is a prompt containing the examples from the drafting step with an additional formal sketch."
]
},
{
"cell_type": "code",
"execution_count": 55,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Formal:\n",
"proof -\n",
" (* If x is even, then it can be represented as 2n where n is some integer. *)\n",
" obtain n where c1: \"x = 2*n\"\n",
" using evenE assms\n",
" sledgehammer\n",
" (* So x + 5 equals 2n + 5. *)\n",
" then have \"x + 5 = 2*n + 5\" \n",
" sledgehammer\n",
" (* We can rewrite 2n + 5 as 2(n + 2) + 1, which is in the form of 2k + 1 where k is an integer (in this case, n + 2). Thus, x + 5 is odd. *)\n",
" also have \"\\<dots> = 2*(n+2) + 1\"\n",
" sledgehammer\n",
" then have exI: \"\\<exists>k. x + 5 = 2*k+1\" \n",
" sledgehammer\n",
" then have \"odd (x+5)\" \n",
" sledgehammer\n",
" then show ?thesis \n",
" sledgehammer\n",
"qed\n"
]
}
],
"source": [
"prompt = \"\"\"Translate the informal solution into a sketch of the\n",
"formal Isabelle proof. Add `sledgehammer` in the sketch whenever\n",
"possible. `sledgehammer` will be used to call the automated Sledgehammer prover. \n",
"Here are some examples:\n",
"\"\"\"\n",
"for x in examples:\n",
" prompt += (x['prompt'] + \"\\n\\n\")\n",
"prompt += \"\"\"Informal:\n",
"(*### Problem\n",
"\n",
"\"\"\"\n",
"\n",
"xf = \"\"\"theorem\n",
"fixes x :: int\n",
"assumes h0: \"even x\"\n",
"shows \"odd (x+5)\" \"\"\"\n",
"\n",
"zi = p.f(prompt, xi + '\\n\\n' + yi + '\\n\\n' + xf)\n",
"print(zi)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Proof\n",
"\n",
"Finally, we call [Sledgehammer](https://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html) to prove the remaining intermediate conjectures.\n",
"\n",
"You can see the completed proof printed in the cell output:\n"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"----------Path to Isabelle source----------\n",
"/home/seanw/Isabelle2022\n",
"----------Path to Isabelle working directory----------\n",
"/home/seanw/Isabelle2022/src/HOL/Examples\n",
"----------Path to Isabelle theory file----------\n",
"/home/seanw/Isabelle2022/src/HOL/Examples/Interactive.thy\n",
"\n",
"==== Success: True\n",
"--- Complete proof:\n",
"theorem\n",
"fixes x :: int\n",
"assumes h0: \"even x\"\n",
"shows \"odd (x+5)\"\n",
"proof -\n",
"(* If x is even, then it can be represented as 2n where n is some integer. *)\n",
"obtain n where c1: \"x = 2*n\"\n",
"using evenE assms\n",
"by auto\n",
"(* So x + 5 equals 2n + 5. *)\n",
"then\n",
"have \"x + 5 = 2*n + 5\"\n",
"by auto\n",
"(* We can rewrite 2n + 5 as 2(n + 2) + 1, which is in the form of 2k + 1 where k is an integer (in this case, n + 2). Thus, x + 5 is odd. *)\n",
"also\n",
"have \"\\<dots> = 2*(n+2) + 1\"\n",
"by auto\n",
"then\n",
"have exI: \"\\<exists>k. x + 5 = 2*k+1\"\n",
"using c1 by blast\n",
"then\n",
"have \"odd (x+5)\"\n",
"by presburger\n",
"then\n",
"show ?thesis\n",
"by auto\n",
"qed\n"
]
}
],
"source": [
"theorem_with_proof = \"\"\"theorem\n",
"fixes x :: int\n",
"assumes h0: \"even x\"\n",
"shows \"odd (x+5)\"\n",
"proof -\n",
" (* If x is even, then it can be represented as 2n where n is some integer. *)\n",
" obtain n where c1: \"x = 2*n\"\n",
" using evenE assms\n",
" sledgehammer\n",
" (* So x + 5 equals 2n + 5. *)\n",
" then have \"x + 5 = 2*n + 5\" \n",
" sledgehammer\n",
" (* We can rewrite 2n + 5 as 2(n + 2) + 1, which is in the form of 2k + 1 where k is an integer (in this case, n + 2). Thus, x + 5 is odd. *)\n",
" also have \"\\<dots> = 2*(n+2) + 1\"\n",
" sledgehammer\n",
" then have exI: \"\\<exists>k. x + 5 = 2*k+1\" \n",
" sledgehammer\n",
" then have \"odd (x+5)\" \n",
" sledgehammer\n",
" then show ?thesis \n",
" sledgehammer\n",
"qed\"\"\"\n",
"\n",
"result = checker.check(theorem_with_proof)\n",
"\n",
"print(\"\\n==== Success: %s\" % result['success'])\n",
"print(\"--- Complete proof:\\n%s\" % result['theorem_and_proof'])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We now have a verified formal proof of the the claim \"If x is even, then x+5 is odd\", and the proof is annotated with informal proof steps as comments (the text inside of `(*....*)`. Pretty cool!"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Proof search\n",
"\n",
"In the simple example above, the formal proof was successful on the first try.\n",
"\n",
"In more complex settings we need to try multiple times. \n",
"\n",
"Namely, we can sample multiple drafts, sample multiple formal sketches for each draft, then see if any of them can be successfully proved with Sledgehammer:\n",
"\n",
"<img src=\"./images/dsp_search.png\" width=\"800px\">\n",
"\n",
"This proof search algorithm is different from the best-first search in next-step suggestion. Namely, it:\n",
"1. narrows the search space to proofs that are \"similar to\" the informal proof\\*\n",
"2. does not interact with the proof assistant after each step\n",
"\n",
"\\*Though ultimately it is up to the neural language model to decide how to use the informal proof (if at all)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Scaling up proof search\n",
"\n",
"The Draft, Sketch, Prove paper shows the effect of scaling up proof search; that is, sampling multiple drafts and/or multiple formal sketches and attempting to verify them.\n",
"\n",
"Namely, proof search with a single sampled sequence yielded less than 100 successful proofs, but scaling to 100 sampled drafts and/or sketches yielded almost 200 successful proofs:\n",
"\n",
"<img src=\"./images/dsp_plot.png\" width=\"500px\">"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Naturally, a better model would require a smaller search budget when measured in terms of number of calls to the model. For instance, imagine a very good model that proved the same ~200 theorems on its first try. This would require fewer calls to the model than above.\n",
"\n",
"Second, the search algorithm used was fairly naive (temperature sampling that only interacts with the proof assistant once). A better search algorithm could yield more successful proofs, and/or a smaller search budget to reach a given number of successful proofs."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Examples\n",
"\n",
"Here is an interesting example from the Draft, Sketch, Prove paper. It shows how the neural model can generate an informal proof that differs from the human-written informal proof. The resulting sketches, and formal proofs produced by the system are much different:\n",
"\n",
"<img src=\"images/dsp_example.png\" width=\"600px\">"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Feel free to play around with the gpt-4 based implementation above to see what it can do."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"----------------------\n",
"\n",
"# Other cascades\n",
"\n",
"[Baldur [First et al 2023]](https://arxiv.org/pdf/2303.04910.pdf) develop a **refinement**, or *proof repair*, module to correct proofs using error messages $e$:\n",
"\n",
"- $y_F^1\\sim p(\\cdot|x_F)$\n",
"- $y_F^{2}\\sim p(\\cdot|x_F,y_F^1,e)$\n",
"\n",
"\n",
"[pySagredo [Azerbayev 2023]](https://github.com/zhangir-azerbayev/pySagredo) is an experimental tactic that uses refinement and GPT-4 to prove theorems in Lean4.\n",
"\n",
"\n",
"More generally, integrating modern language models with proof assistants remains an active area of research."
]
},
{
"cell_type": "markdown",
"metadata": {},
"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.10.11"
}
},
"nbformat": 4,
"nbformat_minor": 4
}