From 3d2e737e0ce073a28bdbf0129db74183701d64e9 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Wed, 29 May 2024 20:57:54 -0700 Subject: [PATCH 1/4] change poetry.lock --- poetry.lock | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/poetry.lock b/poetry.lock index 0d47380..9e5a1ac 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,15 +1,10 @@ -# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. - [[package]] name = "pexpect" version = "4.9.0" description = "Pexpect allows easy control of interactive console applications." +category = "main" optional = false python-versions = "*" -files = [ - {file = "pexpect-4.9.0-py2.py3-none-any.whl", hash = "sha256:7236d1e080e4936be2dc3e326cec0af72acf9212a7e1d060210e70a47e253523"}, - {file = "pexpect-4.9.0.tar.gz", hash = "sha256:ee7d41123f3c9911050ea2c2dac107568dc43b2d3b0c7557a33212c398ead30f"}, -] [package.dependencies] ptyprocess = ">=0.5" @@ -18,14 +13,15 @@ ptyprocess = ">=0.5" name = "ptyprocess" version = "0.7.0" description = "Run a subprocess in a pseudo terminal" +category = "main" optional = false python-versions = "*" -files = [ - {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"}, - {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"}, -] [metadata] -lock-version = "2.0" +lock-version = "1.1" python-versions = "^3.10" content-hash = "54cb66612c110a515f024e54d2b2a0af54ffcbe06602ad7f4ea6a446699d419a" + +[metadata.files] +pexpect = [] +ptyprocess = [] From 90a3a7bd3d026619e748926c01424173efff83c6 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Sun, 2 Jun 2024 14:16:15 -0700 Subject: [PATCH 2/4] update poetry lock; add llm feedback --- pantograph/gen_tactic.py | 76 ++++++++++++++++++++++++++-------------- poetry.lock | 18 ++++++---- 2 files changed, 60 insertions(+), 34 deletions(-) diff --git a/pantograph/gen_tactic.py b/pantograph/gen_tactic.py index 68c7ccb..1d98fd1 100644 --- a/pantograph/gen_tactic.py +++ b/pantograph/gen_tactic.py @@ -1,4 +1,4 @@ -from pantograph.server import Server +from pantograph.server import Server, ServerError from pantograph.expr import Variable, Goal, TacticCalc import unittest import sglang as sgl @@ -16,22 +16,36 @@ def multi_turn_question(s, question_1, question_2): @sgl.function -def select_tactic(s, state): +def select_tactic(s, server, state, goal_id, n_tries = 5): + s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.") s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])") s += sgl.assistant("```intros a b h```") s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])") s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")') s += sgl.user("The current proof state: " + str(state)) - with s.copy() as tmp: - tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64)) - print("==tmp===") - print(tmp["tactic"]) - tactic = extract_code_from_llm_output(tmp["tactic"]) - s += sgl.assistant("```"+tactic+"```") - return tactic - + for i in range(n_tries): + with s.copy() as tmp: + tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64)) + print("==tmp===") + print(tmp["tactic"]) + tactic = extract_code_from_llm_output(tmp["tactic"]) + s += sgl.assistant("```"+tactic+"```") + success, new_state = apply_tactic(server, state, goal_id, tactic) + if not success: + with s.user(): + s += "This answer got Lean compile error:\n" + str(new_state) + "\n" + s += "Please try again by taking the Lean compiler feedback." + + else: + return new_state +def apply_tactic(server, state, goal_id, tactic): + try: + new_state = server.goal_tactic(state, goal_id=goal_id, tactic=tactic) + except ServerError as e: + return False, e + return True, new_state def extract_code_from_llm_output(reply): i = reply.find("```lean") @@ -51,6 +65,7 @@ def extract_code_from_llm_output(reply): class TestServerSGL(unittest.TestCase): def test_conv_calc_sgl(self): + n_trails = 5 sgl.set_default_backend(sgl.OpenAI("gpt-4")) server = Server() @@ -80,14 +95,21 @@ class TestServerSGL(unittest.TestCase): target="a + 1 + 1 = a + b", ), ]) - state = select_tactic.run(str(state2)) - tactic = state.ret_value - for m in state.messages(): - print(m["role"], ":", m["content"]) + state3 = None + for i in range(n_trails): + print(f"===============trail {str(i)}============") + try: + state = select_tactic.run(server, state2, goal_id = 1) + state3 = state.ret_value + for m in state.messages(): + print(m["role"], ":", m["content"]) + + print("\n-- new state --\n", state3) + + except ServerError as e: + print(f"server error: {e}") + continue - print("\n-- tactic --\n", tactic) - - state3 = server.goal_tactic(state2, goal_id=1, tactic=tactic) print("==========state3============") print(state3) # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]") @@ -119,19 +141,19 @@ class TestServerSGL(unittest.TestCase): # print() - def test_sglang_openai(self): - sgl.set_default_backend(sgl.OpenAI("gpt-4")) + # def test_sglang_openai(self): + # sgl.set_default_backend(sgl.OpenAI("gpt-4")) - print('\n----- Test sglang ---') - state = multi_turn_question.run( - question_1="What is the capital of the United States?", - question_2="List two local attractions.", - ) + # print('\n----- Test sglang ---') + # state = multi_turn_question.run( + # question_1="What is the capital of the United States?", + # question_2="List two local attractions.", + # ) - for m in state.messages(): - print(m["role"], ":", m["content"]) + # for m in state.messages(): + # print(m["role"], ":", m["content"]) - print("\n-- answer_1 --\n", state["answer_1"]) + # print("\n-- answer_1 --\n", state["answer_1"]) if __name__ == '__main__': diff --git a/poetry.lock b/poetry.lock index 9e5a1ac..f4c20f5 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,10 +1,15 @@ +# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand. + [[package]] name = "pexpect" version = "4.9.0" description = "Pexpect allows easy control of interactive console applications." -category = "main" optional = false python-versions = "*" +files = [ + {file = "pexpect-4.9.0-py2.py3-none-any.whl", hash = "sha256:7236d1e080e4936be2dc3e326cec0af72acf9212a7e1d060210e70a47e253523"}, + {file = "pexpect-4.9.0.tar.gz", hash = "sha256:ee7d41123f3c9911050ea2c2dac107568dc43b2d3b0c7557a33212c398ead30f"}, +] [package.dependencies] ptyprocess = ">=0.5" @@ -13,15 +18,14 @@ ptyprocess = ">=0.5" name = "ptyprocess" version = "0.7.0" description = "Run a subprocess in a pseudo terminal" -category = "main" optional = false python-versions = "*" +files = [ + {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"}, + {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"}, +] [metadata] -lock-version = "1.1" +lock-version = "2.0" python-versions = "^3.10" content-hash = "54cb66612c110a515f024e54d2b2a0af54ffcbe06602ad7f4ea6a446699d419a" - -[metadata.files] -pexpect = [] -ptyprocess = [] From 155c26e9834cff18bebcf364dbdca9471c1ba905 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Sun, 2 Jun 2024 18:53:23 -0700 Subject: [PATCH 3/4] revert poetry.lock; add rw tutorial --- pantograph/gen_tactic.py | 70 ++++++++++++++++++++++++++++++++++++++-- poetry.lock | 2 +- 2 files changed, 68 insertions(+), 4 deletions(-) diff --git a/pantograph/gen_tactic.py b/pantograph/gen_tactic.py index 1d98fd1..6db1fb8 100644 --- a/pantograph/gen_tactic.py +++ b/pantograph/gen_tactic.py @@ -3,8 +3,69 @@ from pantograph.expr import Variable, Goal, TacticCalc import unittest import sglang as sgl +LEAN4_INTRO = '''/-- A sequence `u` of real numbers converges to `l` if `∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n - l| ≤ ε`. +This condition will be spelled `seq_limit u l`. -/ +def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := +∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε +/- In the above definition, note that the `n`-th term of the sequence `u` is denoted +simply by `u n`. +Similarly, in the next definition, `f x` is what we would write `f(x)` on paper. +Also note that implication is denoted by a single arrow (we'll explain why later). -/ + +/-- A function`f : ℝ → ℝ` is continuous at `x₀` if +`∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ ⇒ |f(x) - f(x₀)| ≤ ε`. +This condition will be spelled `continuous_at f x₀`.-/ +def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) : Prop := +∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε + +/-- Now we claim that if `f` is continuous at `x₀` then it is sequentially continuous +at `x₀`: for any sequence `u` converging to `x₀`, the sequence `f ∘ u` converges +to `f x₀`. -/ +example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) (hf : continuous_at f x₀) : + seq_limit (f ∘ u) (f x₀) := by { -- This `by` keyword marks the beginning of the proof + -- Put your text cursor here and watch the Lean InfoView panel to the right. + -- Then move your cursor from line to line in the proof while monitoring the Infoview. + + -- Our goal is to prove that, for any positive `ε`, there exists a natural + -- number `N` such that, for any natural number `n` at least `N`, + -- `|f(u_n) - f(x₀)|` is at most `ε`. + unfold seq_limit + -- Fix a positive number `ε`. + intros ε hε + -- By assumption on `f` applied to this positive `ε`, we get a positive `δ` + -- such that, for all real number `x`, if `|x - x₀| ≤ δ` then `|f(x) - f(x₀)| ≤ ε` (1). + obtain ⟨δ, δ_pos, Hf⟩ : ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε := hf ε hε + -- The assumption on `u` applied to this `δ` gives a natural number `N` such that + -- for every natural number `n`, if `n ≥ N` then `|u_n - x₀| ≤ δ` (2). + obtain ⟨N, Hu⟩ : ∃ N, ∀ n ≥ N, |u n - x₀| ≤ δ := hu δ δ_pos + -- Let's prove `N` is suitable. + use N + -- Fix `n` which is at least `N`. Let's prove `|f(u_n) - f(x₀)| ≤ ε`. + intros n hn + -- Thanks to (1) applied to `u_n`, it suffices to prove that `|u_n - x₀| ≤ δ`. + apply Hf + -- This follows from property (2) and our assumption on `n`. + exact Hu n hn + -- This finishes the proof! + } + +/- +Now that this proof is over, you can use the file explorer to the +left of this panel to open the file `Exercises > 01Rewriting.lean`. +-/''' + +LEAN4_REWRITE = ''' +example (a b c : Nat) : a + b + c = a + c + b := by + rw [Nat.add_assoc, Nat.add_comm b, ← Nat.add_assoc] + +example (a b c : Nat) : a + b + c = a + c + b := by + rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm b] + +example (a b c : Nat) : a + b + c = a + c + b := by + rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm _ b] +''' @sgl.function def multi_turn_question(s, question_1, question_2): @@ -16,15 +77,16 @@ def multi_turn_question(s, question_1, question_2): @sgl.function -def select_tactic(s, server, state, goal_id, n_tries = 5): +def select_tactic(s, server, state, goal_id, feedback_turns = 5): s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.") + s += sgl.user(LEAN4_REWRITE) s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])") s += sgl.assistant("```intros a b h```") s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])") s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")') s += sgl.user("The current proof state: " + str(state)) - for i in range(n_tries): + for i in range(feedback_turns): with s.copy() as tmp: tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64)) print("==tmp===") @@ -99,7 +161,7 @@ class TestServerSGL(unittest.TestCase): for i in range(n_trails): print(f"===============trail {str(i)}============") try: - state = select_tactic.run(server, state2, goal_id = 1) + state = select_tactic.run(server, state2, goal_id = 0) state3 = state.ret_value for m in state.messages(): print(m["role"], ":", m["content"]) @@ -109,6 +171,8 @@ class TestServerSGL(unittest.TestCase): except ServerError as e: print(f"server error: {e}") continue + state3 = server.goal_tactic(state2, goal_id=0, tactic="rw [Nat.add_assoc]") + print("==========state3============") print(state3) diff --git a/poetry.lock b/poetry.lock index f4c20f5..0d47380 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. [[package]] name = "pexpect" From f9fe626aa8a24498f809b553927701fd18663f56 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Sun, 2 Jun 2024 19:51:20 -0700 Subject: [PATCH 4/4] update llm gen tactics tests --- pantograph/gen_tactic.py | 85 +++++++++++++++++++++------------------- 1 file changed, 45 insertions(+), 40 deletions(-) diff --git a/pantograph/gen_tactic.py b/pantograph/gen_tactic.py index 6db1fb8..24442ac 100644 --- a/pantograph/gen_tactic.py +++ b/pantograph/gen_tactic.py @@ -56,7 +56,7 @@ Now that this proof is over, you can use the file explorer to the left of this panel to open the file `Exercises > 01Rewriting.lean`. -/''' -LEAN4_REWRITE = ''' +LEAN4_REWRITE = '''Rewrite tactic tutorial: example (a b c : Nat) : a + b + c = a + c + b := by rw [Nat.add_assoc, Nat.add_comm b, ← Nat.add_assoc] @@ -65,6 +65,17 @@ example (a b c : Nat) : a + b + c = a + c + b := by example (a b c : Nat) : a + b + c = a + c + b := by rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm _ b] + +example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by + rw [Nat.add_zero] at h + rw [h] + +def Tuple (α : Type) (n : Nat) := + { as : List α // as.length = n } + +example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by + rw [h] at t + exact t ''' @sgl.function @@ -161,63 +172,57 @@ class TestServerSGL(unittest.TestCase): for i in range(n_trails): print(f"===============trail {str(i)}============") try: - state = select_tactic.run(server, state2, goal_id = 0) + state = select_tactic.run(server, state2, goal_id = 1) state3 = state.ret_value for m in state.messages(): print(m["role"], ":", m["content"]) print("\n-- new state --\n", state3) + break except ServerError as e: print(f"server error: {e}") continue - state3 = server.goal_tactic(state2, goal_id=0, tactic="rw [Nat.add_assoc]") + state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2")) print("==========state3============") print(state3) - # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]") - # print("==========state4============") - # print(state4) - # self.assertTrue(state4.is_solved) + state4 = None + for i in range(n_trails): + print(f"===============trail {str(i)}============") + try: + state = select_tactic.run(server, state3, goal_id = 0) + state4 = state.ret_value + for m in state.messages(): + print(m["role"], ":", m["content"]) + + print("\n-- new state --\n", state4) + break + + except ServerError as e: + print(f"server error: {e}") + continue + + state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]") + print("==========state4============") + print(state4) + self.assertTrue(state4.is_solved) - # print("==========state2============") - # print(state2) - # state_c1 = server.goal_conv_begin(state2, goal_id=0) - # print("==========state c1============") - # print(state_c1) - # state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs") - # print("==========state c2============") - # print(state_c2) - # state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]") - # print("==========state c3============") - # print(state_c3) - # state_c4 = server.goal_conv_end(state_c3) - # print("==========state c4============") - # print(state_c4) + def test_sglang_openai(self): + sgl.set_default_backend(sgl.OpenAI("gpt-4")) - # state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl") - # print("==========state c5============") - # print(state_c5) - # self.assertTrue(state_c5.is_solved) + print('\n----- Test sglang ---') + state = multi_turn_question.run( + question_1="What is the capital of the United States?", + question_2="List two local attractions.", + ) - # print() + for m in state.messages(): + print(m["role"], ":", m["content"]) - - # def test_sglang_openai(self): - # sgl.set_default_backend(sgl.OpenAI("gpt-4")) - - # print('\n----- Test sglang ---') - # state = multi_turn_question.run( - # question_1="What is the capital of the United States?", - # question_2="List two local attractions.", - # ) - - # for m in state.messages(): - # print(m["role"], ":", m["content"]) - - # print("\n-- answer_1 --\n", state["answer_1"]) + print("\n-- answer_1 --\n", state["answer_1"]) if __name__ == '__main__':