神经符号协同的几何问题自动求解：基于 Hello-Agents 与 FormalGeo 的双向推理智能体实战

神经符号协同的几何问题自动求解：基于 Hello-Agents 与 FormalGeo 的双向推理智能体实战

【免费下载链接】hello-agents📚 《从零开始构建智能体》——从零开始的智能体原理与实践教程项目地址: https://gitcode.com/GitHub_Trending/he/hello-agents

导读：本文以《从零开始构建智能体》共创项目 BitSecret-GPSAgent 为主体，深入讲解如何将大语言模型智能体与形式化符号求解器深度融合，构建一个可验证、可追溯的高精度几何定理证明与自动解题系统。读完本文，你将掌握神经符号协同推理的完整架构、"推理—执行—反思—记忆"闭环智能体循环、前向推导与后向目标分解统一的双向符号推理引擎原理，以及从环境配置、LLM 接入到批量并行求解与结果分析的完整实战流程。

一、项目概览：为什么需要"神经符号协同"的几何求解器

几何问题求解对 LLM 而言是一个天然的挑战：纯神经网络推理在长链条几何推导中容易出现幻觉，推导的每一步都缺乏形式化验证；而纯符号求解器（如传统的定理证明器）又缺乏对自然语言题面、几何图形的语义理解能力，难以直接面向真实题目。

BitSecret-GPSAgent（Geometry Problem Solving Agent）正是针对这一矛盾设计的统一神经符号推理框架。它把两种能力各司其职地组织起来：

• 大语言模型作为"规划师"：负责高层次的语义理解、定理选择策略与求解路径的反思修正；
• 符号求解器作为"执行器"：负责形式化验证、严格定理应用与精确代数计算。

两者通过"推理 — 执行 — 反思 — 记忆"的闭环迭代机制协同工作。由于每一步推导都必须经过形式化系统验证，模型产生幻觉的风险从根本上被消除，且每一推导步骤均可验证、可追溯。该框架主要面向高精度几何定理证明与自动解题场景，可应用于教育智能辅导、数学竞赛推理及几何知识验证等任务。

项目源码结构如下（位于Co-creation-projects/BitSecret-GPSAgent/）：

如上图所示，系统整体流水线为：原始问题 → Agentic Parser（形式化解析）→ Agentic Solver（LLM 智能体 + 形式化推理计算引擎）→ Agentic Translator（翻译为人类可读的推理图与求解过程）。其中 LLM 智能体通过工具调用与形式化引擎交互，引擎执行前向/后向推理后回传状态更新，构成闭环。

二、核心功能与技术栈

2.1 三大核心能力

• 神经符号协同推理：LLM 作为"规划师"负责高层次语义理解和路径反思，符号求解器作为"执行器"负责定理的严格验证与精确计算。两者通过"推理 — 执行 — 反思 — 记忆"闭环迭代协同工作，确保每一推导步骤均可验证、可追溯。
• 统一双向符号推理引擎：将前向推理（从已知条件推导结论）与后向推理（从目标分解子目标）完整统一的符号求解引擎。每个定理均被定义为可逆操作：前向用于生成新事实，后向用于分解目标。系统同时从两个方向搜索，并在中间状态相遇时终止，相比单向搜索具有指数级的复杂度优势。
• 开箱即用：不依赖任何问题特定的标注数据即可直接运行于个人笔记本电脑，支持多种主流 LLM 作为后端，并提供完整的工具调用接口（定理应用、目标分解、事实查询、状态检查等），方便开发者快速集成与二次开发。

2.2 技术栈

• 使用Hello-Agents API实现 Reflection + ReAct + Plan-and-Solve 融合的智能体框架（即本项目所在《从零开始构建智能体》教程的配套实现）；
• FormalGeo形式化系统与求解器：定义了几何结构谓词、实体、关系、属性与定理五层形式化体系；
• 符号计算库SymPy：负责代数方程组的求解与符号运算。

依赖清单见 requirements.txt，核心包括openai==2.21.0、sympy==1.14.0、func-timeout==4.3.5、hello-agents==1.0.0、matplotlib、numpy、dotenv等。

