experiment: Proof search function from llemma_formal2formal

data/test.jsonl

@@ -0,0 +1,2 @@
+{"full_name": "testing1", "statement": "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b", "file_path": "None"}
+{"full_name": "testing2", "statement": "forall (p q: Prop), Or p q -> Or q p", "file_path": "None"}

output/test/30-05-2024-12-29/logs/testing1.txt

@@ -0,0 +1,49 @@
+Theorem number: 1
+
+Initial state:
+⊢ ∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b
+
+---------------------------
+Iteration 1
+---------------------------
+
+Tactic candidates:
+['intros a b h']
+
+Tactic scores (-log prob):
+[0.30103418611]
+
+Tactic 1 result: not solved
+a : Nat
+b : Nat
+h : b = 2
+⊢ 1 + a + 1 = a + b
+
+---------------------------
+Iteration 2
+---------------------------
+
+Tactic candidates:
+['rw [h]']
+
+Tactic scores (-log prob):
+[0.0892465625]
+
+Tactic 1 result: not solved
+a : Nat
+b : Nat
+h : b = 2
+⊢ 1 + a + 1 = a + 2
+
+---------------------------
+Iteration 3
+---------------------------
+
+Tactic candidates:
+['rw [h]']
+
+Tactic scores (-log prob):
+[0.2368663525]
+
+Theorem error
+Failure reason: ServerError ["tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n  b\na b : Nat\nh : b = 2\n⊢ 1 + a + 1 = a + 2"]

output/test/30-05-2024-12-29/logs/testing2.txt

@@ -0,0 +1,69 @@
+Theorem number: 2
+
+Initial state:
+⊢ forall (p q: Prop), Or p q -> Or q p
+
+---------------------------
+Iteration 1
+---------------------------
+
+Tactic candidates:
+['intros p q h']
+
+Tactic scores (-log prob):
+[0.217274595475]
+
+Tactic 1 result: not solved
+p : Prop
+q : Prop
+h : p ∨ q
+⊢ q ∨ p
+
+---------------------------
+Iteration 2
+---------------------------
+
+Tactic candidates:
+['cases h']
+
+Tactic scores (-log prob):
+[0.06462308351666667]
+
+Tactic 1 result: not solved
+p : Prop
+q : Prop
+h✝ : p
+⊢ q ∨ p
+p : Prop
+q : Prop
+h✝ : q
+⊢ q ∨ p
+
+---------------------------
+Iteration 3
+---------------------------
+
+Tactic candidates:
+['left']
+
+Tactic scores (-log prob):
+[0.602736965]
+
+Tactic 1 result: not solved
+p : Prop
+q : Prop
+h✝ : p
+⊢ q
+
+---------------------------
+Iteration 4
+---------------------------
+
+Tactic candidates:
+['exact h\\xe2\\x9c\\x9d']
+
+Tactic scores (-log prob):
+[0.00540535255116]
+
+Theorem error
+Failure reason: ServerError <pantograph>:1:11: expected end of input

output/test/30-05-2024-12-29/results__gpt-3.5-turbo__0.json

@@ -0,0 +1,54 @@
+{
+    "results": [
+        {
+            "attempt_results": [
+                {
+                    "theorem": "\u2200 (a b: Nat), (b = 2) -> 1 + a + 1 = a + b",
+                    "success": false,
+                    "failure_reason": "ServerError"
+                }
+            ],
+            "success": false,
+            "example": {
+                "full_name": "testing1",
+                "statement": "\u2200 (a b: Nat), (b = 2) -> 1 + a + 1 = a + b",
+                "file_path": "None"
+            }
+        },
+        {
+            "attempt_results": [
+                {
+                    "theorem": "forall (p q: Prop), Or p q -> Or q p",
+                    "success": false,
+                    "failure_reason": "ServerError"
+                }
+            ],
+            "success": false,
+            "example": {
+                "full_name": "testing2",
+                "statement": "forall (p q: Prop), Or p q -> Or q p",
+                "file_path": "None"
+            }
+        }
+    ],
+    "args": {
+        "model_name": "gpt-3.5-turbo",
+        "dataset_name": "test-set",
+        "shard": 0,
+        "resume_from": null,
+        "dataset_path": "data/test.jsonl",
+        "output_dir": "output/test",
+        "early_stop": false,
+        "tp_degree": 1,
+        "num_shards": 8,
+        "max_iters": 5,
+        "timeout": 600,
+        "num_examples": -1,
+        "num_samples": 1,
+        "clear_process_hours": 3,
+        "temperatures": [
+            0.0
+        ],
+        "api_key_path": "../api_key/key.txt"
+    }
+}