Upload folder using huggingface_hub

compile_result/lean4_basic_test/lean4_random_15k_rftpass5.jsonl

@@ -0,0 +1,5 @@
+{
+  "results": [],
+  "pass_1": 0,
+  "pass_5": 0
+}

compile_result/lean4_basic_test/output.log

@@ -1,6 +1,16 @@
-
-Pass@1: 0.21311475409836064
-Pass@5: 0.3155737704918033
+
+Pass@1: 0.1762295081967213
+Pass@5: 0.29508196721311475
+Traceback (most recent call last):
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 273, in <module>
+    main(args)
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 259, in main
+    multi(command_list, args.output_path, args.k)
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 209, in multi
+    os.makedirs(os.path.dirname(output_file), exist_ok=True)
+  File "/usr/lib/python3.9/os.py", line 225, in makedirs
+    mkdir(name, mode)
+FileNotFoundError: [Errno 2] No such file or directory: ''
 
 
 

compile_result/lean4_random_test/output.log

@@ -1,34 +1,16 @@
-
+
+Pass@1: 0.15126050420168066
+Pass@5: 0.2605042016806723
 Traceback (most recent call last):
-  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 165, in multi
-    result = future.result()
-  File "/usr/lib/python3.9/concurrent/futures/_base.py", line 435, in result
-    self._condition.wait(timeout)
-  File "/usr/lib/python3.9/threading.py", line 312, in wait
-    waiter.acquire()
-KeyboardInterrupt
-
-During handling of the above exception, another exception occurred:
-
-Traceback (most recent call last):
-  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 266, in <module>
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 273, in <module>
     main(args)
-  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 252, in main
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 259, in main
     multi(command_list, args.output_path, args.k)
-  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 166, in multi
-    results.append(result)
-  File "/usr/lib/python3.9/concurrent/futures/_base.py", line 628, in __exit__
-    self.shutdown(wait=True)
-  File "/usr/lib/python3.9/concurrent/futures/thread.py", line 229, in shutdown
-    t.join()
-  File "/usr/lib/python3.9/threading.py", line 1033, in join
-    self._wait_for_tstate_lock()
-  File "/usr/lib/python3.9/threading.py", line 1049, in _wait_for_tstate_lock
-    elif lock.acquire(block, timeout):
-KeyboardInterrupt
-
-Pass@1: 0.14285714285714285
-Pass@5: 0.23949579831932774
+  File "/opt/tiger/lean4-compile/pass_rate_new_test.py", line 209, in multi
+    os.makedirs(os.path.dirname(output_file), exist_ok=True)
+  File "/usr/lib/python3.9/os.py", line 225, in makedirs
+    mkdir(name, mode)
+FileNotFoundError: [Errno 2] No such file or directory: ''
 
 
 

compile_result/wild_test/output.log

@@ -1,6 +1,6 @@
-
-Pass@1: 0.009
-Pass@5: 0.053
+
+Pass@1: 0.297
+Pass@5: 0.516
 
 
 

compile_result/wild_test_v2/output.log

@@ -0,0 +1,6 @@
+
+Pass@1: 0.187
+Pass@5: 0.392
+
+
+

pass_rate_multi_pass.py

@@ -26,11 +26,13 @@ def get_output(input_string, k):
 
 # List of input paths
 input_path_lists = [
-    # "/opt/tiger/formal-align/generate_result/zero_shot/lean4_random_test/generation/lean4_random_15k/5",
-    # "/opt/tiger/formal-align/generate_result/zero_shot/lean4_basic_test/generation/lean4_random_15k/5"
-    "/opt/tiger/formal-align/generate_result/zero_shot/wild_test/generation/lean4_random_15k/5"
+    # "/opt/tiger/formal-align/generate_result/zero_shot/lean4_random_test/generation/lean4_random_15k_rft/5",
+    # "/opt/tiger/formal-align/generate_result/zero_shot/lean4_basic_test/generation/lean4_random_15k_rft/5",
+    # "/opt/tiger/formal-align/generate_result/zero_shot/wild_test_v2/generation/lean4_random_15k_rft/5"
     # "/opt/tiger/formal-align/generate_result/zero_shot/gsm8k_train/generation/lean4_random_15k/10",
     # "/opt/tiger/formal-align/generate_result/zero_shot/math_train/generation/lean4_random_15k/10",
+    "/opt/tiger/formal-align/generate_result/zero_shot/math_train/generation/lean4_random_15k_rft/10",
+    "/opt/tiger/formal-align/generate_result/zero_shot/lean4_15k_train/generation/lean4_random_15k_rft/10",
 ]
 
 # Function to extract k from the input path

pass_rate_new_test.py

@@ -204,7 +204,7 @@ def multi(command_list, output_path, k ):
     # print(f"total test: {total}")
     # print(f"Pass rate: {pass_rate}%")
 
-    output_file = f"output_path"
+    output_file = f"{output_path}"
     # Create the directory if it doesn't exist
     os.makedirs(os.path.dirname(output_file), exist_ok=True)
 

trans_from_compile_4_training.py

@@ -48,7 +48,7 @@ def save_passed_results(input_list):
                         id_output = dedup_outputs[id]
                         if id_result.get("status") == 'pass':
                             result_dict = {
-                                'nl_statement': statement,
+                                'nl_problem': statement,
                                 'nl_proof': proof,
                                 'formal': id_output
                             }