三、形式化系统基础：读懂求解器"语言"

要使用这套框架，必须先理解 FormalGeo 形式化系统定义的 5 种概念。它们共同构成了求解器内部的"世界模型"：

3.1 几何结构谓词（拓扑结构）

描述几何图形的拓扑结构信息，共三种：

• Shape(*)：描述由线或弧依次逆时针构成的图形。如Shape(AB,BC,CA)描述三角形 ABC；Shape(AB,BC)描述角 ABC；Shape(PA,OAB,BP)描述扇形（P 是圆心，O 是圆）。
• Collinear(*)：描述按顺序排列的共线点，如Collinear(ABC)表示点 A、B、C 共线。
• Cocircular(*)：描述逆时针排列的共圆点，如Cocircular(O,XYZ)表示点 X、Y、Z 在圆 O 上且按逆时针顺序。

3.2 实体（拓扑结构细化）

求解器识别上述 3 种结构谓词后，会自动扩展出 11 种实体：Point(A)、Line(A,B)、PointOnLine(M,A,B)、Angle(A,B,C)、Triangle(A,B,C)、Quadrilateral(A,B,C,D)、Circle(O)、PointOnCircle(A,O)、DoublePointsOnCircle(A,B,O)、TriplePointsOnCircle(A,B,C,O)、QuadruplePointsOnCircle(A,B,C,D,O)。

实体在求解器中的作用是描述拓扑结构信息，并在添加关系时执行实体存在性检查（EE check）。例如添加关系RightTriangle(A,B,C)时，会检查Triangle(A,B,C)是否存在，若不存在则检查不通过。此外，系统中用点的逆时针顺序表示几何图形：对Triangle(A,B,C)，(B,C,A)与(C,A,B)均合法，但(C,B,A)表示另一种镜像对称的拓扑结构。这一约定在应用镜像对称（定理名中含 mirror）三角形的相似/全等定理时尤为重要，例如MirrorCongruentBetweenTriangle(A,B,C,D,E,F)表示三角形 ABC 和 DEF 镜像相似，点对应关系为 A→D、B→F、C→E。

3.3 关系与实体存在性检查

关系描述实体之间的关系，其参数格式与所需的实体存在性检查在 README 中给出完整清单（节选）：

3.4 属性（定量描述）

属性是几何实体和关系某一性质的定量描述，如角的大小、线的长度等，使用符号表示，例如AOB.ma表示角 AOB 的角度、AB.ll表示线 AB 的长度。完整属性定义包括：

• 三角形：LengthOfLine(A,B):ll、MeasureOfAngle(A,B,C):ma、PerimeterOfTriangle:pt、AreaOfTriangle:at、HeightOfTriangle:ht、相似比rst/rmt；
• 四边形：pq、aq、hq、rsq/rmq；
• 圆与弧：LengthOfArc:la、MeasureOfArc:mar、RadiusOfCircle:rc、DiameterOfCircle:dc、PerimeterOfCircle:pc、AreaOfCircle:ac、PerimeterOfSector:ps、AreaOfSector:as。

3.5 定理（推理规则）

定理定义了关系之间的推理过程，由前提和结论构成：前提是"关系 + 逻辑连接词"构成的逻辑表达式，结论是某个关系。例如平行线传递性：

parallel_judgment_par_par(A,B,C,D,E,F): ParallelBetweenLine(A,B,C,D) & ParallelBetweenLine(C,D,E,F) -> ParallelBetweenLine(A,B,E,F)

应用定理时求解器自动进行字符替换：若应用parallel_judgment_par_par(A,B,M,N,X,Y)，求解器会检查ParallelBetweenLine(A,B,M,N) & ParallelBetweenLine(M,N,X,Y)是否成立，成立则把ParallelBetweenLine(A,B,X,Y)加入已知条件。

