Modify experiment parameters + add some more ground truths

frame/environments/FF/calculations.py

@@ -54,6 +54,20 @@
         z3_translation=lambda a: Z3Template(f"", a), 
         discovered_names={"specialized_(ff_multiply_at_0_to_ff_one)", "specialized_(ff_multiply_at_1_to_ff_one)" }
     ),
+    "ff_multiply_one_eq": GroundTruthEntity(
+        canonical_name="ff_multiply_one_eq",
+        entity_type=EntityType.CONCEPT,
+        description="Multiplying a finite field element with one is equal to the element itself",
+        computational_implementation=lambda a: a * FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) == a,
+        discovered_names={"compose_(ff_multiply_one_with_ff_eq_output_to_input_map={0: 0})"}
+    ),
+    "ff_multiply_one_eq_self": GroundTruthEntity(
+        canonical_name="ff_multiply_one_eq_self",
+        entity_type=EntityType.CONCEPT,
+        description="Multiplying a finite field element with one is equal to the element itself",
+        computational_implementation=lambda a: a * FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) == a,
+        discovered_names={"matched_(ff_multiply_one_eq_indices_[0, 1])"}
+    ),
     "ff_multiply_alpha": GroundTruthEntity(
         canonical_name="ff_multiply_alpha",
         entity_type=EntityType.CONCEPT,
@@ -101,6 +115,30 @@
                           "compose_(ff_add_with_ff_add_output_to_input_map={1: 0})", 
                           "compose_(ff_add_with_ff_add_output_to_input_map={1: 1})"}
     ),
+    "ff_multiply_of_three_elements": GroundTruthEntity(
+        canonical_name="ff_multiply_of_three_elements",
+        entity_type=EntityType.CONCEPT,
+        description="Multiply three finite field elements",
+        computational_implementation=lambda a, b, c: a * b * c,
+        discovered_names={"compose_(ff_multiply_with_ff_multiply_output_to_input_map={0: 0})", 
+                          "compose_(ff_multiply_with_ff_multiply_output_to_input_map={0: 1})", 
+                          "compose_(ff_multiply_with_ff_multiply_output_to_input_map={1: 0})", 
+                          "compose_(ff_multiply_with_ff_multiply_output_to_input_map={1: 1})"}
+    ),
+    "ff_multiply_of_three_elements_eq": GroundTruthEntity(
+        canonical_name="ff_multiply_of_three_elements_eq",
+        entity_type=EntityType.CONCEPT,
+        description="Multiply three finite field elements is equal to a",
+        computational_implementation=lambda a, b, c, d: a * b * c == d,
+        discovered_names={"compose_(ff_multiply_of_three_elements_with_ff_eq_output_to_input_map={0: 0})"}
+    ),
+    "ff_multiply_of_three_elements_eq_zero": GroundTruthEntity(
+        canonical_name="ff_multiply_of_three_elements_eq_zero",
+        entity_type=EntityType.CONCEPT,
+        description="Multiply three finite field elements is equal to zero",
+        computational_implementation=lambda a, b, c: a * b * c == FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)),
+        discovered_names={"specialized_(ff_multiply_of_three_elements_eq_at_1_to_ff_zero)"}
+    ),
     "ff_sum_three_times": GroundTruthEntity(
         canonical_name="ff_sum_three_times",
         entity_type=EntityType.CONCEPT,
@@ -120,7 +158,7 @@
         entity_type=EntityType.CONCEPT,
         description="The Frobenius automorphism x -> x^3",
         computational_implementation=lambda a: a ** 3,
-        discovered_names={"specialized_(ff_power_at_1_to_three)"}
+        discovered_names={"specialized_(ff_power_at_1_to_three), matched_(ff_multiply_of_three_elements_indices_[0, 1, 2])"}
     ),
     "ff_twenty_seven_power": GroundTruthEntity(
         canonical_name="ff_twenty_seven_power",
@@ -161,12 +199,13 @@
         discovered_names={"specialized_(ff_multiply_zero_eq_at_1_to_ff_zero)"}
     ),
     "ff_sum_three_times_eq": GroundTruthEntity(
-        canonical_name="ff_sum_three_times_eq_zero",
+        canonical_name="ff_sum_three_times_eq",
         entity_type=EntityType.CONCEPT,
-        description="Sum a finite field element three times is equal to zero",
+        description="Sum a finite field element three times",
         computational_implementation=lambda a, b: a + a + a == b,
         discovered_names={"compose_(ff_sum_three_times_with_ff_eq_output_to_input_map={0: 0})"}
     ),
