aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

examples with leni

This commit is contained in:
Brando Miranda 2024-09-26 20:20:32 -07:00
parent 0d278e1343
commit d2f53ccc80
15 changed files with 1428 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
examples/lean4_dsp/debug/khan_debug.jsonl Normal file
View File

@ -0,0 +1,3 @@
{"problem": "$ E = \\left[\\begin{array}{rr}5 & 1 \\\\ 2 & 3\\end{array}\\right]$ What is the determinant of $ E$ ?", "hints": ["The determinant of a 2x2 matrix can be computed the following way:", "$ = $", "In this specific case,", "$ = $", "$ = 13 $"]}
{"problem": "If $a + b + c = 9$, what is $7c + 7a + 7b$ ?", "hints": ["$= 7a + 7b + 7c$", "$= (7) \\cdot (a + b + c) $", "$= (7) \\cdot (9) $", "$= 63$"]}
{"problem": "Find $\\lim_{x\\to\\infty}\\dfrac{x^2-4}{\\cos(x)}$. Choose 1 answer: Choose 1 answer: (Choice A) A $4$ (Choice B) B $-2$ (Choice C) C $0$ (Choice D) D The limit doesn't exist", "hints": ["When dealing with limits that include $\\cos(x)$, it's important to remember that $\\lim_{x\\to\\infty}\\cos(x)$ doesn't exist, as $\\cos(x)$ keeps oscillating between $-1$ and $1$ forever. ${2}$ ${4}$ ${6}$ ${8}$ ${\\llap{-}4}$ ${\\llap{-}6}$ ${\\llap{-}8}$ ${2}$ $y$ $x$ $y=\\cos(x)$ This doesn't necessarily mean that our limit doesn't exist. Think what happens to $\\dfrac{x^2-4}{\\cos(x)}$ as $x$ increases towards positive infinity.", "While $x^2-4$ keeps growing boundlessly, $\\cos(x)$ oscillates from $-1$, to $0$, to $1$, to $0$, to $-1$ again. The result is a graph that goes up and down forever, with vertical asymptotes every now and then. ${5}$ ${10}$ ${15}$ ${\\llap{-}5}$ ${\\llap{-}10}$ ${\\llap{-}15}$ ${50}$ ${100}$ ${150}$ ${\\llap{-}50}$ ${\\llap{-}100}$ ${\\llap{-}150}$ $y$ $x$ $y=\\dfrac{x^2-4}{\\cos(x)}$ This limit doesn't approach any specific value as $x$ increases towards infinity.", "In conclusion, $\\lim_{x\\to\\infty}\\dfrac{x^2-4}{\\cos(x)}$ doesn't exist."]}

3
examples/lean4_dsp/debug/mathematica_debug.jsonl Normal file
View File

File diff suppressed because one or more lines are too long

10
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/n_plus_zero_full_proof.json Normal file
View File

@ -0,0 +1,10 @@
{
"problem": "For any natural number n, n + 0 = n.",
"level": "SF foundations level 1",
"type": "Algebra",
"solution": [
"Consider some natural number n. The proof will be by induction. Consider the base case n=0. We have 0 + 0 = 0 which holds by the definition of addion.",
"Now the inductive case we want to show n'+1 + 0 = n'+1. Assume it holds for n i.e., n' + 0 = n. So now by the we know the LHS is equal to (n'+0) + 1.",
"Then by the induction hypothesis we know the LHS simplifies to n'+1 completing the proof. Qed."
]
}

6
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_full_proof.json Normal file
View File

@ -0,0 +1,6 @@
{
"problem": "For any natural number n, 0 + n = n.",
"level": "SF foundations level 1",
"type": "Algebra",
"solution": "Consider some natural number n. We now want to show 0 + n = n. Using addition both sides are equal."
}

6
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_proof.json Normal file
View File

@ -0,0 +1,6 @@
{
"problem": "For any natural number n, 0 + n = n.",
"level": "SF foundations level 1",
"type": "Algebra",
"solution": "Consider some natural number n. We now want to show 0 + n = n. For that we use the definition of addition to get n = n and conclude both sides are equal (by reflexity)."
}

25
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug3_sf.json Normal file
View File

@ -0,0 +1,25 @@
[
{
"problem": "For any natural number n, 0 + n = n.",
"level": "SF foundations level 1",
"type": "Logical Foundations",
"solution": [
"Consider some natural number n. We want to show 0 + n = n. ",
"By using definition of addition on both sides, LHS and RHS are now equal, done."
]
},
{
"problem": "For any natural number n, n + 0 = n.",
"level": "SF foundations level 1",
"type": "Logical Foundations",
"solution": [
"Consider some natural number n. The proof will be by induction. ",
"The base case n=0, so we have 0 + 0 = 0, which holds by the definition of addion. ",
"Consider the inductive case, so we want to show (k + 1) + 0 = (k + 1) for any k < n assuming the IH holds for such k (IH: k + 0 = k). ",
"By the IH we have (k + 1) + 0 = (k + 1). ",
"By def of addition we have (k + 0) + 1 = (k + 1). ",
"By the induction hypothesis (IH) we have k + 0 = k. ",
"LHS and RHS are equal so proof is complete."
]
}
]

368
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug4_sf.json Normal file
View File