形式化系统中定义的定理覆盖了平行线判定与性质、垂直平分线、角平分线、三角形内角和、周长面积公式、中位线、重心、全等/相似三角形（含镜像形式）、勾股定理及其逆定理、特殊角直角三角形、等腰/等边三角形、平行四边形/矩形/菱形/筝形/梯形判定与性质、圆幂定理、圆心角/圆周角、切线、扇形面积等大量定理。这些定理均通过 utils.py 中的_parse_one_theorem与_get_gpl解析成可执行的 GPL（几何前提列表）结构，供求解器前向应用与后向分解使用。

四、智能体工具集：LLM 与求解器的交互接口

系统为 LLM 定义了 6 种工具，实现与求解器的交互（对应 symbolic_solver.py 中的apply、decompose、find_fact、find_goal、check方法，以及 agent_loop.py 中的工具分发逻辑）：

1.apply(theorem)— 前向应用定理

尝试应用一条定理扩展已知条件，并返回应用结果。例如应用平行线传递性可写为apply(parallel_judgment_par_par())，推理器会自动组合所有相关前提得到对应结论。成功应用后返回新添加的条件；失败则返回失败原因（如某个前提不存在）；也可能返回报错信息（如定理未定义）。

注意：部分定理必须使用带参数形式，包括bisector_of_angle_property_line_ratio、right_triangle_property_pythagorean、circle_property_circular_power_chord_and_chord、circle_property_circular_power_tangent_and_segment_line、circle_property_circular_power_segment_and_segment_line，以及求解周长（perimeter）和面积（area）相关的定理、相似（similar）的判定和性质定理、全等（congruent）的判定和性质定理。例如求解三角形 ABC 的面积需调用apply(triangle_area_formula_common(A,B,C))。除这些定理外，强烈建议使用定理的无参模式（由求解器自动枚举参数组合）。这一约束与源码中 symbolic_solver.py 的special_theorem集合以及apply中的参数检查逻辑完全对应。

2.decompose(theorem)— 后向分解目标

将定理的结论分解为其前提（子目标）。例如decompose(parallel_judgment_par_par(A,B,M,N,X,Y))：若存在目标ParallelBetweenLine(A,B,X,Y)，推理器会将其分解为ParallelBetweenLine(A,B,M,N)和ParallelBetweenLine(M,N,X,Y)两个子目标。与apply不同，decompose只能使用带参数形式。源码中decompose方法在theorem_paras is None时会直接抛出ValueError（见 symbolic_solver.py）。

3.find_fact(relation_type)— 查询已知条件

返回所有种类为 relation 的条件。例如find_fact(ParallelBetweenLine)可能返回(A,B,C,D), (C,D,E,F)等。若关系未定义则报错。当查询Eq类型时，求解器会返回按变量是否相交分组的代数方程组以及所有已求解出值的变量（对应源码find_fact中针对Eq的特殊分支）。

4.find_goal(relation_type)— 查询求解目标

返回所有种类为 relation 的目标及其状态（0 待求解 / 1 已求解 / -1 不可能实现）。例如find_goal(ParallelBetweenLine)可能返回(A,B,X,Y)。

5.check()— 校验求解状态

返回当前几何问题的目标是否被成功求解，用于判断求解过程是否终止。特别要注意：只有check()的返回结果才可以作为求解过程是否终止的依据——解题过程必须经过形式化系统的验证。对应源码中check()方法：初始目标状态为 1 时返回"求解成功，需要调用 finish() 结束"。

6.finish()— 结束求解

当调用check()确认目标已求解后，简单总结求解过程并调用finish()结束。

7. 隐藏工具：summarize— 记忆压缩

在 agent_loop.py 中还存在一个summarize工具：当上下文长度超过max_context阈值时，系统会向 LLM 注入 summarize 提示词，要求其总结当前进度，然后Agent.summarize()将历史对话保存到history，仅保留 system 提示与总结内容，从而压缩工作记忆、支持超长推理链。这也对应了项目简介中"推理 — 执行 — 反思 —记忆"闭环中的记忆环节。

五、环境配置与快速开始

5.1 数据准备

项目不依赖问题特定的标注数据进行推理，但需要下载包含 7000 道形式化几何题目的数据集和日志（问题编号范围 1–7000）。从项目 README 中提供的公开云盘链接（Google Drive 或百度网盘）下载数据集与日志，解压到项目目录后，目录结构应如下所示：