+    # important for characteristic conjecture
     "ff_sum_three_times_eq_zero": GroundTruthEntity(
         canonical_name="ff_sum_three_times_eq_zero",
         entity_type=EntityType.CONCEPT,
@@ -177,15 +216,16 @@
     "ff_sum_of_three_elements_eq": GroundTruthEntity(
         canonical_name="ff_sum_of_three_elements_eq",
         entity_type=EntityType.CONCEPT,
-        description="Sum of three finite field elements is equal to zero",
-        computational_implementation=lambda a, b, c: a + b + c == b,
+        description="Sum of three finite field elements",
+        computational_implementation=lambda a, b, c, d: a + b + c == d,
         discovered_names={"compose_(ff_sum_of_three_elements_with_ff_eq_output_to_input_map={0: 0})"}
     ),
+    # line towards cap set statement
     "ff_sum_of_three_elements_eq_zero": GroundTruthEntity(
         canonical_name="ff_sum_of_three_elements_eq_zero",
         entity_type=EntityType.CONCEPT,
         description="Sum of three finite field elements is equal to zero",
-        computational_implementation=lambda a, b, c: a + b + c == FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)),
+        computational_implementation=lambda a, b, c,: a + b + c == FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)),
         discovered_names={"specialized_(ff_sum_of_three_elements_eq_at_1_to_ff_zero)"}
     ),
     "ff_is_square": GroundTruthEntity(

frame/environments/FF/conjectures.py

@@ -14,6 +14,12 @@
         description="Frobenius identity for F_27: x^27 = x",
         discovered_names={"forall_(ff_frobenius_identity_predicate_indices_to_quantify_[0])"}
     ),
+    "ff_multiply_one_eq_self": GroundTruthEntity(
+        canonical_name="ff_multiply_one_eq_self",
+        entity_type=EntityType.CONJECTURE,
+        description="Multiplying a finite field element with one is equal to the element itself",
+        discovered_names={"forall_(ff_multiply_one_eq_self_indices_to_quantify_[0])"}
+    ),
     # TODO: Add discovered_names for this conjecture
     "ff_multiplicative_group_cyclic": GroundTruthEntity(
         canonical_name="ff_multiplicative_group_cyclic",

frame/policies/interestingness_guided_policy.py

@@ -221,7 +221,7 @@ def __init__(self,
         # Set simulation limit for SIMULATE_AND_SCORE strategy
         # (default used if not provided)
         action_selection_params = action_selection_params or {}
-        self.simulation_limit = action_selection_params.get('simulation_limit', 3) # TODO(Make this configurable.)
+        self.simulation_limit = action_selection_params.get('simulation_limit', 2) # TODO(Make this configurable.)
         self.action_selection_params = action_selection_params
 
         # We'll store the current graph for interestingness scoring
@@ -480,13 +480,13 @@ def select_action(self, env: MathEnv) -> Optional[ValidAction]:
                 sampled_concepts_map = {}
 
                 if numeric_concepts:
-                    num_to_sample = min(3, len(numeric_concepts))
+                    num_to_sample = min(self.top_k_concepts+1, len(numeric_concepts))
                     numeric_ids, numeric_scores = self._sample_concepts(graph, numeric_concepts, k=num_to_sample)
                     for i, cid in enumerate(numeric_ids):
                         sampled_concepts_map[cid] = numeric_scores[i]
 
                 if ff_concepts:
-                    num_to_sample = min(3, len(ff_concepts))
+                    num_to_sample = min(self.top_k_concepts+1, len(ff_concepts))
                     ff_ids, ff_scores = self._sample_concepts(graph, ff_concepts, k=num_to_sample)
                     for i, cid in enumerate(ff_ids):
                         sampled_concepts_map[cid] = ff_scores[i]

scripts/ff_all_zero_100_episodes.sh

@@ -9,12 +9,12 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
-  experiment.max_steps=100 \
+  experiment.num_episodes=64 \
+  experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \
   z3_usage.use_z3_prover=true \
-  z3_usage.use_z3_example_search=true \
+  z3_usage.use_z3_example_search=false \
   ++policy.params.interestingness_function_path="frame/interestingness/learning/baselines/all_zero.py"
 
 

scripts/ff_hr_applicability_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_comprehensibility_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_equal_weight_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_novelty_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_parsimony_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_productivity_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \

scripts/ff_hr_weighted_by_perf_100_episodes.sh

@@ -9,7 +9,7 @@ cd "$(dirname "$0")/.."
 # Run the experiment with the standard policy config
 poetry run python -m frame.theory_builder \
   --config-name ff_standard_experiment \
-  experiment.num_episodes=100 \
+  experiment.num_episodes=64 \
   experiment.max_steps=1000 \
   experiment.episode_timeout_seconds=120 \
   experiment.num_workers=64 \