@ -0,0 +1,368 @@
[
{
"nl_problem": "For any natural number n, n + 0 = n.",
"nl_solution": [
"Consider some natural number n. We want to show n + 0 = n. ",
"By using fats of addition on both sides, LHS and RHS are now equal, done."
],
"fl_problem": "theorem n_plus_zero : ∀ n : ℕ, n + 0 = n := by",
"fl_solution": [
"-- Prove that n + 0 = n.\n",
"theorem n_plus_zero : ∀ n : ℕ, n + 0 = n := by\n",
" -- Consider some n in Nats.\n",
" intro n",
"-- Using facts of addition simplify n + 0 to n.\n",
" rw [Nat.add_zero]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
],
"nl_problem_proved_sketch": "For any natural number n, n + 0 = n.",
"nl_solution_proved_sketch": [
"We want to show n + 0 = n. ",
"We have the fact of addition that, n + 0 = n. ",
"Thus, the left-hand side and right-hand side are equal, which completes the proof."
],
"fl_problem_proved_sketch": "theorem n_plus_zero_proved_formal_sketch : ∀ n : ℕ, n + 0 = n := by",
"fl_solution_proved_sketch": [
"-- Prove that n + 0 = n via a formal proof sketch",
"theorem n_plus_zero_proved_formal_sketch : ∀ n : ℕ, n + 0 = n := by",
" -- We have the fact of addition n + 0 = n, use it to show left and right are equal.",
" have h_nat_add_zero: ∀ n : ℕ, n + 0 = n := Nat.add_zero",
" exact h_nat_add_zero"
],
"src_header_fl_solution_proved_sketch": ["import Mathlib.Data.Nat.Basic"],
"nl_problem_proved_sketch_aesop": "For any natural number n, n + 0 = n.",
"nl_solution_proved_sketch_aesop": [
"We want to show n + 0 = n. ",
"We have the fact of addition that, n + 0 = n. ",
"Thus, the left-hand side and right-hand side are equal, which completes the proof."
],
"fl_problem_proved_sketch_aesop": "theorem n_plus_zero_proved_formal_sketch' : ∀ n : ℕ, n + 0 = n := by",
"fl_solution_proved_sketch_aesop": [
"-- Prove that n + 0 = n via a formal proof sketch with aesop. ",
"theorem n_plus_zero_proved_formal_sketch' : ∀ n : ℕ, n + 0 = n := by",
" -- We have the fact of addition n + 0 = n, use it to show left and right are equal. ",
" have h_nat_add_zero: ∀ n : ℕ, n + 0 = n := by aesop",
" exact h_nat_add_zero"
],
"src_header_fl_solution_proved_sketch_aesop": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
]
},
{
"nl_problem": "For any natural number n, 0 + n = n.",
"nl_solution": [
"Consider some natural number n. We want to show 0 + n = n.",
"By using facts of addition and induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem zero_plus_n : ∀ n : ℕ, 0 + n = n := by",
"fl_solution": [
"-- Prove that 0 + n = n by induction",
"theorem zero_plus_n : ∀ n : ℕ, 0 + n = n := by",
"-- Consider some n in Nats.",
"intro n",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: 0 + 0 = 0",
"rw [Nat.add_zero]",
"| succ n ih =>",
"-- Inductive step: assume 0 + n = n, prove 0 + succ n = succ n",
"rw [Nat.add_succ]",
"rw [ih]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
],
"nl_problem_proved_sketch": "For any natural number n, 0 + n = n.",
"nl_solution_proved_sketch": [
"We want to show 0 + n = n.",
"By using the fact of addition and performing induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem_proved_sketch": "theorem zero_plus_n_proved_formal_sketch : ∀ n : ℕ, 0 + n = n := by",
"fl_solution_proved_sketch": [
"-- Prove that 0 + n = n by induction via a formal proof sketch",
"theorem zero_plus_n_proved_formal_sketch : ∀ n : ℕ, 0 + n = n := by",
"-- Consider some n in Nats.",
"intro n",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: 0 + 0 = 0",
"have h_base: 0 + 0 = 0 := by rw [Nat.add_zero]",
"exact h_base",
"| succ n ih =>",
"-- Inductive step: assume 0 + n = n, prove 0 + succ n = succ n",
"have h_inductive: 0 + Nat.succ n = Nat.succ n := by",
"rw [Nat.add_succ]",
"rw [ih]",
"exact h_inductive"
],
"src_header_fl_solution_proved_sketch": [
"import Mathlib.Data.Nat.Basic"
],
"nl_problem_proved_sketch_aesop": "For any natural number n, 0 + n = n.",
"nl_solution_proved_sketch_aesop": [
"We want to show 0 + n = n.",
"By using the fact of addition and performing induction on n, we can prove the statement for both the base case and the inductive step using aesop."
],
"fl_problem_proved_sketch_aesop": "theorem zero_plus_n_proved_formal_sketch' : ∀ n : ℕ, 0 + n = n := by",
"fl_solution_proved_sketch_aesop": [
"-- Prove that 0 + n = n by induction via a formal proof sketch with aesop.",
"theorem zero_plus_n_proved_formal_sketch' : ∀ n : ℕ, 0 + n = n := by",
"-- Consider some n in Nats.",
"intro n",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: 0 + 0 = 0",
"have h_base: 0 + 0 = 0 := by aesop",
"exact h_base",
"| succ n ih =>",
"-- Inductive step: assume 0 + n = n, prove 0 + succ n = succ n",
"have h_inductive: 0 + Nat.succ n = Nat.succ n := by aesop",
"exact h_inductive"
],
"src_header_fl_solution_proved_sketch_aesop": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
]
},
{
"nl_problem": "For any natural numbers n and m we have commutativity, n + m = m + n.",
"nl_solution": [
"Consider some natural numbers n and m. We want to show n + m = m + n.",
"By using facts of addition and induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_comm_normal : ∀ n m : ℕ, n + m = m + n := by",
"fl_solution": [
"-- Prove that n + m = m + n",
"theorem add_comm_normal : ∀ n m : ℕ, n + m = m + n := by",
"-- Consider some n and m in Nats.",
"intros n m",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + m = m + 0.",
"-- Using the definition of addition, 0 + m = m and m + 0 = m.",
"rw [Nat.zero_add, Nat.add_zero]",
"| succ n ih =>",
"-- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.",
"-- We use the fact n + (m + 1) = (n + m) + 1.",
"have plus_n_Sm_normal: ∀ n m : ℕ, n + (m + 1) = (n + m) + 1 := by",
" intros n m",
" rw [Nat.add_succ]",
"-- Apply the fact to rewrite succ n + m = (n + m) + 1.",
"rw [Nat.add_succ, Nat.add_zero]",
"rw [← ih]",
"rw [Nat.succ_add]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
]
},
{
"nl_problem": "For any natural numbers n and m, n + m = m + n.",
"nl_solution": [
"Consider some natural numbers n and m. We want to show n + m = m + n.",
"By using the fact of addition and performing induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_comm_proved_formal_sketch : ∀ n m : ℕ, n + m = m + n := by",
"fl_solution": [
"-- Prove that n + m = m + n via a formal proof sketch",
"theorem add_comm_proved_formal_sketch : ∀ n m : ℕ, n + m = m + n := by",
"-- Consider some n and m in Nats.",
"intros n m",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + m = m + 0.",
"-- We have the fact 0 + m = m by the definition of addition.",
"have h_base: 0 + m = m := Nat.zero_add m",
"-- We also have the fact m + 0 = m by the definition of addition.",
"have h_symm: m + 0 = m := Nat.add_zero m",
"-- Combining these, we get 0 + m = m + 0.",
"rw [h_base, h_symm]",
"| succ n ih =>",
"-- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.",
"-- By the inductive hypothesis, we have n + m = m + n.",
"have h_inductive: n + m = m + n := ih",
"-- proof is:",
"-- We eventually want to flip n + m and simplify to make both sides the same. Thus,",
"-- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.",
"have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := by rw [Nat.add_succ]",
"-- 2. then to flip m + S n to something like S (n + m) we need to use the IH.",
"have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := by rw [h_inductive]",
"-- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.",
"have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := by rw [Nat.succ_add]",
"-- Combining these, we get succ n + m = m + succ n.",
"rw [h_pull_succ_out_from_right, ←h_flip_n_plus_m, h_pull_succ_out_from_left]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
]
},
{
"nl_problem": "For any natural numbers n and m, n + m = m + n.",
"nl_solution": [
"Consider some natural numbers n and m. We want to show n + m = m + n.",
"By using the fact of addition and performing induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_comm_proved_formal_sketch_aesop : ∀ n m : ℕ, n + m = m + n := by",
"fl_solution": [
"-- Prove that n + m = m + n via a formal proof sketch with aesop.",
"theorem add_comm_proved_formal_sketch_aesop : ∀ n m : ℕ, n + m = m + n := by",
"-- Consider some n and m in Nats.",
"intros n m",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + m = m + 0.",
"-- We have the fact 0 + m = m by the definition of addition.",
"have h_base: 0 + m = m := by aesop",
"-- We also have the fact m + 0 = m by the definition of addition.",
"have h_symm: m + 0 = m := by aesop",
"-- Combining these, we get 0 + m = m + 0.",
"rw [h_base, h_symm]",
"| succ n ih =>",
"-- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.",
"-- By the inductive hypothesis, we have n + m = m + n.",
"have h_inductive: n + m = m + n := by aesop",
"-- proof is:",
"-- We eventually want to flip n + m and simplify to make both sides the same. Thus,",
"-- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.",
"have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := by aesop",
"-- 2. then to flip m + S n to something like S (n + m) we need to use the IH.",
"have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := by aesop",
"-- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.",
"have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := by rw [Nat.succ_add]",
"-- Combining these, we get succ n + m = m + succ n.",
"rw [h_pull_succ_out_from_right, ←h_flip_n_plus_m, h_pull_succ_out_from_left]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
]
},
{
"nl_problem": "Prove that for any natural numbers n, m, and p, n + (m + p) = (n + m) + p.",
"nl_solution": [
"Consider some natural numbers n, m, and p. We want to show n + (m + p) = (n + m) + p.",
"By using facts of addition and induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_assoc_normal : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"fl_solution": [
"-- Prove that n + (m + p) = (n + m) + p",
"theorem add_assoc_normal : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"-- Consider some n, m, and p in Nats.",
"intros n m p",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + (m + p) = (0 + m) + p.",
"-- Using the definition of addition, 0 + (m + p) = m + p and (0 + m) + p = m + p.",
"rw [Nat.zero_add, Nat.zero_add]",
"| succ n ih =>",
"-- Inductive step: Assume n + (m + p) = (n + m) + p, we need to show succ n + (m + p) = (succ n + m) + p.",
"-- proof strategy is, we move succ n out (or in) enough times then use the IH until both sides are the same.",
"-- 1. let's start by pulling out the succ from the left side and have the entire addition inside the succ.",
"rw [Nat.succ_add]",
"-- 2. Now that we have the IH hypothesis appearing inside the left, let's apply it so we have n + (m + p) = (n + m) + p.",
"rw [ih]",
"-- 3. Now that the parentheses (apps of plus) are in the right place for both sides, push the succ on the left twice so both terms are the same.",
"rw [← Nat.succ_add, ← Nat.succ_add]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
]
},
{
"nl_problem": "Prove that for any natural numbers n, m, and p, n + (m + p) = (n + m) + p.",
"nl_solution": [
"Consider some natural numbers n, m, and p. We want to show n + (m + p) = (n + m) + p.",
"By using facts of addition and induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_assoc_proved_formal_sketch : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"fl_solution": [
"-- Prove that n + (m + p) = (n + m) + p",
"theorem add_assoc_proved_formal_sketch : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"-- Consider some n, m, and p in Nats.",
"intros n m p",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + (m + p) = (0 + m) + p.",
"-- Using the definition of addition, 0 + (m + p) = m + p and (0 + m) + p = m + p.",
"rw [Nat.zero_add, Nat.zero_add]",
"| succ n ih =>",
"-- Inductive step: Assume n + (m + p) = (n + m) + p, we need to show succ n + (m + p) = (succ n + m) + p.",
"-- proof strategy is, we move succ n out (or in) enough times then use the IH until both sides are the same.",
"-- 1. let's start by pulling out the succ from the left side and have the entire addition inside the succ.",
"have h_pull_add_succ_out_from_left: Nat.succ n + (m + p) = Nat.succ (n + (m + p)) := by rw [Nat.succ_add]",
"-- 2. Now that we have the IH hypothesis appearing inside the left, let's apply it so we have n + (m + p) = (n + m) + p.",
"have h_inside_left_associates: Nat.succ (n + (m + p)) = Nat.succ ((n + m) + p) := by rw [ih]",
"-- 3. Now that the parentheses (apps of plus) are in the right place for both sides, push the succ on the left twice so both terms are the same.",
"have h_push_succ_in_left_twice: Nat.succ ((n + m) + p) = ((Nat.succ n) + m) + p := by rw [← Nat.succ_add, ← Nat.succ_add]",
"-- Combining these, we get succ n + (m + p) = (succ n + m) + p.",
"rw [h_pull_add_succ_out_from_left, h_inside_left_associates, h_push_succ_in_left_twice]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic"
]
},
{
"nl_problem": "Prove that for any natural numbers n, m, and p, n + (m + p) = (n + m) + p.",
"nl_solution": [
"Consider some natural numbers n, m, and p. We want to show n + (m + p) = (n + m) + p.",
"By using facts of addition and induction on n, we can prove the statement for both the base case and the inductive step."
],
"fl_problem": "theorem add_assoc_proved_formal_sketch_aesop : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"fl_solution": [
"-- Prove that n + (m + p) = (n + m) + p via a formal proof sketch with aesop",
"theorem add_assoc_proved_formal_sketch_aesop : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by",
"-- Consider some n, m, and p in Nats.",
"intros n m p",
"-- Perform induction on n.",
"induction n with",
"| zero =>",
"-- Base case: When n = 0, we need to show 0 + (m + p) = (0 + m) + p.",
"-- Using the definition of addition, 0 + (m + p) = m + p and (0 + m) + p = m + p.",
"rw [Nat.zero_add, Nat.zero_add]",
"| succ n ih =>",
"-- Inductive step: Assume n + (m + p) = (n + m) + p, we need to show succ n + (m + p) = (succ n + m) + p.",
"-- proof strategy is, we move succ n out (or in) enough times then use the IH until both sides are the same.",
"-- 1. let's start by pulling out the succ from the left side and have the entire addition inside the succ.",
"have h_pull_add_succ_out_from_left: Nat.succ n + (m + p) = Nat.succ (n + (m + p)) := by rw [Nat.succ_add]",
"-- 2. Now that we have the IH hypothesis appearing inside the left, let's apply it so we have n + (m + p) = (n + m) + p.",
"have h_inside_left_associates: Nat.succ (n + (m + p)) = Nat.succ ((n + m) + p) := by aesop",
"-- 3. Now that the parentheses (apps of plus) are in the right place for both sides, push the succ on the left twice so both terms are the same.",
"have h_push_succ_in_left_twice: Nat.succ ((n + m) + p) = ((Nat.succ n) + m) + p := by rw [← Nat.succ_add, ← Nat.succ_add]",
"-- Combining these, we get succ n + (m + p) = (succ n + m) + p.",
"rw [h_pull_add_succ_out_from_left, h_inside_left_associates, h_push_succ_in_left_twice]"
],
"src_header_fl_solution": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
]
}
]

98
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_test.json Normal file
View File

@ -0,0 +1,98 @@
[
{
"nl_problem": ["Prove that for any natural number n, 0 + n = n."],
"nl_solution": [
"Consider any natural number n. We will prove the statement by induction on n.",
"Base case: When n = 0, we need to show that 0 + 0 = 0. This is true by the definition of addition.",
"Inductive step: Assume that for some natural number n, 0 + n = n. We need to show that 0 + (n + 1) = (n + 1). By the definition of addition and the inductive hypothesis, we have 0 + (n + 1) = (0 + n) + 1 = n + 1. Therefore, the statement holds for n + 1.",
"Thus, by induction, we have proved that for any natural number n, 0 + n = n."
],
"nl_solution_sketch": [
"Consider any natural number n, and do induction on n.",
"Base case: 0 + 0 = 0 by properties of addition.",
"Inductive step we have 0 + n = n. Then 0 + (n + 1) = (0 + n) + 1 = n + 1.",
"Where, 0 + n = n by assumption,qed."
],
"fl_problem": ["theorem zero_plus_n_proved_formal_sketch : ∀ n : ℕ, 0 + n = n := "],
"fl_partial_sketch": [
"by\n",
" -- Consider some n in Nats.\n",
" intro n\n",
" -- Perform induction on n.\n",
" induction n with\n",
" | zero =>\n",
" -- Base case: 0 + 0 = 0\n",
" have h_base: 0 + 0 = 0 := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n",
" | succ n ih =>\n",
" -- Inductive step: assume 0 + n = n, prove 0 + succ n = succ n\n",
" have h_inductive: 0 + Nat.succ n = Nat.succ n := <TODO_PROOF_OR_HAMMER>\\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "1"
},
{
"nl_problem": ["Prove that for any natural number n, m, and p, n + (m + p) = (n + m) + p."],
"nl_solution": [
"Consider any natural numbers n, m, and p. We will prove the statement by induction on n.",
"Base case: When n = 0, we need to show that 0 + (m + p) = (0 + m) + p. By the definition of addition, we have 0 + (m + p) = m + p and (0 + m) + p = m + p. Therefore, 0 + (m + p) = (0 + m) + p.",
"Inductive step: Assume that for some natural number n, n + (m + p) = (n + m) + p. We need to show that (n + 1) + (m + p) = ((n + 1) + m) + p.",
"1. First, pull out the successor from the left side to have the entire addition inside the successor: (n + 1) + (m + p) = (n + (m + p)) + 1.",
"2. By the inductive hypothesis, we know that n + (m + p) = (n + m) + p. So we can replace n + (m + p) with (n + m) + p inside the successor: (n + (m + p)) + 1 = ((n + m) + p) + 1.",
"3. Finally, push the successor on the left twice to align both sides: ((n + m) + p) + 1 = (n + 1) + (m + p) = ((n + 1) + m) + p.",
"Thus, by induction, we have proved that for any natural numbers n, m, and p, n + (m + p) = (n + m) + p."
],
"nl_solution_sketch": [
"Consider any natural numbers n, m, and p. We will do induction on n.",
"Base case: 0 + (m + p) = (0 + m) + p by properties of addition.",
"Inductive step, we have n + (m + p) = (n + m) + p. Then (n + 1) + (m + p) = (n + (m + p)) + 1 = ((n + m) + p) + 1.",
"Thus, (n + 1) + (m + p) = ((n + 1) + m) + p, qed."
],
"fl_problem": ["theorem add_assoc_proved_formal_sketch : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := "],
"fl_partial_sketch": [
"by\n",
" -- Consider some n, m, and p in Nats.\n",
" intros n m p\n",
" -- Perform induction on n.\n",
" induction n with\n",
" | zero =>\n",
" -- Base case: When n = 0, we need to show 0 + (m + p) = (0 + m) + p.\n",
" -- We have the fact 0 + (m + p) = m + p by the definition of addition.\n",
" have h_base: 0 + (m + p) = m + p := <TODO_PROOF_OR_HAMMER>\n",
" -- We also have the fact (0 + m) + p = m + p by the definition of addition.\n",
" have h_symm: (0 + m) + p = m + p := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n",
" | succ n ih =>\n",
" -- Inductive step: Assume n + (m + p) = (n + m) + p, we need to show succ n + (m + p) = (succ n + m) + p.\n",
" -- By the inductive hypothesis, we have n + (m + p) = (n + m) + p.\n",
" have h_inductive: n + (m + p) = (n + m) + p := <TODO_PROOF_OR_HAMMER>\n",
" -- 1. Let's start by pulling out the succ from left side and have the entire addition inside the succ.\n",
" have h_pull_succ_out_from_left: Nat.succ n + (m + p) = Nat.succ (n + (m + p)) := <TODO_PROOF_OR_HAMMER>\n",
" -- 2. Now that we have the IH hypothesis appearing inside the left, let's apply it so we have n + (m + p) = (n + m) + p.\n",
" have h_inside_left_associates: Nat.succ (n + (m + p)) = Nat.succ ((n + m) + p) := <TODO_PROOF_OR_HAMMER>\n",
" -- 3. Now that the parentheses (apps of plus) are in the right place for both sides, push the succ on the left twice so both terms are the same.\n",
" have h_push_succ_in_left_twice: Nat.succ ((n + m) + p) = ((Nat.succ n) + m) + p := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "4"
}
]

117
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json Normal file
View File

@ -0,0 +1,117 @@
[
{
"nl_problem": ["Prove that for any natural number n, n + 0 = n."],
"nl_solution": [
"Consider any natural number n.",
"Using the properties of addition, we know that adding zero to any number does not change the value of that number.",
"Therefore, we can conclude that n + 0 = n."
],
"nl_solution_sketch": [
"Consider any natural number n.",
"From properties of addition, adding zero does not change its values.",
"Thus, n + 0 = n."
],
"fl_problem": ["theorem n_plus_zero_normal : ∀ n : ℕ, n + 0 = n := "],
"fl_partial_sketch": [
"by\n",
" -- We have the fact of addition n + 0 = n, use it to show left and right are equal.\n",
" have h_nat_add_zero: ∀ n : ℕ, n + 0 = n := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts with to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "0"
},
{
"nl_problem": ["Prove that for any natural number n, n + (m + 1) = (n + m) + 1."],
"nl_solution": [
"Consider any natural numbers n and m. We want to show that n + (m + 1) = (n + m) + 1.",
"Using the properties of addition, we know that adding 1 to the sum of n and m is the same as first adding m to n and then adding 1.",
"Therefore, we can conclude that n + (m + 1) = (n + m) + 1."
],
"nl_solution_sketch": [
"Consider any natural numbers n and m.",
"From properties of addition, adding 1 to the sum of n and m is the same as first adding m to n and then adding 1.",
"Thus, n + (m + 1) = (n + m) + 1."
],
"fl_problem": ["theorem plus_n_Sm_proved_formal_sketch : ∀ n m : ℕ, n + (m + 1) = (n + m) + 1 := "],
"fl_partial_sketch": [
"by\n",
" -- We have the fact of addition n + (m + 1) = (n + m) + 1, use it to show left and right are equal.\n",
" have h_nat_add_succ: ∀ n m : ℕ, n + (m + 1) = (n + m) + 1 := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "2"
},
{
"nl_problem": ["Prove that for any natural number n and m, n + m = m + n."],
"nl_solution": [
"Consider any natural numbers n and m. We will prove the statement by induction on n.",
"Base case: When n = 0, we need to show that 0 + m = m + 0. By the definition of addition, we have 0 + m = m and m + 0 = m. Therefore, 0 + m = m + 0.",
"Inductive step: Assume that for some natural number n, n + m = m + n. We need to show that (n + 1) + m = m + (n + 1).",
"1. Start by using the fact that (n + 1) + m = n + (m + 1) and m + (n + 1) = (m + n) + 1.",
"2. By the inductive hypothesis, we have n + m = m + n. So we can replace n + (m + 1) with (m + n) + 1.",
"3. Now, both sides have the same structure, showing that (n + 1) + m = m + (n + 1).",
"Thus, by induction, we have proved that for any natural numbers n and m, n + m = m + n."
],
"nl_solution_sketch": [
"Consider any natural numbers n and m. We will do induction on n.",
"Base case: 0 + m = m + 0 by properties of addition.",
"Inductive step, we have n + m = m + n. Then (n + 1) + m = (n + m) + 1 = (m + n) + 1 = m + (n + 1).",
"Thus, by induction, n + m = m + n, qed."
],
"fl_problem": ["theorem add_comm_proved_formal_sketch : ∀ n m : ℕ, n + m = m + n := "],
"fl_partial_sketch": [
"by\n",
" -- Consider some n and m in Nats.\n",
" intros n m\n",
" -- Perform induction on n.\n",
" induction n with\n",
" | zero =>\n",
" -- Base case: When n = 0, we need to show 0 + m = m + 0.\n",
" -- We have the fact 0 + m = m by the definition of addition.\n",
" have h_base: 0 + m = m := <TODO_PROOF_OR_HAMMER>\n",
" -- We also have the fact m + 0 = m by the definition of addition.\n",
" have h_symm: m + 0 = m := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n",
" | succ n ih =>\n",
" -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n",
" -- By the inductive hypothesis, we have n + m = m + n.\n",
" have h_inductive: n + m = m + n := <TODO_PROOF_OR_HAMMER>\n",
" -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.\n",
" have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := <TODO_PROOF_OR_HAMMER>\n",
" -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n",
" have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := <TODO_PROOF_OR_HAMMER>\n",
" -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.\n",
" have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "3"
}
]

106
examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/readme.md Normal file
View File

@ -0,0 +1,106 @@
https://www.evernote.com/shard/s410/nl/75276202/2170cbbd-24a1-2d25-da32-bd8f3270d190?title=prompt%20for%20creating%20toy%20example
https://chatgpt.com/c/0ad32608-cbc9-4627-a705-786ed7421826
I want all final responses in this format:
```json
{
"nl_problem": ["Prove that for any natural number n, n + 0 = n."],
"nl_solution": [
"Consider any natural number n.",
"Using the properties of addition, we know that adding zero to any number does not change the value of that number.",
"Therefore, we can conclude that n + 0 = n."
],
"nl_solution_sketch": [
"Consider any natural number n.",
"From properties of addition, adding zero does not change its values.",
"Thus, n + 0 = n."
],
"fl_problem": ["theorem n_plus_zero_normal : ∀ n : ℕ, n + 0 = n :="],
"fl_partial_sketch": [
"-- Prove that n + 0 = n via a formal proof sketch with holes to be filled\n",
"theorem n_plus_zero_proved_formal_sketch'' : ∀ n : ℕ, n + 0 = n := by\n",
" -- We have the fact of addition n + 0 = n, use it to show left and right are equal.\n",
" have h_nat_add_zero: ∀ n : ℕ, n + 0 = n := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts with to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
],
"path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
"fl_statement_idx": "0"
},
{
"nl_problem": ["Prove that for any natural number n, 0 + n = n."],
"nl_solution": [
"Consider any natural number n. We will prove the statement by induction on n.",
"Base case: When n = 0, we need to show that 0 + 0 = 0. This is true by the definition of addition.",
"Inductive step: Assume that for some natural number n, 0 + n = n. We need to show that 0 + (n + 1) = (n + 1). By the definition of addition and the inductive hypothesis, we have 0 + (n + 1) = (0 + n) + 1 = n + 1. Therefore, the statement holds for n + 1.",
"Thus, by induction, we have proved that for any natural number n, 0 + n = n."
],
"nl_solution_sketch": [
"Consider any natural number n, and do induction on n.",
"Base case: 0 + 0 = 0 by properties of addition.",
"Inductive step we have 0 + n = n. Then 0 + (n + 1) = (0 + n) + 1 = n + 1.",
"Where, 0 + n = n by assumption,qed."
],
"fl_problem": ["theorem zero_plus_n_proved_formal_sketch : ∀ n : ℕ, 0 + n = n :="],
"fl_partial_sketch": [
"-- Prove that 0 + n = n by induction via a formal proof sketch with holes to be filled\n",
"theorem zero_plus_n_proved_formal_sketch'' : ∀ n : ℕ, 0 + n = n := by\n",
" -- Consider some n in Nats.\n",
" intro n\n",
" -- Perform induction on n.\n",
" induction n with\n",
" | zero =>\n",
" -- Base case: 0 + 0 = 0\n",
" have h_base: 0 + 0 = 0 := <TODO_PROOF_OR_HAMMER>\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n",
" | succ n ih =>\n",
" -- Inductive step: assume 0 + n = n, prove 0 + succ n = succ n\n",
" have h_inductive: 0 + Nat.succ n = Nat.succ n := <TODO_PROOF_OR_HAMMER>\\n",
" -- Combine facts to close goal\n",
" <TODO_PROOF_OR_HAMMER>\n"
],
"src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"],
"fl_header_sketch": [
"import Mathlib.Data.Nat.Basic",
"import Aesop"
]
}
```
I want to translate the following formal proof (solution) in lean 4 to a natural language proof (solution) that a human would write (without lean code in it) and eventually make it into a concise nl_solution_sketch, like the following one:
```human_problem_solution_proof.json
"nl_problem": ["Let \\[f(x) = \\left\\{\n\\begin{array}{cl} ax+3, &\\text{ if }x>2, \\\\\nx-5 &\\text{ if } -2 \\le x \\le 2, \\\\\n2x-b &\\text{ if } x <-2.\n\\end{array}\n\\right.\\]Find $a+b$ if the piecewise function is continuous (which means that its graph can be drawn without lifting your pencil from the paper)."],
"nl_solution_sketch": ["For the piecewise function to be continuous, the cases must \"meet\" at $2$ and $-2$. For example, $ax+3$ and $x-5$ must be equal when $x=2$. This implies $a(2)+3=2-5$, which we solve to get $2a=-6 \\Rightarrow a=-3$. Similarly, $x-5$ and $2x-b$ must be equal when $x=-2$. Substituting, we get $-2-5=2(-2)-b$, which implies $b=3$. So $a+b=-3+3=\\boxed{0}$."]
```
This is my lean 4 fl theorem (fl problem) and fl proof (fl solution):
```
-- Prove that n + (m + p) = (n + m) + p
theorem add_assoc_proved_formal_sketch : ∀ n m p : ℕ, n + (m + p) = (n + m) + p := by
-- Consider some n, m, and p in Nats.
intros n m p
-- Perform induction on n.
induction n with
| zero =>
-- Base case: When n = 0, we need to show 0 + (m + p) = (0 + m) + p.
-- Using the definition of addition, 0 + (m + p) = m + p and (0 + m) + p = m + p.
simp [Nat.zero_add, Nat.zero_add]
| succ n ih =>
-- Inductive step: Assume n + (m + p) = (n + m) + p, we need to show succ n + (m + p) = (succ n + m) + p.
-- proof strategy is, we move succ n out (or in) enough times then use the IH until both sides are the same.
-- 1. let's start by pulling out the scc from left side and have the entire addition inside the succ.
have h_pull_add_succ_out_from_left: Nat.succ n + (m + p) = Nat.succ (n + (m + p)) := by simp [Nat.succ_add]
-- 2. Now that we have the IH hypothesis appearing inside the left, let's apply it so we have n + (m + p) = (n + m) + p.
have h_inside_left_associates: Nat.succ (n + (m + p)) = Nat.succ ((n + m) + p) := by simp [ih]
-- 3. Now that the parenthesis (apps of plus) are on the right place for both side, push the succ on the left twice so both terms are the same.
have h_push_succ_in_left_twice: Nat.succ ((n + m) + p) = ((Nat.succ n) + m) + p := by simp [Nat.succ_add, Nat.succ_add]
-- Combining these, we get succ n + (m + p) = (succ n + m) + p.
simp [h_pull_add_succ_out_from_left, h_inside_left_associates, h_push_succ_in_left_twice]
```
use the comments to translate the fl proof (solution) to natural language solution then use that to output a natural language concise sketch. Make the natural language proof (solution) sketch concise with the core elements of the solution proof. Do this by first outputting the natural language solution, distill it into a very concise proof sketch in natural language with only the core components. Output everything in a json code block please:

102
examples/lean4_dsp/dsp_for_lean4.py
View File

@ -1,18 +1,20 @@
"""
DSP (Draft Sketch Prove) for Lean 4
"""
import sys
from collections import namedtuple
import fire
from pathlib import Path
from tqdm import tqdm
from typing import Union, Any
import json
import os
from openai import OpenAI
import wandb
from tenacity import retry, stop_after_attempt, wait_exponential
from solve.dsp_lean_prompts import SYSTEM_PROMPT_DRAFT_V0, prompt_draft_template_lean4_v0, STOP_TOKENS_DRAFT_V0
from solve.dsp_lean_prompts import SYSTEM_PROMPT_SKETCH_V0, prompt_sketch_template_lean4_v0, STOP_TOKENS_SKETCH_V0
# prompt_draft_template_lean4_v0 = "Draft an informal solution similar to the one below. The informal solution will be used to sketch a formal proof in the Lean 4 Proof Assistant. Here are some examples of informal problem solutions pairs:\n\nInformal:\n(*### Problem\n\nProve that for any natural number n, n + 0 = n.\n\n### Solution\n\nConsider any natural number n. From properties of addition, adding zero does not change its values. Thus, n + 0 = n.*)\n\nInformal:\n(*### Problem\n\nProve that for any natural number n, n + (m + 1) = (n + m) + 1.\n\n### Solution\n\nConsider any natural numbers n and m. From properties of addition, adding 1 to the sum of n and m is the same as first adding m to n and then adding 1. Thus, n + (m + 1) = (n + m) + 1.*)\n\nInformal:\n(*### Problem\n\nProve that for any natural number n and m, n + m = m + n.\n\n### Solution\n\nConsider any natural numbers n and m. We will do induction on n. Base case: 0 + m = m + 0 by properties of addition. Inductive step, we have n + m = m + n. Then (n + 1) + m = (n + m) + 1 = (m + n) + 1 = m + (n + 1). Thus, by induction, n + m = m + n, qed.*)\n\nInformal: \n(*### Problem\n\n{nl_problem}\n\n### Solution\n"
class Engine:
def __init__(self):
pass
@ -29,12 +31,12 @@ class OpenAI_DSP_Engine(Engine):
# Draft Params
draft_system_prompt: str = SYSTEM_PROMPT_DRAFT_V0, # 'You are an expert mathematician and an expert in the Lean 4 Proof Assistant.' (goal do draft)
draft_prompt_template: str = prompt_draft_template_lean4_v0,
draft_sampling_params: SamplingParams = SamplingParams(n=1, max_tokens=2048, top_p=0.95, temperature=0.8),
draft_sampling_params = None,
draft_stop_tokens: list[str] = STOP_TOKENS_DRAFT_V0,
# Sketch Params
sketch_system_prompt: str = SYSTEM_PROMPT_SKETCH_V0,
sketch_prompt_template: str = prompt_sketch_template_lean4_v0,
sketch_sampling_params: SamplingParams = SamplingParams(n=1, max_tokens=2048, top_p=0.95, temperature=0.8, stop=STOP_TOKENS_DSP_V0),
sketch_sampling_params = None,
sketch_stop_tokens: list[str] = STOP_TOKENS_SKETCH_V0,
# Prove Params
# ...TODO not sure if needed right now...
@ -50,12 +52,12 @@ class OpenAI_DSP_Engine(Engine):
self.draft_system_prompt = draft_system_prompt
self.draft_prompt_template = draft_prompt_template
self.draft_sampling_params = draft_sampling_params
self.draft_sampling_params.stop = draft_stop_tokens
# self.draft_sampling_params.stop = draft_stop_tokens
# Sketch params
self.sketch_system_prompt = sketch_system_prompt
self.sketch_prompt_template = sketch_prompt_template
self.sketch_sampling_params = sketch_sampling_params
self.sketch_sampling_params.stop = sketch_stop_tokens
# self.sketch_sampling_params.stop = sketch_stop_tokens
# Prove params
# ...TODO not sure if needed right now...
@ -79,7 +81,7 @@ def draft(
y_pred_nl ~ draft(eng, x_nl_prob, P_draft)
"""
# Make prompt from template
nl_problem: str = data_pt['nl_problem']
nl_problem: str = data_pt['nl_problem'][0]
prompt = eng.draft_prompt_template.replace('{nl_problem}', nl_problem)
# Get all **completions** to single prompt, one (in) -> many (out)
# ref: https://platform.openai.com/docs/api-reference/chat/object
@ -113,15 +115,15 @@ def sketch(
"""
assert len(drafts) == 1, f"For now only 1 draft."
# Make prompt from template
x_nl_problem: str = data_pt['nl_problem']
x_nl_problem: str = data_pt['nl_problem'][0]
y_nl_solution: str = drafts[0]
if autoformalize_prob_in_prompt:
prompt = eng.sketch_prompt_template.replace('{nl_problem}', x_nl_problem).replace('{nl_solution}', y_nl_solution)
# prompt = eng.sketch_prompt_template.replace('{nl_problem}', x_nl_problem).replace('{nl_solution}', y_nl_solution)
not NotImplemented
else:
x_fl_problem = data_pt['fl_problem'] if 'fl_problem' in data_pt else autoformalize_prob(eng, data_pt)
prompt = eng.sketch_prompt_template.replace('{nl_problem}', x_nl_problem).replace('{nl_solution}', y_nl_solution)
# Get all **completions** to single prompt, one (in) -> many (out)
# ref: https://platform.openai.com/docs/api-reference/chat/object
x_fl_problem = data_pt['fl_problem'][0] if 'fl_problem' in data_pt else autoformalize_prob(eng, data_pt)
prompt = eng.sketch_prompt_template.replace('{fl_problem}', x_nl_problem).replace('{fl_problem}', y_nl_solution)
# Get all **completions** to single prompt, one (in) -> many (out), ref: https://platform.openai.com/docs/api-reference/chat/object
response: Any = eng.llm.chat.completions.create(
model=eng.model,
messages=[
@ -131,7 +133,7 @@ def sketch(
temperature=eng.sketch_sampling_params.temperature,
top_p=eng.sketch_sampling_params.top_p,
n=eng.sketch_sampling_params.n,
stop=eng.sketch_sampling_params.stop[:3],
# stop=eng.sketch_sampling_params.stop[:3],
)
# Get all completions for single prompt
completions: list[str] = [completion.message.content for completion in response.choices] # response.choices[i].message
@ -144,12 +146,14 @@ def prove(
fl_prob: str,
fl_sketch: list[str],
):
""" Complete formal sketch and check if it proves the theorem. """
from pantograph.server import Server
server = Server()
state0 = server.goal_start(fl_prob)
print(f'{state0=}')
print()
"""
Complete formal sketch and check if it proves the theorem.
fl_prob --> Lean4 theorem (problem)
fl_sketch --> Lean4 Form Sketch --> have x have ha
"""
# -- Prove
correct: bool = False
# -- Return
@ -158,8 +162,8 @@ def prove(
# -- DSP for Lean
def single_proof_search_dsp_lean(
eng: Engine,
data_pt: dict,
eng: Engine,
data_pt: dict,
) -> bool:
# -- Draft: [y_nl_pred_draft]_n ~ draft(eng, x_nl_prob, P_draft)
y_nl_pred_drafts = draft(eng, data_pt)
@ -184,26 +188,24 @@ def full_proof_search_dsp_lean(
print(f'{len(eval_dataset)=}')
# -- Proof search by DSP over all eval data
data_pt: dict
for data_pt in tqdm(eval_dataset, total=len(eval_dataset)):
# -- DSP
for data_pt in tqdm(eval_dataset, total=len(eval_dataset), desc='DSP proof loop per data point in benchmark.'):
print(f'{data_pt=}')
single_proof_search_dsp_lean(eng, data_pt)
# -- Return
return
# -- Main
def main(
path_2_eval_dataset: str = '~/gold-ai-olympiad/data/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json',
# model: str = 'mistralai/Mistral-7B-Instruct-v0.1',
path_2_eval_dataset: str = '~/PyPantograph/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json',
# model: str = 'deepseek-ai/deepseek-math-7b-instruct',
# model: str = 'gpt2',
model: str = 'gpt-3.5-turbo',
# model: str = 'gpt-4-turbo',
# model: str = 'gpt-3.5-turbo',
model: str = 'gpt-4o',
start: int = 0,
end: int = sys.maxsize,
# end: int = 10, # do 10 so enough boxed qs are there
batch_size: int = 10, # putnam has 348
n: int = 4, # num seqs to return for given prompt
n: int = 1, # num seqs to return for given prompt
max_tokens: int = 2048,
top_p: float = 0.95,
temperature: float = 0.8,
@ -213,37 +215,35 @@ def main(
print(f'{path_2_eval_dataset=}')
# - Start wandb run
print(f'\n\n-- Setup params')
CUDA_VISIBLE_DEVICES = os.environ.get("CUDA_VISIBLE_DEVICES")
current_tmux_session = os.environ.get("TMUX", "").split(",")[-1]
today = datetime.datetime.now().strftime("%Y-m%m-d%d-t%Hh_%Mm_%Ss")
config = {'today': today, "CUDA_VISIBLE_DEVICES": CUDA_VISIBLE_DEVICES, "current_tmux_session": current_tmux_session, "model": model, "path_2_eval_dataset": path_2_eval_dataset}
project: str = 'pypantograph'
run_name = f"{project}: ({config})"
run = wandb.init(mode=mode, project=project, name=run_name, save_code=True, config=config)
print(f"{run.url=}")
print(f'\n Config: \n{config=}')
# print(f'\n\n-- Setup params')
# CUDA_VISIBLE_DEVICES = os.environ.get("CUDA_VISIBLE_DEVICES")
# current_tmux_session = os.environ.get("TMUX", "").split(",")[-1]
# today = datetime.datetime.now().strftime("%Y-m%m-d%d-t%Hh_%Mm_%Ss")
# config = {'today': today, "CUDA_VISIBLE_DEVICES": CUDA_VISIBLE_DEVICES, "current_tmux_session": current_tmux_session, "model": model, "path_2_eval_dataset": path_2_eval_dataset}
# project: str = 'pypantograph'
# run_name = f"{project}: ({config})"
# run = wandb.init(mode=mode, project=project, name=run_name, save_code=True, config=config)
# print(f"{run.url=}")
# print(f'\n Config: \n{config=}')
# - Run DSP for Lean
print(f'\n\n-- Run DSP for Lean')
# stop: list[str] = STOP_TOKENS
dtype: str = get_dtype_for_vllm()
print(f'{dtype=}')
sampling_params: SamplingParams = SamplingParams(n=n, max_tokens=max_tokens, top_p=top_p, temperature=temperature, stop=stop)
if 'gpt-4-' in model or 'gpt-3.5-' in model or 'gpt-4o' in model:
# # api_key = open(Path('~/keys/openai_api_brandos_personal_key.txt').expanduser(), 'r').read().strip()
api_key = open(Path('~/keys/openai_api_key_brandos_koyejolab.txt').expanduser(), 'r').read().strip()
eng: OpenAI_DSP_Engine = OpenAI_DSP_Engine(model=model, api_key=api_key, verbose_init=True)
SamplingParams = namedtuple('SamplingParams', ['n', 'max_tokens', 'top_p', 'temperature', 'stop'])
draft_sampling_params = SamplingParams(n=n, max_tokens=max_tokens, top_p=top_p, temperature=temperature, stop=STOP_TOKENS_DRAFT_V0)
sketch_sampling_params = SamplingParams(n=n, max_tokens=max_tokens, top_p=top_p, temperature=temperature, stop=STOP_TOKENS_SKETCH_V0)
eng: OpenAI_DSP_Engine = OpenAI_DSP_Engine(model=model, api_key=api_key, verbose_init=True, draft_sampling_params=draft_sampling_params, sketch_sampling_params=sketch_sampling_params)
else:
raise ValueError(f"Model {model=} not supported.")
# - Full proof search with DSP
print(f'\n\n-- Full proof search with DSP')
full_proof_search_dsp_lean(eng, path_2_eval_dataset)
# - End run
wandb.config.update(config)
print(f"{wandb.config=}")
run.finish()
# wandb.config.update(config)
# print(f"{wandb.config=}")
# run.finish()
if __name__ == "__main__":
import time

255
examples/lean4_dsp/solve/dsp_for_lean4.py Normal file
View File

@ -0,0 +1,255 @@
"""
DSP (Draft Sketch Prove) for Lean 4
"""
import fire
from pathlib import Path
from tqdm import tqdm
from typing import Union, Any
import json
import os
import wandb
from tenacity import retry, stop_after_attempt, wait_exponential
from solve.dsp_lean_prompts import SYSTEM_PROMPT_DRAFT_V0, prompt_draft_template_lean4_v0, STOP_TOKENS_DRAFT_V0
from solve.dsp_lean_prompts import SYSTEM_PROMPT_SKETCH_V0, prompt_sketch_template_lean4_v0, STOP_TOKENS_SKETCH_V0
class Engine:
def __init__(self):
pass
def __call__(self, *args, **kwards):
pass
class OpenAI_DSP_Engine(Engine):
def __init__(
self,
model: str,
api_key: str = None,
base_url: str = None, # e.g., Mistral-7B-Instrcut-v0.2 on http://120.77.8.29:12345
# Draft Params
draft_system_prompt: str = SYSTEM_PROMPT_DRAFT_V0, # 'You are an expert mathematician and an expert in the Lean 4 Proof Assistant.' (goal do draft)
draft_prompt_template: str = prompt_draft_template_lean4_v0,
draft_sampling_params: SamplingParams = SamplingParams(n=1, max_tokens=2048, top_p=0.95, temperature=0.8),
draft_stop_tokens: list[str] = STOP_TOKENS_DRAFT_V0,
# Sketch Params
sketch_system_prompt: str = SYSTEM_PROMPT_SKETCH_V0,
sketch_prompt_template: str = prompt_sketch_template_lean4_v0,
sketch_sampling_params: SamplingParams = SamplingParams(n=1, max_tokens=2048, top_p=0.95, temperature=0.8, stop=STOP_TOKENS_DSP_V0),
sketch_stop_tokens: list[str] = STOP_TOKENS_SKETCH_V0,
# Prove Params
# ...TODO not sure if needed right now...
# Misc
verbose_init: bool = True,
):
super().__init__()
print(f'{api_key=}, {base_url=}') if verbose_init else None
self.model = model
self.api_key = api_key
self.llm = OpenAI(api_key=self.api_key, base_url=base_url)
# Draft params
self.draft_system_prompt = draft_system_prompt
self.draft_prompt_template = draft_prompt_template
self.draft_sampling_params = draft_sampling_params
self.draft_sampling_params.stop = draft_stop_tokens
# Sketch params
self.sketch_system_prompt = sketch_system_prompt
self.sketch_prompt_template = sketch_prompt_template
self.sketch_sampling_params = sketch_sampling_params
self.sketch_sampling_params.stop = sketch_stop_tokens
# Prove params
# ...TODO not sure if needed right now...
@retry(stop=stop_after_attempt(15), wait=wait_exponential(multiplier=2, max=128))
def autoformalize_prob(
eng,
data_pt: dict,
verbose: bool = False,
):
""" Autoformalize natural language problem to formal language problem. """
...
@retry(stop=stop_after_attempt(15), wait=wait_exponential(multiplier=2, max=128))
def draft(
eng,
data_pt: dict,
verbose: bool = False,
) -> list:
"""
Creates (informal nl) draft (nl soln, nl proof sketch) for latter use in a formal proof sketch.
y_pred_nl ~ draft(eng, x_nl_prob, P_draft)
"""
# Make prompt from template
nl_problem: str = data_pt['nl_problem']
prompt = eng.draft_prompt_template.replace('{nl_problem}', nl_problem)
# Get all **completions** to single prompt, one (in) -> many (out)
# ref: https://platform.openai.com/docs/api-reference/chat/object
response: Any = eng.llm.chat.completions.create(
model=eng.model,
messages=[
{"role": "system", "content": eng.draft_system_prompt},
{"role": "user", "content": prompt},
],
temperature=eng.draft_sampling_params.temperature,
top_p=eng.draft_sampling_params.top_p,
n=eng.draft_sampling_params.n,
stop=eng.draft_sampling_params.stop[:3],
)
# Get all completions for single prompt
completions: list[str] = [completion.message.content for completion in response.choices] # response.choices[i].message
drafts: list[str] = completions
return drafts
@retry(stop=stop_after_attempt(15), wait=wait_exponential(multiplier=2, max=128))
def sketch(
eng,
data_pt: dict,
drafts: list,
autoformalize_prob_in_prompt: bool = False,
verbose: bool = False,
) -> list:
"""
Creates (formal fl) sketch (fl proof sketch) for latter use in a formal proof sketch.
z_pred_fl ~ sketch(eng, x_nl_prob, y_pred_nl, x_fl_prob, P_sketch)
"""
assert len(drafts) == 1, f"For now only 1 draft."
# Make prompt from template
x_nl_problem: str = data_pt['nl_problem']
y_nl_solution: str = drafts[0]
if autoformalize_prob_in_prompt:
prompt = eng.sketch_prompt_template.replace('{nl_problem}', x_nl_problem).replace('{nl_solution}', y_nl_solution)
else:
x_fl_problem = data_pt['fl_problem'] if 'fl_problem' in data_pt else autoformalize_prob(eng, data_pt)
prompt = eng.sketch_prompt_template.replace('{nl_problem}', x_nl_problem).replace('{nl_solution}', y_nl_solution)
# Get all **completions** to single prompt, one (in) -> many (out)
# ref: https://platform.openai.com/docs/api-reference/chat/object
response: Any = eng.llm.chat.completions.create(
model=eng.model,
messages=[
{"role": "system", "content": eng.sketch_system_prompt},
{"role": "user", "content": prompt},
],
temperature=eng.sketch_sampling_params.temperature,
top_p=eng.sketch_sampling_params.top_p,
n=eng.sketch_sampling_params.n,
stop=eng.sketch_sampling_params.stop[:3],
)
# Get all completions for single prompt
completions: list[str] = [completion.message.content for completion in response.choices] # response.choices[i].message
sketches: list[str] = completions
# Return
return sketches, x_fl_problem
def prove(
eng,
fl_prob: str,
fl_sketch: list[str],
):
""" Complete formal sketch and check if it proves the theorem. """
from pantograph.server import Server
server = Server()
state0 = server.goal_start(fl_prob)
print(f'{state0=}')
print()
# -- Prove
correct: bool = False
# -- Return
return correct
# -- DSP for Lean
def single_proof_search_dsp_lean(
eng: Engine,
data_pt: dict,
) -> bool:
# -- Draft: [y_nl_pred_draft]_n ~ draft(eng, x_nl_prob, P_draft)
y_nl_pred_drafts = draft(eng, data_pt)
# -- Sketch: z_fl_pred_sketch ~ sketch(eng, x_nl_prob, [y_nl_pred_draft]_n, x_fl_prob, P_sketch)
z_fl_pred_sketches, x_fl_prob = sketch(eng, data_pt, y_nl_pred_drafts)
# -- Prove: y_fl = prove(eng, x_fl_prob, z_fl_pred_sketches)
correct: bool = prove(eng, x_fl_prob, z_fl_pred_sketches)
# -- Return
return
def full_proof_search_dsp_lean(
eng: Engine,
path_2_eval_dataset: Union[str, Path],
):
# -- Get eval data
path_2_eval_dataset = Path(path_2_eval_dataset).expanduser()
eval_dataset: list[dict] = json.load(open(path_2_eval_dataset, 'r'))
print(f'{len(eval_dataset)=}')
# -- Proof search by DSP over all eval data
data_pt: dict
for data_pt in tqdm(eval_dataset, total=len(eval_dataset)):
# -- DSP
single_proof_search_dsp_lean(eng, data_pt)
# -- Return
return
# -- Main
def main(
path_2_eval_dataset: str = '~/gold-ai-olympiad/data/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json',
# model: str = 'mistralai/Mistral-7B-Instruct-v0.1',
# model: str = 'deepseek-ai/deepseek-math-7b-instruct',
# model: str = 'gpt2',
model: str = 'gpt-3.5-turbo',
# model: str = 'gpt-4-turbo',
start: int = 0,
end: int = sys.maxsize,
# end: int = 10, # do 10 so enough boxed qs are there
batch_size: int = 10, # putnam has 348
n: int = 4, # num seqs to return for given prompt
max_tokens: int = 2048,
top_p: float = 0.95,
temperature: float = 0.8,
mode: str = "dryrun",
# mode: str = "online",
):
path_2_eval_dataset = Path(path_2_eval_dataset).expanduser()
print(f'{path_2_eval_dataset=}')
# - Start wandb run
print(f'\n\n-- Setup params')
# num_workers = min(144, cpu_count())
# print(f'{num_workers=} {cpu_count()=}')
CUDA_VISIBLE_DEVICES = os.environ.get("CUDA_VISIBLE_DEVICES")
current_tmux_session = os.environ.get("TMUX", "").split(",")[-1]
today = datetime.datetime.now().strftime("%Y-m%m-d%d-t%Hh_%Mm_%Ss")
config = {'today': today, "CUDA_VISIBLE_DEVICES": CUDA_VISIBLE_DEVICES, "current_tmux_session": current_tmux_session, "model": model, "path_2_eval_dataset": path_2_eval_dataset}
project: str = 'pypantograph'
run_name = f"{project}: ({config})"
run = wandb.init(mode=mode, project=project, name=run_name, save_code=True, config=config)
print(f"{run.url=}")
print(f'\n Config: \n{config=}')
# - Run DSP for Lean
print(f'\n\n-- Run DSP for Lean')
# stop: list[str] = STOP_TOKENS
dtype: str = get_dtype_for_vllm()
print(f'{dtype=}')
sampling_params: SamplingParams = SamplingParams(n=n, max_tokens=max_tokens, top_p=top_p, temperature=temperature, stop=stop)
if 'gpt-4-' in model or 'gpt-3.5-' in model or 'gpt-4o' in model:
# # api_key = open(Path('~/keys/openai_api_brandos_personal_key.txt').expanduser(), 'r').read().strip()
api_key = open(Path('~/keys/openai_api_key_brandos_koyejolab.txt').expanduser(), 'r').read().strip()
eng: OpenAI_DSP_Engine = OpenAI_DSP_Engine(model=model, api_key=api_key, verbose_init=True)
else:
raise ValueError(f"Model {model=} not supported.")
# - Full proof search with DSP
full_proof_search_dsp_lean(eng, path_2_eval_dataset)
# - End run
wandb.config.update(config)
print(f"{wandb.config=}")
run.finish()
if __name__ == "__main__":
import time
start_time = time.time()
fire.Fire(main)
print(f"Time taken: {time.time() - start_time:.2f} seconds, or {(time.time() - start_time) / 60:.2f} minutes, or {(time.time() - start_time) / 3600:.2f} hours.\a")

162
examples/lean4_dsp/solve/dsp_lean_prompts.py Normal file
View File

@ -0,0 +1,162 @@
"""
core part of data for prompt for dsp:
"nl_problem": ..., # x*_nl
"nl_solution": ..., # y*_nl = draft*
"fl_problem": ..., # x*_fl
"fl_partial_sketch": ..., # z_fl example = sketch
"src_header_fl_problem": ..., #src_header_x*_fl
"fl_header_sketch": ..., # hz_fl suggested header
"""
import json
import sys
from pathlib import Path
from typing import Optional
# just an example of stop tokens from the MATH eval code
# STOP_TOKENS: list[str] = ["Solution:", "Problem:", "Question:", "USER:", "USER:", "USER", "ASSISTANT:", "ASSISTANT", "Instruction:", "Instruction", "Response:", "Response"]
default_path_2_examples = '~/gold-ai-olympiad/data/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json'
# -- Prompt draft (P_draft) for Lean 4
"""
Draft an informal solution similar to the one below.
The informal solution will be used to sketch a formal proof in the Lean 4 Proof Assistant.
Here are some examples:
Informal:
(*### Problem\n\n
[...nl/i problem text...]\n\n
### Solution\n\n
[...nl/i solution/draft text...]\n\n
*)\n\n
Informal:
(*### Problem\n\n
{nl_problem}
### Solution\n\n
[...Model Completion...]
"""
SYSTEM_PROMPT_DRAFT_V0 = 'You are an expert mathematician and an expert in the Lean 4 Proof Assistant.'
STOP_TOKENS_DRAFT_V0: list[str] = ['Informal:', '(*### Problem']
prompt_draft_template_lean4_v0 = ("Draft an informal solution similar to the one below. "
"The informal solution will be used to sketch a formal proof in the Lean 4 Proof Assistant. "
"Here are some examples of informal problem solutions pairs:\n")
def get_prompt_draft_template_4_lean_v0(
path_2_examples: str = default_path_2_examples,
start: int = 0,
end: int = sys.maxsize,
prompt_draft_template_4_lean: Optional[str] = prompt_draft_template_lean4_v0,
verbose: bool = False,
):
path_2_examples = Path(path_2_examples).expanduser()
# load json file with list of dicts from file in one line
with open(path_2_examples, 'r') as f:
examples: list[dict] = json.load(f)
print(f'{len(examples)=}') if verbose else None
examples = examples[start:end]
# -- Create prompt by appending few shot examples
for example in examples:
nl_problem = example['nl_problem']
new_few_shot_example = "\nInformal:\n(*### Problem\n\n" + ' '.join(nl_problem)
nl_solution_sketch = example['nl_solution_sketch']
new_few_shot_example += "\n\n### Solution\n\n" + ' '.join(nl_solution_sketch) + "*)\n"
prompt_draft_template_4_lean += new_few_shot_example
# Add part to elicit model to do task
prompt_draft_template_4_lean += "\nInformal: \n(*### Problem\n\n{nl_problem}\n\n### Solution\n"
# Return
print(prompt_draft_template_4_lean) if verbose else None
return prompt_draft_template_4_lean
prompt_draft_template_lean4_v0 = get_prompt_draft_template_4_lean_v0()
# -- Prompt sketch (P_sketch) for Lean 4
"""
[... Translate informal draft to a formal sketch in Lean 4. Here are some examples: ...]
Informal:\n
(*### Problem\n\n
[...nl/i problem text...]\n\n
### Solution\n\n
[...nl/i solution/draft text...]\n\n
*)\n\n
Formal:\n
[...fl/i problem text...]
[...fl/i partial sketch text...]
\n\n
Informal:\n
(*### Problem\n\n
{nl_problem}
### Solution\n\n
{nl_solution}
*)\n\n
Formal:\n
{fl_problem}
[...Model Completion...]
"""
# tasks is mostly writing lean but perhaps making it think it's good at maths is also good? we could later test just focusing system prompting it to be good at Lean 4.
SYSTEM_PROMPT_SKETCH_V0 = 'You are an expert mathematician and an expert in the Lean 4 Proof Assistant.'
STOP_TOKENS_SKETCH_V0: list[str] = ['Informal:', '(*### Problem', '###Solution', 'Formal:']
prompt_sketch_template_lean4_v0 = ("Translate the informal solution into a sketch in the "
"formal Lean 4 proof. Add <TODO_PROOF_OR_HAMMER> in the formal sketch whenever possible. "
"<TODO_PROOF_OR_HAMMER> will be used to call a automated theorem prover or tactic in Lean 4. "
"Here are some examples:\n"
)
def get_prompt_sketch_template_4_lean_v0(
path_2_examples: str = default_path_2_examples,
start: int = 0,
end: int = sys.maxsize,
prompt_sketch_template_4_lean: Optional[str] = prompt_sketch_template_lean4_v0,
autoformalize_prob_in_prompt: Optional[bool] = False,
verbose: bool = False,
):
path_2_examples = Path(path_2_examples).expanduser()
# load json file with list of dicts from file in one line
with open(path_2_examples, 'r') as f:
examples: list[dict] = json.load(f)
print(f'{len(examples)=}') if verbose else None
examples = examples[start:end]
# -- Create prompt by appending few shot examples
for example in examples:
# TODO: might need to figure out the header thing
nl_problem = example['nl_problem']
new_few_shot_example = "\nInformal:\n(*### Problem\n\n" + ' '.join(nl_problem)
nl_solution_sketch = example['nl_solution_sketch']
new_few_shot_example += "\n\n### Solution\n\n" + ' '.join(nl_solution_sketch) + "*)\n"
fl_problem = example['fl_problem']
fl_header_sketch = example['fl_header_sketch']
fl_header_sketch = '\n'.join(fl_header_sketch) + '\n\n'
new_few_shot_example += "\nFormal:\n"+ fl_header_sketch + ' '.join(fl_problem)
fl_partial_sketch = example['fl_partial_sketch']
new_few_shot_example += ' '.join(fl_partial_sketch)
prompt_sketch_template_4_lean += new_few_shot_example
# Add part to elicit model to do task
if autoformalize_prob_in_prompt:
prompt_sketch_template_4_lean += "\nInformal:\n(*### Problem\n\n{nl_problem}\n\n### Solution\n\n{nl_solution}*)\n\nFormal:\n"
else:
prompt_sketch_template_4_lean += "\nInformal:\n(*### Problem\n\n{nl_problem}\n\n### Solution\n\n{nl_solution}*)\n\nFormal:\n{fl_problem}"
# Return
print(prompt_sketch_template_4_lean) if verbose else None
return prompt_sketch_template_4_lean
prompt_sketch_template_lean4_v0 = get_prompt_sketch_template_4_lean_v0()
# -- Main
def main(
verbose: bool = True,
):
# -- Print Prompt Draft
# print('-- Prompt Draft --')
# print(prompt_draft_template_lean4_v0)
# -- Print Prompt Sketch
print('-- Prompt Sketch --')
sketch_prompt: str = get_prompt_sketch_template_4_lean_v0(verbose=verbose)
# print(prompt_sketch_template_lean4_v0)
print(sketch_prompt)
if __name__ == '__main__':
import time
start = time.time()
# fire.Fire()
main()
end = time.time()
print(f'Time elapsed: {end - start} seconds, or {(end - start) / 60} minutes, or {(end - start) / 3600} hours.')

186
examples/lean4_dsp/solve/dsp_prompt_draft_4_isabelle.py Normal file
View File

@ -0,0 +1,186 @@
examples_for_dsp_draft_prompt_original = [
{"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"},
{"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"},
{"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"}
]
examples_for_dsp_draft_prompt_template = [
{
"tag": "aimeI_2000_p7",
"category": "algebra",
"metadata": {},
"prompt": (
"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"
"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"
"Formal:\n"
"theorem\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\"\n"
"proof -\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\n"
"qed"
),
},
{
"tag": "algebra_2rootsintpoly_am10tap11eqasqpam110",
"category": "algebra",
"metadata": {},
"prompt": (
"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"
"Formal:\n"
"theorem\n"
" fixes a :: complex\n"
" shows \"(a-10) * (a+11) = a^2 + a -110\"\n"
"proof -\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\n"
"qed"
),
},
{
"tag": "mathd_numbertheory_335",
"category": "number_theory",
"metadata": {},
"prompt": (
"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"
"Formal:\n"
"theorem\n"
" fixes n :: nat\n"
" assumes h0 : \"n mod 7 = 5\"\n"
" shows \"(5 * n) mod 7 = 4\"\n"
"proof -\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\n"
"qed"
),
}
]
# -- Prompts for generating (informal) drafts (basically informal/natural language solution strings, that contain less details than a formal proof, hence why they are called "drafts")
prompt_draft_template_4_isabelle = """Draft an informal solution similar to the one below.
The informal solution will be used to sketch a formal Isabelle proof.
Here are some examples: \n"""
for example in examples_for_dsp_draft_prompt_template:
# P_draft_isa_prompt_template += ("Example:\n" + x['prompt'][:x['prompt'].find('Formal:')] + "\n\n")
# - Extract the 'prompt' field from the current example
prompt_text = example['prompt']
# - Find the index where the 'Formal:' keyword starts
formal_index = prompt_text.find('Formal:')
# - Extract the part of the prompt before the 'Formal:' keyword
nl_prob_soln = prompt_text[:formal_index] # Append nl/i draft examples: prob_nl, soln_nl/draft_nl
# - Append this i draft example our prompt draft/P_draft
prompt_draft_template_4_isabelle += f"Example:\n{informal_part}\n\n"
# append the final part of the prompt template that prompts model to do prediction, we'd need to insert new nl problem text here before using it
prompt_draft_template_4_isabelle += """Informal:
(*### Problem
"""
# P_sketch isabelle, ref: https://github.com/brando90/ntptutorial-II/blob/main/partII_dsp/notebooks/II_dsp__part2_dsp.ipynb
prompt = """Translate the informal solution into a sketch of the
formal Isabelle proof. Add `sledgehammer` in the sketch whenever
possible. `sledgehammer` will be used to call the automated Sledgehammer prover.
Here are some examples:
"""
for x in examples:
prompt += (x['prompt'] + "\n\n")
prompt += """Informal:
(*### Problem
"""
xf = """theorem
fixes x :: int
assumes h0: "even x"
shows "odd (x+5)" """
zi = p.f(prompt, xi + '\n\n' + yi + '\n\n' + xf)
print(zi)

32
examples/lean4_dsp/solve/readme.md Normal file
View File

@ -0,0 +1,32 @@
#
## Related work
### Tony's AF
Ton'y original AF: ((Yuhuai et al.))[https://arxiv.org/abs/2205.12615]
Tony's paper improve MiniF2F from: `29.6% to 35.2%`, by `5.6%`.
Expert Iteration:
- AF used: "We explore if one can improve neural theorem provers by training the neural models on proofs of automatically translated theorems".
- they only translate **problem theorems** (nl_thm := "problem + answer") then use a prover to get the formal proof.
- ExpIt algorithn:
- `M_0 := Isabelle_Thor()`
- `Search/Prover := Best_First_Search()` # TODO recall best first search
- ExpIT.fine_tune := "train model to predict next proof_step/tactic given current proof_state and previous proof_step on successful proofs.
- i.e., `<x=(proof_state_{t}, proof_step_{t-1}), y=(proof_step_{t})>` #TODO: I think, confirm with Albert https://twitter.com/messages/1253358235-1267913180153548800
Base Model for Neural Theorem Prover (NTP):
- Thor_GPT2 := "We use a pre-trained and fine-tuned Thor based on a GPT-2 with 700M non-embedding parameters." Note: ReProver used 299M parameters enc-dec.
- fine-tuned on the PILE arxiv + github
Neural Theorem Prover (NTP) for `M_0`:
- Thor :=
- The Thor agent is fine-tuned on the PISA dataset which consists of 2.49 million proof steps from the Isabelle/HOL library.
- The model is trained with the objective to predict the next token in va proof step, given the proof state and the last proof step.
- proof step := "tactic in Isabelle" #TODO confirm with Albert https://twitter.com/messages/1253358235-1267913180153548800
Questions:
- Q1: what is this: "we perform deduplication by problem statements" when does it matter? All MATH train are unique, so why would I care about this?
Idea:
- Idea1: use the formal ground truth solution string in MATH, implement Draft Sketch Proof (DSP) for Lean4 + use some symbolic/ntp solver (hammer/tidy/ReProver)