BitSecret-GPSAgent/ |--datasets/ | |--diagram/ | |--ggbs/ | |--problems/ | |--summarize_prompt.txt | |--system_prompt.txt | └──gdl.json | |--outputs/ | |--agent/ | |--log/ | |--fig-statistics.pdf | └──tab-main_results.txt | |--src/ | └──gps/ | |--agent_loop.py | |--chart.py | |--symbolic_solver.py | └──utils.py | |--.env |--architecture.png |--requirements.txt └──README.md

其中gdl.json是形式化系统的定义文件（几何领域语言），problems/下每个{problem_id}.json是一个形式化题目，system_prompt.txt与summarize_prompt.txt是提示词模板。系统提示词由 agent_loop.py 中的get_system_prompt动态生成：读取模板后，将gdl.json中的关系定义、属性符号、可用定理（通过get_theorems()过滤出测试集实际用到的定理）分别替换到{relation}、{attribution}、{theorem}占位符中。

5.2 创建环境并安装依赖

项目要求 Python 3.12（README 与 Notebook 均标注python=3.12.12），执行：

$ conda create -n GPSAgent python=3.12.12 $ conda activate GPSAgent $ pip install -r requirements.txt

5.3 配置 LLM 后端（.env）

运行agent_loop.py之前，需在src/gps目录下添加.env文件（源码通过dotenv.load_dotenv()加载），并配置以下参数：

Deepseek_BASE_URL="https://api.deepseek.com" Deepseek_API_KEY="your_api_key" Deepseek_MODEL_ID="deepseek-v4-pro"

如果想使用其他基础模型，例如 Qwen（百炼平台），可在.env中添加：

BaiLian_BASE_URL="https://dashscope.aliyuncs.com/compatible-mode/v1" BaiLian_API_KEY="your_api_key" BaiLian_MODEL_ID="qwen3.6-plus"

同时修改agent_loop.py中main函数的参数model_names=['BaiLian']。每个模型名称对应一个进程——从源码看，多进程机制在 agent_loop.py 的multiprocess_solve中实现：主进程将题目放入task_queue，为model_names中的每个模型各启动一个multiprocessing.Process，各进程通过环境变量${model_name}_API_KEY、${model_name}_BASE_URL、${model_name}_MODEL_ID读取自己的凭据与模型 ID。因此可以配置多个模型名称实现并行，例如model_names=['Deepseek', 'Deepseek', 'BaiLian']会启动 3 个进程。

5.4 运行求解器

$ cd src/gps $ python agent_loop.py

程序会打印几何问题求解过程与 Agent 交互历史（debug_mode=True时输出带图标的详细日志，如 System/User/Assistant/Tool 各角色消息，见Agent.add_memory中的彩色打印逻辑）。

六、使用示例：main 函数参数详解

通过 main.ipynb 或直接调用agent_loop.py中的main函数，可以灵活控制求解过程。完整参数如下：

