diff --git a/frame/environments/FF/calculations.py b/frame/environments/FF/calculations.py index b75f6c0..a49c111 100644 --- a/frame/environments/FF/calculations.py +++ b/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( diff --git a/frame/environments/FF/conjectures.py b/frame/environments/FF/conjectures.py index cef0fde..26ee57e 100644 --- a/frame/environments/FF/conjectures.py +++ b/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", diff --git a/frame/policies/interestingness_guided_policy.py b/frame/policies/interestingness_guided_policy.py index 5a82ca2..007d448 100644 --- a/frame/policies/interestingness_guided_policy.py +++ b/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] diff --git a/scripts/ff_all_zero_100_episodes.sh b/scripts/ff_all_zero_100_episodes.sh index 05817d0..945aebc 100755 --- a/scripts/ff_all_zero_100_episodes.sh +++ b/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" diff --git a/scripts/ff_hr_applicability_100_episodes.sh b/scripts/ff_hr_applicability_100_episodes.sh index aaa6055..6d541de 100755 --- a/scripts/ff_hr_applicability_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_comprehensibility_100_episodes.sh b/scripts/ff_hr_comprehensibility_100_episodes.sh index 1c9d9cf..4866374 100755 --- a/scripts/ff_hr_comprehensibility_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_equal_weight_100_episodes.sh b/scripts/ff_hr_equal_weight_100_episodes.sh index 04ab387..0c22518 100755 --- a/scripts/ff_hr_equal_weight_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_novelty_100_episodes.sh b/scripts/ff_hr_novelty_100_episodes.sh index 9e1c602..7067b14 100755 --- a/scripts/ff_hr_novelty_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_parsimony_100_episodes.sh b/scripts/ff_hr_parsimony_100_episodes.sh index fc5ea47..c3a555c 100755 --- a/scripts/ff_hr_parsimony_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_productivity_100_episodes.sh b/scripts/ff_hr_productivity_100_episodes.sh index 3a9c779..9ec0c6d 100755 --- a/scripts/ff_hr_productivity_100_episodes.sh +++ b/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 \ diff --git a/scripts/ff_hr_weighted_by_perf_100_episodes.sh b/scripts/ff_hr_weighted_by_perf_100_episodes.sh index 4ab22ef..9304f33 100755 --- a/scripts/ff_hr_weighted_by_perf_100_episodes.sh +++ b/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 \