from __future__ import annotations import copy import pytest from gap_pipeline.models import CanonicalItem @pytest.fixture def item() -> CanonicalItem: return CanonicalItem( item_id="demo-A-1", problem=r"Let \(a>0\). Prove that \(a+1/a\ge 2\).", solution=( r"Since \((a-1)^2\ge0\), expanding gives \(a^2-2a+1\ge0\). " r"Divide by \(a>0\) to obtain \(a+1/a\ge2\)." ), variables=["a"], problem_type="proof", ) @pytest.fixture def dag_dict() -> dict: return { "nodes": [ { "node_id": "n1", "claim": "(a-1)^2 >= 0", "derivation": "a square is nonnegative", "dependencies": [], "source_span": "Since (a-1)^2 >= 0", "mathematical_objects": ["a", "(a-1)^2"], }, { "node_id": "n2", "claim": "a+1/a >= 2", "derivation": "expand and divide by positive a", "dependencies": ["n1"], "source_span": "Divide by a>0", "mathematical_objects": ["a"], }, ], "terminal_node_id": "n2", } @pytest.fixture def plan_dict() -> dict: return { "steps": [ { "node_id": "n1", "method_label": "use nonnegativity of a square", "input_roles": ["positive scalar"], "output_role": "nonnegative expression", "invariants": ["scalar is real"], }, { "node_id": "n2", "method_label": "expand and divide by a positive quantity", "input_roles": ["nonnegative expression", "positive scalar"], "output_role": "target inequality", "invariants": ["divisor is positive"], }, ], "terminal_node_id": "n2", } @pytest.fixture def replacement_dict() -> dict: return { "target_node_id": "n1", "original_object": "(a-1)^2", "replacement_object": "(x-2)^2", "guard_conditions": ["x>0"], "guard_evidence": ["choose x in the positive reals"], "expected_downstream_changes": ["expand around 2", "divide by x"], "rationale": "the same square-nonnegativity plan applies", } @pytest.fixture def diffused_dict(plan_dict: dict) -> dict: return { "node_instantiations": [ { "node_id": "n1", "method_label": plan_dict["steps"][0]["method_label"], "instantiated_claim": "(x-2)^2 >= 0", "instantiated_derivation": "a square is nonnegative", "dependencies": [], }, { "node_id": "n2", "method_label": plan_dict["steps"][1]["method_label"], "instantiated_claim": "x+4/x >= 4", "instantiated_derivation": "expand and divide by positive x", "dependencies": ["n1"], }, ], "regenerated_proof": ( "Since (x-2)^2 >= 0, expand and divide by x>0 to get x+4/x >= 4." ), "terminal_answer": "x+4/x >= 4", } @pytest.fixture def candidate_dict(replacement_dict: dict, diffused_dict: dict) -> dict: return { "problem": "Let x>0. Prove that x+4/x >= 4.", "proof": diffused_dict["regenerated_proof"], "terminal_answer": diffused_dict["terminal_answer"], "node_instantiations": diffused_dict["node_instantiations"], "replacement": replacement_dict, } def changed_candidate(candidate: dict, suffix: str) -> dict: value = copy.deepcopy(candidate) value["problem"] = value["problem"] + f" [{suffix}]" value["proof"] = value["proof"] + f" Repair {suffix}." return value