from agent_loop import main main( test_pids=[1, 2, 3], # 要运行的题目列表，范围 1-7000 log_path="../../outputs/log/log_pssr_agent.json", # 保存日志的地址 model_names=['Deepseek'], # 要使用的 LLM（每个名称对应一个进程） max_epoch=50, # 单个问题与 LLM 的最大交互次数 max_context=80000, # 单个问题最大上下文长度（超过后触发 summarize） solve_again=True, # 为 True 时，若问题求解不成功，再次运行依然尝试求解 debug_mode=True # 为 True 时输出对话交互历史 )

各参数在源码 agent_loop.py 中的行为：

• test_pids：题目 ID 列表。main会先加载log_path中已有的日志，跳过已求解/已尝试的题目，并random.shuffle打乱顺序后放入任务队列。
• log_path：JSON 日志文件路径，记录{"total": ..., "solved": {...}, "unsolved": {...}, "timeout": {...}, "error": {...}}四类结果，每个题目记录epoch与timing。保存时采用先写.bk备份再替换的方式（见utils.save_json）。
• model_names：模型列表，每个模型名称启动一个子进程从任务队列取题求解。
• max_epoch：单个题目的最大交互轮次。超出后判定为timeout（超时），Agent.run中还有一个独立的内部重试机制：单次模型调用异常时会等待time_sleep秒重试，最多尝试max_epoch次。
• max_context：上下文长度上限（按字符数累计，见Agent.context_length）。超过后向 LLM 注入 summarize 提示词进行记忆压缩。
• solve_again：为 True 时清空日志中unsolved/timeout/error记录，允许再次尝试；为 False 时保留记录并跳过。
• debug_mode：为 True 时设置全局debug标志，打印完整交互历史与求解过程。

求解结束后，每个题目的完整对话历史会保存到outputs/agent/solving_history_{problem_id}.json，包含timing、model_name与多轮history，供后续统计分析使用。

七、LLM 求解循环：ReAct 风格的工具调用协议

LLM 与求解器的交互遵循严格的 JSON 输出协议。系统提示词要求模型每次输出：

{ "thinking": "你的思考过程和下一步计划", "action": "你希望调用的工具" }

其中thinking是思考过程与下一步计划，action是严格按照格式调用的工具。以下是系统提示词给出的 7 个输出示例模式：

从源码 agent_loop.py 的parse_response可以看出工具调用的解析逻辑：response['action']按第一个(切分为工具名与参数，tool_name == 'summarize'时参数取自thinking字段，其余工具去掉末尾)。随后主循环（solve函数）将工具名分发到求解器的对应方法，把执行结果作为 user 消息回填给 LLM，形成"模型思考 → 工具调用 → 状态更新 → 再思考"的 ReAct 闭环；当solver.status_of_goal[0] == 1时自动注入"检测到问题已求解，自动结束"，退出循环并判定结果为solved。

八、完整输出示例：一道全等三角形题的求解全记录

README 中给出了一个完整的实际求解输出（JSON 日志），展示了上述闭环的真实运行过程。题目为两个全等三角形 RST 与 XYZ，已知：

• 结构：Shape(RS,ST,TR), Shape(XY,YZ,ZX)
• 条件：CongruentBetweenTriangle(R,S,T,X,Y,Z)、Eq(TR.ll-x-21)、Eq(ZX.ll-2*x+14)、Eq(TRS.ma-4*y+10)、Eq(ZXY.ma-3*y-5)
• 目标：Eq(y-15)

求解过程如下：

第 1 轮——LLM 规划：利用全等三角形性质得到对应边、对应角相等。选择congruent_triangle_property_line_equal(S,T,R,Y,Z,X)（此时 BC 边为 TR、EF 边为 ZX，正好对应）：

action: apply(congruent_triangle_property_line_equal(S,T,R,Y,Z,X))

执行结果：

新推导出的条件： Eq(TR.ll-ZX.ll) Eq(TR.ll-56) Eq(ZX.ll-56) Eq(x-35)

第 2 轮——LLM 规划：用congruent_triangle_property_angle_equal得到角 TRS 等于角 ZXY：

action: apply(congruent_triangle_property_angle_equal(R,S,T,X,Y,Z))

执行结果：

新推导出的条件： Eq(TRS.ma-ZXY.ma) Eq(TRS.ma-50) Eq(ZXY.ma-50) Eq(y-15) 部分目标的状态更新为（括号内数字表示目标状态，0表示此目标待求解，1表示此目标已求解，-1表示此目标不可能实现）： Eq(y-15)(1)

收尾——系统检测到目标已求解：检测到问题已求解，自动结束。，最终日志记录求解结束：成功✅，并附上总耗时timing与模型名model_name。

这个例子直观展示了三个要点：其一，LLM 需要理解定理参数的"旋转对应"关系（(S,T,R,Y,Z,X)而非(R,S,T,X,Y,Z)），这考验语义理解与规划能力；其二，每一步推导都被求解器形式化验证，代数方程（如Eq(TR.ll-56)与Eq(ZX.ll-56)合并解出x=35）由 SymPy 自动完成；其三，目标状态Eq(y-15)(1)由求解器严格判定，LLM 无权自行宣告"已解出"，幻觉被结构性杜绝。

九、源码级原理：双向符号推理引擎如何工作

9.1 状态表示与构建流程

SymbolicSolver（symbolic_solver.py）在初始化时维护了完整的形式化状态：

• 前向结构：facts（事实表，记录(谓词, 实例, 前提ID集合, 操作ID)）、fact_id（事实去重索引）、predicate_to_fact_instances（按谓词索引事实）；
• 后向结构：goals（目标表，记录(谓词, 实例, 父目标ID, 操作ID)）、status_of_goal（0 待求解 / 1 已求解 / -1 不可能实现）、sub_operations（子目标操作树）；
• 共享结构：operations（所有操作：Preset/Apply/Decompose）、operation_groups（按操作分组的事实/目标）、theorem_instances（定理实例）；
• 代数系统：points（坐标）、sym_to_value（已解变量）、sym_to_sym/sym_to_syms（多重形式符号统一）、equations（按变量相交分组的方程组）、simplified_algebraic_goal（代数目标）、solved_target_cache与attempted_equations_cache（求解缓存，避免重复计算）。

_construct方法（symbolic_solver.py）按以下步骤初始化一个问题：

1. 初始化谓词索引（Presets 与 Relations，Eq特殊处理）；
2. 添加构造性 CDL（construction_cdl）为初始事实；
3. 记录各点坐标；
4. 拓扑扩展（约 300 行，是框架的精华之一）：从Collinear扩展点/线/PointOnLine；从Cocircular扩展圆、点圆关系与多重共圆点关系；对Shape执行"拼图式"组合（jigsaw），将相邻的线段/弧逐步合并为更大的多边形，同时进行"无环（no ring）"、"无洞（no holes）"、"共线点合并"等合法性检查；对角度执行相邻角组合扩展；最终把扩展出的实体统一注册为扩展事实；
5. 添加关系型 CDL（relation_cdl，来自 text_cdl + image_cdl），逐条通过几何约束检查（EE check）；
6. 设置目标（goal_cdl），并对代数目标做GoalAutoExpand自动分解。

这一拓扑扩展机制意味着：只要给出最基础的Shape/Collinear/Cocircular结构，求解器就能自动推导出所有隐含的三角形、四边形、角度等实体，LLM 无需关心底层实体枚举。

9.2 前向推理：定理应用与代数求解联动

apply(theorem)（symbolic_solver.py）分两种模式：

• 带参数模式：直接校验各前提是否在fact_id中，通过后生成Apply操作并添加结论事实；
• 无参模式：通过_run_gpl对定理的 GPL（前提列表）执行受约束的笛卡尔积枚举——为每个"产品谓词"遍历predicate_to_fact_instances中所有实例，按"固有相同索引"与"互相同一索引"约束剪枝，再逐条校验几何前提、代数前提与代数约束，最终枚举出所有可应用的定理实例并逐一添加结论。

添加Eq类型事实时，_add_fact会触发代数子系统：用已解变量替换符号、合并共享变量的方程组、调用 SymPy 的nonlinsolve求解（带func_timeout超时保护，默认 5 秒），过滤负数/无数值解后，将唯一解回写为新的Eq事实，并同步更新受影响的代数目标（simplified_algebraic_goal中依赖相同变量的目标）。

9.3 后向推理：目标分解与状态传播

decompose(theorem)（symbolic_solver.py）的工作流：

1. 解析定理参数（必须带参），根据结论实例化目标；
2. 依次通过代数约束检查与几何实体存在性检查；
3. 通过_find_father_ids找到当前所有待求解的同名目标（status_of_goal == 0）作为父节点；
4. 通过_generate_sub_goals把定理前提（几何前提 + 代数前提）构造成子目标，_add_goals将其挂到父目标下（同时做"不能是祖先目标"的防环检查）；
5. 调用_check_goals检查新子目标是否已被事实满足。

_set_status（symbolic_solver.py）实现了目标状态的三态传播：目标求解（1）时向上检查同操作组的兄弟目标是否全部求解，全部求解则向上层传播；目标不可能（-1）时横向传播给所有兄弟、向下传播给所有子目标。当一个后向分解出的子目标恰好被某个已知事实满足时，求解器会在"相遇点"自动反向应用定理生成结论——这正是 README 所述"系统同时从两个方向搜索，并在中间状态相遇时终止"的实现基础。

9.4 可验证性与输出

check()仅依据status_of_goal[0]判定初始目标是否完成；state()负责把求解器内部状态序列化为供 LLM 阅读的自然语言描述（结构信息、初始条件、目标状态、实体、已知条件、代数方程组分组、目标树）。所有反馈字符串中的目标状态均标注(0/1/-1)，确保 LLM 与人类都能精确感知每一步的形式化进展。

十、实验结果分析与统计可视化

运行求解后，可使用 chart.py 生成论文级统计图表（fig-statistics.pdf）与主结果表格（tab-main_results.txt）。该模块提供三类统计：

• 按难度分级的平均上下文长度（get_avg_context_len）：问题难度由theorem_seqs长度映射（>12 条定理为 Level 6，否则按int(len/2)+len%2分 1–5 级），分别统计已求解问题与其他问题；
• 按难度分级的平均交互轮次（get_avg_epoch）：从日志的epoch字段统计；
• 按难度分级的平均工具调用次数（get_tool_call）：解析每条 assistant 消息的action字段，统计apply、decompose、find（含 find_fact/find_goal）、check、error五类调用，其中 JSON 解析失败计为 error——这也是评估 LLM 输出格式规范性的一项代理指标。

draw_figure将三类指标绘制为"发散柱状图 + 双折线"组合图：每个难度级别下，向下柱为已求解问题的工具调用均值、向上柱为未求解问题的均值，折线分别叠加已解决/未解决的平均上下文长度与平均轮次。draw_table则汇总包括神经求解器、神经符号求解器与纯符号求解器在内的多方法对比表（各方法数据来自outputs/log/下的不同日志文件），输出 LaTeX 兼容格式。Note: 表格中涉及的具体对比数值来自outputs/log/中预设的日志文件，实际数值以你下载并运行后生成的结果为准，不要将其视为本文的实测结论。

十一、常见问题与调优建议

• 模型调用失败/返回空：Agent.run内置重试机制，空响应不计入调用次数（max_epoch += 1）；可调整time_sleep控制重试间隔。
• 上下文过长：调低max_context会更早触发 summarize 记忆压缩；调高则保留更多细节但增加 token 成本。实测可通过chart.py的按难度平均上下文长度统计来权衡。
• 求解超时/失败：max_epoch限制总交互轮次；solve_again=True允许后续重新尝试未解出的题目。可从outputs/agent/solving_history_{pid}.json回溯失败原因（是工具调用格式错误、定理选择失当还是上下文不足）。
• 多进程提速：model_names=['Deepseek', 'Deepseek', 'BaiLian']可启动 3 个进程并行；注意各模型需在.env中分别配置_BASE_URL、_API_KEY、_MODEL_ID三件套。
• 定理参数规则：牢记"周长/面积/相似/全等"类定理必须带参数，其余优先用无参模式让求解器自动枚举，可显著降低 LLM 的输出难度。

结语

BitSecret-GPSAgent 展示了"神经 + 符号"融合的一种极具工程价值的范式：LLM 负责"想"，符号求解器负责"证"，每一步都有形式化系统的背书。通过 Hello-Agents 提供的智能体 API 与 FormalGeo 的完备定理库，这套框架在不依赖问题特定标注数据的前提下即可在个人笔记本上运行，且天然支持多模型并行与完整的求解轨迹审计。无论你是研究几何自动推理、构建教育辅导智能体，还是想借鉴神经符号协同的 Agent 架构，这个项目都提供了从原理到代码的完整参考实现。更详细的架构、提示词模板与数据集说明，可继续阅读 README.md 与 main.ipynb，并深入探索 symbolic_solver.py 中的前向/后向引擎实现。

【免费下载链接】hello-agents📚 《从零开始构建智能体》——从零开始的智能体原理与实践教程项目地址: https://gitcode.com/GitHub_Trending/he/hello-agents