{"record":{"id":"93817061cfdbd763","repo":"datawhalechina/hello-agents","slug":"unknown-theorem-name-theorem-name","errorCode":null,"errorMessage":"Unknown theorem name: '{theorem_name}'.","messagePattern":"Unknown theorem name: '(.+?)'\\.","errorType":"exception","errorClass":"Exception","httpStatus":null,"severity":"error","filePath":"Co-creation-projects/BitSecret-GPSAgent/src/gps/symbolic_solver.py","lineNumber":1261,"sourceCode":"            )\n            for goal_id in updated_goal_ids:\n                goal = _anti_parse_fact((self.goals[goal_id][0], self.goals[goal_id][1]))\n                goal = goal + f'({self.status_of_goal[goal_id]})'\n                result.append(goal)\n\n        return '\\n'.join(result)\n\n    def _parse_theorem(self, theorem):\n        try:\n            theorem_name, theorem_paras = parse_fact(theorem.replace(' ', ''))\n        except Exception as e:\n            e_msg = (f\"Error '{repr(e)}' occurred while parsing the theorem '{theorem}'. \"\n                     f\"The theorem format is incorrect.\")\n            raise Exception(e_msg)\n\n        if theorem_name not in self.parsed_gdl[\"Theorems\"]:\n            e_msg = f\"Unknown theorem name: '{theorem_name}'.\"\n            raise Exception(e_msg)\n\n        error_paras = set([char for char in theorem_paras if not char.isupper()])\n        if len(error_paras) > 0:\n            e_msg = (f\"Theorem parameters must be uppercase letters and , only. \"\n                     f\"The current theorem contains invalid characters '{str(error_paras)}'.\")\n            raise Exception(e_msg)\n\n        if len(theorem_paras) != 0 and len(theorem_paras) != len(self.parsed_gdl[\"Theorems\"][theorem_name]['paras']):\n            e_msg = (f\"'{theorem}' has wrong number of parameters \"\n                     f\"(expected {len(self.parsed_gdl[\"Theorems\"][theorem_name]['paras'])}).\")\n            raise Exception(e_msg)\n\n        if len(theorem_paras) == 0:\n            theorem_paras = None\n\n        return theorem_name, theorem_paras\n\n    def apply(self, theorem):","sourceCodeStart":1243,"sourceCodeEnd":1279,"githubUrl":"https://github.com/datawhalechina/hello-agents/blob/606a07d341a47be773fab7f4b71177f53f96b2c3/Co-creation-projects/BitSecret-GPSAgent/src/gps/symbolic_solver.py#L1243-L1279","documentation":"Raised by GPSAgent's symbolic solver in _parse_theorem when the name part of a theorem string (e.g. 'cong_triangle(A,B,C)') does not exist in the loaded GDL theorem dictionary self.parsed_gdl['Theorems']. The solver validates every theorem passed to apply()/decompose() against the theorem database parsed for the current problem, and rejects names it does not know before doing any inference. It is a pure input-validation error, not an inference failure.","triggerScenarios":"Calling solver.apply(theorem) or solver.decompose(theorem) where parse_fact() extracts a name that is misspelled, uses different naming conventions, or belongs to a different problem's GDL file. Spaces are stripped before parsing ('cong triangle(...)' becomes 'congtriangle(...)'), which can silently merge into an unknown name.","commonSituations":"LLM-driven agents hallucinating theorem names not in the current geometry problem's theorem set; copying theorems between problems with different GDL configurations; renaming theorems in the GDL source without updating prompts/tool descriptions.","solutions":["Print or expose sorted(self.parsed_gdl['Theorems'].keys()) and use only those exact names in the theorem string.","Check the spelling of the theorem name; remember leading/trailing spaces are removed but internal spaces are too, so 'isoceles_triangle' vs 'isosceles_triangle' style typos survive to this check.","If the theorem genuinely should exist, verify the correct problem/GDL configuration was loaded and parsed into parsed_gdl before calling apply/decompose."],"exampleFix":"# before\nsolver.apply('cong_triangel(A,B,C,D)')  # misspelled name\n\n# after\nvalid = sorted(solver.parsed_gdl['Theorems'].keys())\nprint(valid)  # pick exact name from this list\nsolver.apply('cong_triangle(A,B,C,D)')","handlingStrategy":"validation","validationCode":"def check_theorem_name(solver, theorem):\n    name = theorem.replace(' ', '').split('(')[0]\n    known = solver.parsed_gdl['Theorems']\n    if name not in known:\n        raise KeyError(f'{name!r} not in {sorted(known)}')\n    return theorem","typeGuard":null,"tryCatchPattern":"try:\n    solver.apply(theorem)\nexcept Exception as e:\n    if str(e).startswith(\"Unknown theorem name\"):\n        # pick from sorted(solver.parsed_gdl['Theorems']) and retry / re-prompt\n        ...","preventionTips":["Expose the theorem list from parsed_gdl['Theorems'] in the agent prompt so only valid names are emitted.","Strip and normalize theorem strings before calling apply/decompose.","Log the unknown name together with the closest known names for fast typo fixing."],"tags":["geometry","symbolic-solver","validation","theorem"],"backgroundTag":null,"analyzedSha":"606a07d341a47be773fab7f4b71177f53f96b2c3","analyzedAt":"2026-08-14T22:57:27.446Z","schemaVersion":2},"datasetVersion":"2026-08-15T22:17:37.221Z"}