resolved comments

Author: root

examples/EarlyStopping/game24_example.py

@@ -25,7 +25,7 @@ def get_model_short_name(model_name: str) -> str:
     short_name = short_name.replace(" ", "_").replace(":", "-")
     return short_name
 
-def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/Gameof24_results"):
+def get_output_dirs(main_model: str, base_dir: str = "../../Outputs/Gameof24_results"):
     """Create and return output directory paths based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
@@ -42,14 +42,14 @@ def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/
 
     return dirs
 
-def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/Gameof24_results") -> str:
+def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs/Gameof24_results") -> str:
     """Generate log filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
     os.makedirs(output_base, exist_ok=True)
     return os.path.join(output_base, f"EAT_{num_examples}examples.log")
 
-def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/Gameof24_results") -> str:
+def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs/Gameof24_results") -> str:
     """Generate token CSV filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)

examples/EarlyStopping/maze_example.py

@@ -28,7 +28,7 @@ def get_model_short_name(model_name: str) -> str:
     short_name = short_name.replace(" ", "_").replace(":", "-")
     return short_name
 
-def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/MazeResults"):
+def get_output_dirs(main_model: str, base_dir: str = "../Outputs/MazeResults"):
     """Create and return output directory paths based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
@@ -46,14 +46,14 @@ def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/
 
     return dirs
 
-def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/MazeResults") -> str:
+def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../Outputs/MazeResults") -> str:
     """Generate log filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
     os.makedirs(output_base, exist_ok=True)
     return os.path.join(output_base, f"EAT_{num_examples}examples.log")
 
-def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/MazeResults") -> str:
+def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../Outputs/MazeResults") -> str:
     """Generate token CSV filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)

examples/EarlyStopping/spatialmap_example.py

@@ -28,7 +28,7 @@ def get_model_short_name(model_name: str) -> str:
     short_name = short_name.replace(" ", "_").replace(":", "-")
     return short_name
 
-def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/SpatialMap_results"):
+def get_output_dirs(main_model: str, base_dir: str = "../Outputs/SpatialMap_results"):
     """Create and return output directory paths based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
@@ -46,14 +46,14 @@ def get_output_dirs(main_model: str, base_dir: str = "../../Outputs_SANITY_FULL/
 
     return dirs
 
-def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/SpatialMap_results") -> str:
+def get_log_filename(main_model: str, num_examples: int, base_dir: str = "../Outputs/SpatialMap_results") -> str:
     """Generate log filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)
     os.makedirs(output_base, exist_ok=True)
     return os.path.join(output_base, f"EAT_{num_examples}examples.log")
 
-def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../../Outputs_SANITY_FULL/SpatialMap_results") -> str:
+def get_token_filename(main_model: str, num_examples: int, base_dir: str = "../Outputs/SpatialMap_results") -> str:
     """Generate token CSV filename based on model name."""
     model_short_name = get_model_short_name(main_model)
     output_base = os.path.join(base_dir, model_short_name)

examples/TTSwithVerification/mazemeta.py

@@ -377,7 +377,7 @@ def evaluate_maze_answer(answer, options, ground_truth):
             answer = asyncio.run(stream_completion(
                 full_prompt,
                 llm_server=llm_server,
-                monitors=(),
+                monitors=(monitor),
                 add_delay=False,
                 termination_requires_validation=False,
                 async_execution=True

examples/TTSwithVerification/spatialmeta.py

@@ -439,7 +439,7 @@ def evaluate_spatialmap_answer(answer, options, ground_truth):
             answer = asyncio.run(stream_completion(
                 full_prompt,
                 llm_server=llm_server,
-                monitors=(),
+                monitors=(monitor,),
                 add_delay=False,
                 termination_requires_validation=False,
                 async_execution=True

interwhen/utils/spatialmap_verifier.py

@@ -13,7 +13,7 @@
 
 import re
 from typing import Dict, List, Tuple, Optional, Set
-from z3 import Solver, Real, And, sat
+from z3 import Solver, Real, And, Not, sat, unsat
 
 
 class SpatialMapZ3Solver:
@@ -259,9 +259,8 @@ def count_objects_in_direction(
             # Check if this entity MUST be in that direction
             # (i.e. the negation is unsatisfiable)
             self.solver.push()
-            from z3 import Not
             self.solver.add(Not(constraint))
-            must_be = self.solver.check() != sat
+            must_be = self.solver.check() == unsat
             self.solver.pop()
 
             if must_be:
@@ -487,7 +486,7 @@ def verify_spatialmap_step(
     Returns:
         (is_valid, errors)
     """
-    from z3 import Not as Z3Not, sat as z3sat
+    from z3 import Not as Z3Not, unsat as z3unsat
 
     errors = []
 
@@ -508,7 +507,7 @@ def verify_spatialmap_step(
         if compiled is not None:
             z3_solver.solver.push()
             z3_solver.solver.add(Z3Not(compiled))
-            is_entailed = z3_solver.solver.check() != z3sat
+            is_entailed = z3_solver.solver.check() == z3unsat
             z3_solver.solver.pop()
             if is_entailed:
                 z3_solver.apply_ir(claim)
@@ -725,7 +724,7 @@ def get_possible_count_range(
 
     Returns ``None`` if the reference entity cannot be found.
     """
-    from z3 import And as Z3And, Not as Z3Not, sat as z3sat
+    from z3 import And as Z3And, Not as Z3Not, sat as z3sat, unsat as z3unsat
 
     direction = direction.lower().strip()
     if direction in ('north', 'south', 'east', 'west'):
@@ -782,7 +781,7 @@ def _find(name):
         # Must it be?
         solver.solver.push()
         solver.solver.add(Z3Not(c))
-        must_be = solver.solver.check() != z3sat
+        must_be = solver.solver.check() == z3unsat
         solver.solver.pop()
 
         if must_be: