From a5747122cd4971b21b248d2a01c2a59a33159a56 Mon Sep 17 00:00:00 2001 From: Chuyue Sun Date: Wed, 5 Jun 2024 13:49:34 -0700 Subject: [PATCH] new semantic --- pantograph/search_llm.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/pantograph/search_llm.py b/pantograph/search_llm.py index 89ea810..b47c1bb 100644 --- a/pantograph/search_llm.py +++ b/pantograph/search_llm.py @@ -19,11 +19,9 @@ class LLMAgent(Agent): "intro", ] self.tactics = [ - "intro h", - "cases h", "simp", - "apply Or.inl", - "apply Or.inr", + "rfl", + "decide", ] self.no_space_tactics = [ "assumption", @@ -40,10 +38,8 @@ class LLMAgent(Agent): tactics = self.tactics else: tactics = self.no_space_tactics - if i >= len(tactics): return None - self.goal_tactic_id_map[key] = i + 1 new_state = None for ii in range(self.n_trials):