Agent 的计划可执行性检查器：约束表达与静态验证思路
·
Agent 的计划可执行性检查器：约束表达与静态验证思路
引言
各位开发者、架构师、AI 应用落地工程师们，大家好！我是在科技行业摸爬滚打了15年的架构师兼技术博主老王。最近半年多前，我在一家自动驾驶初创公司负责边缘智能驾驶行为规划的AI Agent 落地项目踩了个超级大的坑——
我们开发了一个基于 LLM + 工具链的城市物流无人车决策 Agent：白天它是快递员小李子，会规划取件→绕行堵车→送件→充电的完整计划链，一切看起来都美好得像童话；但上线第一天凌晨四点，监控室里突然传来“无人车停在高架桥下充电了！”的警报——
我们复盘日志发现：无人车规划了一个取件点A（高度2.2米的快递柜）→ 绕行点B（需要通过一条限高2.5米的市政隧道（无人车本身高度2.8米）→ 充电点C（有足够空间）的路径，**LLM 生成的计划完全忽略了无人车的物理尺寸与隧道的硬性限高约束！
更糟糕的是，计划执行时的动态检查模块完全依赖感知系统——而那天凌晨市政隧道口的标识牌被大货车撞歪了，感知系统没识别到，就这么硬闯了进去……卡在隧道口进退不得，直到凌晨五点我们拖车把它救出来，还赔了市政部门的清理费。
这件事让我深刻意识到：对于有强物理环境约束、安全敏感、资源受限的 AI Agent 应用场景，完全依赖 LLM 生成计划、或只依赖动态检查模块事后发现问题、或依赖动态执行时的感知反馈，都是“拿系统稳定性和用户信任开玩笑”。
我们真正需要的，是一个在Agent 计划生成之后、正式执行之前，就能够对计划的所有可量化、可形式化的约束条件进行快速、严谨、无遗漏的静态验证的工具——也就是我们今天要聊的 Agent 的计划可执行性检查器（Agent Plan Executability Checker, APEC）。
核心概念
问题背景
1. 从“LLM 生成即执行”到“多步验证即落地”
在过去的两年里，AI Agent 经历了从“玩具阶段”到“落地尝试阶段”的巨大转变：
- 玩具阶段（2022-2023Q3）：Agent 主要是用 LLM 调用 Google 搜索、写邮件、订机票这些“软约束、低风险、容错率高”的场景，LLM 生成错了大不了重试一次就行，没人在乎。
- 落地尝试阶段（2023Q4至今）：越来越多的 Agent 开始进入硬约束、高风险、容错率极低甚至为零的场景：
- **自动驾驶/无人配送无人车：物理尺寸、限高限宽、电池电量、交通规则、配送时效
- **工业机器人控制：机械臂自由度、负载能力、安全围栏位置、操作顺序、安全距离、能耗
- **金融交易风控：交易金额限制、风险敞口、监管合规、合规规则、交易时段
- **医疗辅助诊断：检查顺序、检查设备可用性、患者生理参数、合规检查设备使用条件
- **云资源编排成本优化：预算约束、实例规格限制、可用区、依赖关系
- **太空探测器任务规划：轨道参数、燃料限制、通信窗口、操作顺序、负载能力
在这些场景下，“玩具阶段的“LLM 生成即执行”“动态发现错误再重试”的模式完全行不通了——重试一次的成本可能是几百万、几千万甚至是生命代价。
2. 动态验证的局限性
很多团队可能会说：“我们加了动态检查模块啊！执行每一步都检查一遍不就行了？”
是的，动态检查确实能解决一部分问题，但它有三个致命的局限性：
- 事后诸葛亮： 问题往往是在计划执行了几步之后才发现的，这时候已经浪费了时间、资源甚至造成了不可逆的后果（比如我们开头说的无人车已经开到隧道口进退不得）。
- 依赖外部数据/感知系统： 外部数据可能不准确、感知系统可能失效（比如开头说的标识牌被撞歪了），这时候动态检查就变成了“瞎子摸象”。
- 效率低下： 对于长计划链的动态检查往往需要调用外部 API/传感器，耗时较长，无法满足实时性要求极高的场景（比如自动驾驶需要在毫秒级内完成路线调整后的计划验证）。
3. 静态验证的优势与机遇
静态验证（Static Verification）是一种在不执行计划的情况下，通过形式化方法、约束求解、符号执行等技术手段，对计划的可执行性进行验证的方法。它的优势在于：
- 事前验证： 在计划执行之前就发现问题，完全避免了“事后诸葛亮”的尴尬。
- 不依赖外部数据/感知系统： 只依赖 Agent 自身的模型参数、环境的先验约束知识库、计划的语义结构，不依赖任何外部输入。
- 效率极高： 静态验证通常是纯逻辑运算，不需要调用外部 API/传感器，耗时可以控制在毫秒级甚至微秒级。
- 无遗漏： 形式化方法可以保证对所有可能的情况进行验证，不会出现“漏检”的情况。
近年来，随着约束规划（Constraint Programming, CP）、满足性模理论（Satisfiability Modulo Theories, SMT）、自动规划（Automated Planning, AP）、大语言模型结构化输出（Structured Output from LLMs） 等技术的成熟，Agent 的计划可执行性静态验证终于从“理论研究”阶段进入了“工程落地”阶段——也就是我们今天要聊的 APEC 的核心机遇。
问题描述
我们先给 Agent 的计划可执行性检查器（APEC） 下一个清晰、严谨、可工程化的定义：
**APEC 是一个独立的、可插拔的软件组件，它接收三个输入：
- Agent 模型库（Agent Model Library, AML）：包含 Agent 自身的所有可量化、可形式化的属性（比如无人车的高度、宽度、载重量、电池容量、最大续航里程、最大速度等）。
- 环境约束知识库（Environment Constraint Knowledge Base, ECKB）：包含 Agent 运行环境的所有可量化、可形式化的约束（比如市政隧道的限高限宽、交通规则、充电点的位置、可用时间、充电桩类型等）。
- 结构化 Agent 计划（Structured Agent Plan, SAP）：由大语言模型或自动规划器生成的、具有明确语义结构的计划（比如有序的动作序列、分支计划、循环计划、并行计划等）。
它的输出是一个可执行性验证报告（Executability Verification Report, EVR）：
- 验证结果（Pass/Fail）：计划是否满足所有约束条件。
- 失败原因列表（Failure Reason List, FRL）：如果验证失败，列出所有违反的约束条件、违反的位置（在计划中的动作序列中的哪一步或哪几步）、违反的严重程度（Critical/High/Medium/Low）、建议的修复方案（Suggested Fixes）。
- 约束满足度（Constraint Satisfaction Rate, CSR）：计划满足所有约束条件的百分比。
- 优化建议（Optimization Suggestions）：即使验证通过，也会给出一些优化计划的建议（比如缩短配送路径、减少电池消耗、降低风险敞口等）。**
接下来，我们用一个具体的问题实例来描述 APEC 需要解决的问题：
问题实例：城市物流无人车配送计划验证
我们先定义三个输入：
1. Agent 模型库（AML）
我们的无人车“快递员小李子”的 AML 如下（我们用 JSON 格式来表示，因为 JSON 是结构化输出的常用格式，也方便后续的代码实现）：
{
"agent_id": "courier_001",
"agent_type": "urban_logistics_drone_truck",
"attributes": {
"physical_dimensions": {
"height_m": 2.8,
"width_m": 1.5,
"length_m": 4.0,
"turning_radius_m": 3.0
},
"payload": {
"max_payload_kg": 100.0,
"current_payload_kg": 45.5,
"current_volume_m3": 0.3
},
"power_system": {
"battery_type": "lithium_ion",
"current_battery_level_kwh": 8.5,
"max_battery_level_kwh": 20.0,
"energy_consumption_per_km_kwh": 0.35,
"min_safe_battery_level_kwh": 2.0
},
"navigation_system": {
"max_speed_kmh": 40.0,
"max_speed_in_residential_area_kmh": 15.0,
"max_speed_in_tunnel_kmh": 30.0
},
"compatibility": {
"supported_charging_port_types": ["type2_ac", "ccs_dc"],
"supported_package_types": ["standard", "fragile", "cold_chain_0-8"]
}
}
}
2. 环境约束知识库（ECKB）
我们的城市“虚拟城”的 ECKB 如下（同样用 JSON 格式表示，这里我们只列出与本次问题实例相关的约束）：
{
"environment_id": "virtual_city_001",
"environment_type": "urban_area",
"constraints": [
{
"constraint_id": "tunnel_001_height",
"constraint_type": "physical_constraint",
"constraint_scope": "tunnel",
"constraint_target": "agent_physical_dimensions_height",
"constraint_operator": "<=",
"constraint_value": 2.5,
"constraint_location": {
"tunnel_id": "tunnel_001",
"start_point": {"lat": 31.2304, "lng": 121.4737},
"end_point": {"lat": 31.2354, "lng": 121.4787}
},
"severity": "Critical",
"description": "虚拟城隧道001的限高为2.5米"
},
{
"constraint_id": "pickup_001_cold_chain",
"constraint_type": "compatibility_constraint",
"constraint_scope": "pickup_point",
"constraint_target": "agent_supported_package_types",
"constraint_operator": "contains",
"constraint_value": "cold_chain_-18",
"constraint_location": {
"pickup_point_id": "pickup_001",
"lat": 31.2284,
"lng": 121.4717
},
"severity": "High",
"description": "取件点001的包裹是-18℃冷链包裹，需要Agent支持该类型包裹"
},
{
"constraint_id": "delivery_deadline_001",
"constraint_type": "temporal_constraint",
"constraint_scope": "delivery_point",
"constraint_target": "plan_delivery_time",
"constraint_operator": "<=",
"constraint_value": "2024-06-01T10:00:00+08:00",
"constraint_location": {
"delivery_point_id": "delivery_001",
"lat": 31.2384,
"lng": 121.4817
},
"severity": "High",
"description": "送件点001的配送截止时间是2024-06-01T10:00:00+08:00"
},
{
"constraint_id": "battery_safe_level",
"constraint_type": "agent_state_constraint",
"constraint_scope": "all_actions",
"constraint_target": "agent_power_system_current_battery_level_kwh",
"constraint_operator": ">=",
"constraint_value": 2.0,
"severity": "Critical",
"description": "Agent在执行任何动作时的电池电量必须大于等于2.0kWh"
},
{
"constraint_id": "charging_port_type",
"constraint_type": "compatibility_constraint",
"constraint_scope": "charging_point",
"constraint_target": "charging_point_port_type",
"constraint_operator": "in",
"constraint_value": ["type2_ac", "ccs_dc"],
"constraint_location": {
"charging_point_id": "charging_001",
"lat": 31.2404,
"lng": 121.4837,
"port_type": "type2_gb"
},
"severity": "High",
"description": "Agent的充电端口类型必须在充电点的支持的端口类型列表中"
}
]
}
3. 结构化 Agent 计划（SAP）
我们的大语言模型 GPT-4o 生成的 SAP 如下（我们用 JSON 格式表示，这里我们使用 **PDDL（Planning Domain Definition Language，自动规划领域的标准语言）的简化版本作为 SAP 的语义结构，因为 PDDL 有明确的动作、状态、目标的定义，非常适合静态验证；当然，你也可以使用你自己定义的语义结构，比如 JSON Schema 或者 Prolog 事实库）：
{
"plan_id": "courier_001_plan_20240601_0900",
"plan_type": "sequential_plan",
"start_time": "2024-06-01T09:00:00+08:00",
"start_state": {
"agent_current_location_lat": 31.2264,
"agent_current_location_lng": 121.4697,
"agent_current_battery_level_kwh": 8.5,
"agent_has_package": false,
"package_at_pickup_001": true
},
"goal_state": {
"agent_has_package": false,
"package_at_delivery_001": true
},
"actions": [
{
"action_id": "action_001",
"action_type": "navigate",
"action_name": "从当前位置导航到取件点001",
"start_time": "2024-06-01T09:00:00+08:00",
"end_time": "2024-06-01T09:15:00+08:00",
"parameters": {
"start_location": {"lat": 31.2264, "lng": 121.4697},
"end_location": {"lat": 31.2284, "lng": 121.4717},
"route": [
{"lat": 31.2264, "lng": 121.4697},
{"lat": 31.2274, "lng": 121.4707},
{"lat": 31.2284, "lng": 121.4717}
],
"distance_km": 2.0,
"estimated_energy_consumption_kwh": 0.7
},
"preconditions": {
"agent_has_package": false,
"agent_current_battery_level_kwh": ">=",
"agent_current_battery_level_kwh_value": 2.0
},
"effects": {
"agent_current_location_lat": 31.2284,
"agent_current_location_lng": 121.4717,
"agent_current_battery_level_kwh": 8.5 - 0.7 = 7.8
}
},
{
"action_id": "action_002",
"action_type": "pickup",
"action_name": "在取件点001取件",
"start_time": "2024-06-01T09:15:00+08:00",
"end_time": "2024-06-01T09:20:00+08:00",
"parameters": {
"pickup_point_id": "pickup_001",
"package_type": "cold_chain_-18",
"package_weight_kg": 5.0,
"package_volume_m3": 0.1
},
"preconditions": {
"agent_current_location": "pickup_001",
"agent_has_package": false,
"package_at_pickup_001": true,
"agent_current_payload_kg": "<=",
"agent_current_payload_kg_value": 95.0,
"agent_current_volume_m3": "<=",
"agent_current_volume_m3_value": 0.9
},
"effects": {
"agent_has_package": true,
"package_at_pickup_001": false,
"agent_current_payload_kg": 45.5 + 5.0 = 50.5,
"agent_current_volume_m3": 0.3 + 0.1 = 0.4
}
},
{
"action_id": "action_003",
"action_type": "navigate",
"action_name": "从取件点001导航到送件点001",
"start_time": "2024-06-01T09:20:00+08:00",
"end_time": "2024-06-01T09:50:00+08:00",
"parameters": {
"start_location": {"lat": 31.2284, "lng": 121.4717},
"end_location": {"lat": 31.2384, "lng": 121.4817},
"route": [
{"lat": 31.2284, "lng": 121.4717},
{"lat": 31.2294, "lng": 121.4727},
{"lat": 31.2304, "lng": 121.4737},
{"lat": 31.2314, "lng": 121.4747},
{"lat": 31.2324, "lng": 121.4757},
{"lat": 31.2334, "lng": 121.4767},
{"lat": 31.2344, "lng": 121.4777},
{"lat": 31.2354, "lng": 121.4787},
{"lat": 31.2364, "lng": 121.4797},
{"lat": 31.2374, "lng": 121.4807},
{"lat": 31.2384, "lng": 121.4817}
],
"distance_km": 15.0,
"estimated_energy_consumption_kwh": 5.25
},
"preconditions": {
"agent_has_package": true,
"agent_current_battery_level_kwh": ">=",
"agent_current_battery_level_kwh_value": 2.0
},
"effects": {
"agent_current_location_lat": 31.2384,
"agent_current_location_lng": 121.4817,
"agent_current_battery_level_kwh": 7.8 - 5.25 = 2.55
}
},
{
"action_id": "action_004",
"action_type": "deliver",
"action_name": "在送件点001送件",
"start_time": "2024-06-01T09:50:00+08:00",
"end_time": "2024-06-01T09:55:00+08:00",
"parameters": {
"delivery_point_id": "delivery_001"
},
"preconditions": {
"agent_current_location": "delivery_001",
"agent_has_package": true
},
"effects": {
"agent_has_package": false,
"package_at_delivery_001": true
}
},
{
"action_id": "action_005",
"action_type": "navigate",
"action_name": "从送件点001导航到充电点001",
"start_time": "2024-06-01T09:55:00+08:00",
"end_time": "2024-06-01T10:00:00+08:00",
"parameters": {
"start_location": {"lat": 31.2384, "lng": 121.4817},
"end_location": {"lat": 31.2404, "lng": 121.4837},
"route": [
{"lat": 31.2384, "lng": 121.4817},
{"lat": 31.2394, "lng": 121.4827},
{"lat": 31.2404, "lng": 121.4837}
],
"distance_km": 2.0,
"estimated_energy_consumption_kwh": 0.7
},
"preconditions": {
"agent_has_package": false,
"agent_current_battery_level_kwh": ">=",
"agent_current_battery_level_kwh_value": 2.0
},
"effects": {
"agent_current_location_lat": 31.2404,
"agent_current_location_lng": 121.4837,
"agent_current_battery_level_kwh": 2.55 - 0.7 = 1.85
}
}
]
}
4. 期望的可执行性验证报告（EVR）
我们的 APEC 应该输出如下的 EVR（同样用 JSON 格式表示）：
{
"plan_id": "courier_001_plan_20240601_0900",
"verification_result": "Fail",
"failure_reason_list": [
{
"failure_id": "failure_001",
"constraint_id": "tunnel_001_height",
"constraint_severity": "Critical",
"violation_action_id": "action_003",
"violation_description": "Agent的高度为2.8米，隧道001的限高为2.5米，Agent无法通过隧道001",
"violation_route_points": [
{"lat": 31.2304, "lng": 121.4737},
{"lat": 31.2314, "lng": 121.4747},
{"lat": 31.2324, "lng": 121.4757},
{"lat": 31.2334, "lng": 121.4767},
{"lat": 31.2344, "lng": 121.4777},
{"lat": 31.2354, "lng": 121.4787}
],
"suggested_fixes": [
"修改action_003的路线，绕过隧道001",
"使用高度更低的Agent（比如高度为2.4米的无人车）"
]
},
{
"failure_id": "failure_002",
"constraint_id": "pickup_001_cold_chain",
"constraint_severity": "High",
"violation_action_id": "action_002",
"violation_description": "Agent不支持-18℃冷链包裹，无法取件",
"suggested_fixes": [
"使用支持-18℃冷链包裹的Agent",
"与取件点001的客户联系，更换包裹类型或更换取件Agent"
]
},
{
"failure_id": "failure_003",
"constraint_id": "battery_safe_level",
"constraint_severity": "Critical",
"violation_action_id": "action_005",
"violation_description": "Agent在执行action_005后的电池电量为1.85kWh，低于最小安全电池电量2.0kWh",
"suggested_fixes": [
"在执行action_005之前先充电",
"修改action_003的路线，缩短距离，减少电池消耗",
"使用电池容量更大的Agent"
]
},
{
"failure_id": "failure_004",
"constraint_id": "charging_port_type",
"constraint_severity": "High",
"violation_action_id": "action_005",
"violation_description": "充电点001的端口类型是type2_gb，不在Agent支持的端口类型列表中",
"suggested_fixes": [
"修改action_005的终点，改为支持type2_ac或ccs_dc的充电点",
"使用支持type2_gb端口类型的Agent"
]
}
],
"constraint_satisfaction_rate": 0.2,
"optimization_suggestions": []
}
问题解决
现在我们知道了 APEC 是什么，以及它需要解决什么问题，接下来我们来讨论如何解决这个问题——也就是 APEC 的核心设计思路。
APEC 的核心设计思路可以概括为**“一个核心、两个支柱、三个模块、四个步骤**：
1. 一个核心：形式化约束表达（Formal Constraint Expression）
APEC 的核心是将所有可量化、可形式化的约束条件用一种计算机可以理解、可以推理的语言表达出来——如果约束条件不能形式化，那么静态验证就无从谈起。
2. 两个支柱：约束求解（Constraint Solving） 和 符号执行（Symbolic Execution）
APEC 的两个支柱是约束求解和符号执行：
- 约束求解：用来验证静态约束条件是否可满足（Satisfiable）——也就是是否存在一个状态，使得所有约束条件都成立。
- 符号执行：用来跟踪计划执行过程中的状态变化——也就是把计划执行过程中的状态变量用符号表示，而不是用具体的数值表示，这样就可以一次性验证所有可能的情况。
3. 三个模块：约束解析与编译模块（Constraint Parsing and Compilation Module, CPCM）、计划解析与符号执行模块（Plan Parsing and Symbolic Execution Module, PPSEM）、约束求解与验证报告生成模块（Constraint Solving and Verification Report Generation Module, CSVRGM）
APEC 的三个模块是约束解析与编译模块、计划解析与符号执行模块、约束求解与验证报告生成模块：
- 约束解析与编译模块：负责将 AML、ECKB 中的约束条件解析并编译成约束求解器可以理解的格式。
- 计划解析与符号执行模块：负责将 SAP 解析并执行符号执行，生成状态变化的约束条件。
- 约束求解与验证报告生成模块：负责将所有约束条件输入到约束求解器中进行求解，然后根据求解结果生成验证报告。
4. 四个步骤：输入解析与预处理、符号执行与约束生成、约束求解与结果分析、验证报告生成
APEC 的四个步骤是输入解析与预处理、符号执行与约束生成、约束求解与结果分析、验证报告生成：
- 输入解析与预处理：解析 AML、ECKB、SAP，检查它们的语法是否正确，是否有缺失的字段，是否有矛盾的内容，然后进行预处理（比如将时间戳转换为统一的格式，将地理位置转换为统一的坐标系等）。
- 符号执行与约束生成：对 SAP 进行符号执行，跟踪计划执行过程中的状态变化，生成状态变化的约束条件，同时将 ECKB 中的约束条件与计划的每个动作的前置条件和后置条件绑定起来，生成完整的约束条件集合。
- 约束求解与结果分析：将完整的约束条件集合输入到约束求解器中进行求解，如果约束条件集合是不可满足的（Unsatisfiable），那么计划就是不可执行的，约束求解器会返回一个不可满足的核心（Unsatisfiable Core, UNSAT Core）——也就是导致约束条件集合不可满足的最小子集，我们可以根据这个 UNSAT Core 来定位违反的约束条件；如果约束条件集合是可满足的，那么计划就是可执行的，约束求解器会返回一个模型（Model）——也就是满足所有约束条件的一个具体的状态序列。
- 验证报告生成：根据约束求解的结果生成验证报告，包括验证结果、失败原因列表、约束满足度、优化建议等。
边界与外延
1. 边界
APEC 有一些明确的边界，也就是它不能做什么：
- 不能验证不可形式化的约束条件：比如“用户满意度”“品牌形象”“人际关系”等不可量化、不可形式化的约束条件，APEC 是无法验证的——这些约束条件需要由 LLM 或人工来验证。
- 不能验证动态变化的环境约束条件（除非有先验的概率分布）：比如“明天会不会下雨”“交通拥堵程度”等动态变化的环境约束条件，如果没有先验的概率分布，APEC 是无法验证的——不过，如果有先验的概率分布，我们可以用概率约束规划（Probabilistic Constraint Programming, PCP） 来验证计划的可执行性概率。
- 不能验证 LLM 生成的计划的语义正确性（除非有明确的语义定义）：比如“LLM 生成的计划是否符合用户的意图”“LLM 生成的计划是否符合道德规范”等语义正确性问题，如果没有明确的语义定义，APEC 是无法验证的——不过，如果有明确的语义定义，我们可以用形式化验证（Formal Verification） 来验证计划的语义正确性。
- 不能替代动态检查模块：APEC 是静态验证，它只能验证先验的约束条件，不能验证执行过程中的动态变化——比如“执行过程中突然出现的障碍物”“执行过程中电池电量的实际消耗与估计值不一致”等，这些需要由动态检查模块来验证。
2. 外延
APEC 也有一些明确的外延，也就是它可以扩展做什么：
- 可以作为自动规划器的约束条件输入：APEC 可以将 ECKB 中的约束条件直接输入到自动规划器中，让自动规划器在生成计划的时候就考虑这些约束条件，从而生成一个可执行的计划——这样就不需要事后验证了。
- 可以作为 LLM 的结构化输出约束：APEC 可以将约束条件转换为 JSON Schema 或者 Prolog 事实库，作为 LLM 的结构化输出约束，让 LLM 在生成计划的时候就输出符合约束条件的计划——这样也可以减少事后验证的工作量。
- 可以作为计划优化器的基础：APEC 可以在验证计划通过之后，进一步优化计划——比如缩短配送路径、减少电池消耗、降低风险敞口等。
- 可以作为多 Agent 协作的约束条件验证器：APEC 可以验证多 Agent 协作的计划的可执行性——比如验证多个无人车的配送计划是否会发生碰撞、是否会超出交通流量限制等。
概念结构与核心要素组成
核心要素组成
APEC 的核心要素组成可以分为输入要素、处理要素、输出要素三个部分：
1. 输入要素
输入要素包括Agent 模型库（AML）、环境约束知识库（ECKB）、结构化 Agent 计划（SAP）：
1.1 Agent 模型库（AML）
Agent 模型库是 APEC 的第一个输入要素，它包含 Agent 自身的所有可量化、可形式化的属性。AML 的核心要素包括：
- Agent ID：Agent 的唯一标识符。
- Agent 类型：Agent 的类型（比如 urban_logistics_drone_truck、industrial_robot、financial_trading_agent 等）。
- Agent 属性集合：Agent 的属性集合，每个属性都有一个**属性名称、属性类型、属性值、属性单位（如果有的话）、属性约束（比如属性的取值范围、属性的变化规则等）。
Agent 属性集合可以进一步细分为物理属性、功能属性、状态属性、兼容性属性四个子集合：
- 物理属性：Agent 的物理属性（比如高度、宽度、长度、载重量、体积等）。
- 功能属性：Agent 的功能属性（比如最大速度、最大续航里程、机械臂自由度等）。
- 状态属性：Agent 的状态属性（比如当前电池电量、当前载重量、当前位置等）——这些属性会随着计划的执行而变化。
- 兼容性属性：Agent 的兼容性属性（比如支持的充电端口类型、支持的包裹类型、支持的文件格式等）。
1.2 环境约束知识库（ECKB）
环境约束知识库是 APEC 的第二个输入要素，它包含 Agent 运行环境的所有可量化、可形式化的约束。ECKB 的核心要素包括：
- 环境 ID：环境的唯一标识符。
- 环境类型：环境的类型（比如 urban_area、factory_floor、financial_market 等）。
- 环境约束集合：环境的约束集合，每个约束都有一个约束 ID、约束类型、约束范围、约束目标、约束操作符、约束值、约束位置（如果有的话）、约束严重程度、约束描述。
环境约束集合可以进一步细分为物理约束、时间约束、空间约束、资源约束、兼容性约束、安全约束、合规约束七个子集合：
- 物理约束：环境的物理约束（比如隧道的限高限宽、桥梁的限重、门的宽度等）。
- 时间约束：环境的时间约束（比如配送截止时间、充电点的可用时间、金融交易的时段等）。
- 空间约束：环境的空间约束（比如禁止通行区域、安全围栏位置、操作区域等）。
- 资源约束：环境的资源约束（比如充电桩的数量、原材料的数量、云实例的数量等）。
- 兼容性约束：环境的兼容性约束（比如充电端口类型、包裹类型、文件格式等）。
- 安全约束：环境的安全约束（比如安全距离、安全速度、安全操作顺序等）。
- 合规约束：环境的合规约束（比如交通规则、金融监管规则、医疗合规规则等）。
1.3 结构化 Agent 计划（SAP）
结构化 Agent 计划是 APEC 的第三个输入要素，它是由大语言模型或自动规划器生成的、具有明确语义结构的计划。SAP 的核心要素包括：
- 计划 ID：计划的唯一标识符。
- 计划类型：计划的类型（比如 sequential_plan、branching_plan、looping_plan、parallel_plan、hierarchical_plan 等）。
- 开始时间：计划的开始时间。
- 开始状态：计划的开始状态，也就是计划执行之前 Agent 和环境的状态。
- 目标状态：计划的目标状态，也就是计划执行之后 Agent 和环境的期望状态。
- 动作集合：计划的动作集合，每个动作都有一个动作 ID、动作类型、动作名称、开始时间、结束时间、参数集合、前置条件集合、后置条件集合。
动作集合可以进一步细分为原子动作、复合动作两个子集合：
- 原子动作：不可再分解的动作（比如 navigate、pickup、deliver、charge 等）。
- 复合动作：由多个原子动作或复合动作组成的动作（比如 pick_up_and_deliver 是由 pickup 和 deliver 两个原子动作组成的复合动作）。
2. 处理要素
处理要素包括约束解析与编译模块（CPCM）、计划解析与符号执行模块（PPSEM）、约束求解与验证报告生成模块（CSVRGM）、约束求解器：
2.1 约束解析与编译模块（CPCM）
约束解析与编译模块是 APEC 的第一个处理要素，它负责将 AML、ECKB 中的约束条件解析并编译成约束求解器可以理解的格式。CPCM 的核心功能包括：
- AML 解析与预处理：解析 AML，检查它的语法是否正确，是否有缺失的字段，是否有矛盾的内容，然后进行预处理（比如将属性值转换为统一的单位）。
- ECKB 解析与预处理：解析 ECKB，检查它的语法是否正确，是否有缺失的字段，是否有矛盾的内容，然后进行预处理（比如将时间戳转换为统一的格式，将地理位置转换为统一的坐标系）。
- 约束条件编译：将 AML 中的属性约束和 ECKB 中的环境约束编译成约束求解器可以理解的格式（比如 SMT-LIB 格式、Z3 格式、CPLEX 格式等）。
2.2 计划解析与符号执行模块（PPSEM）
计划解析与符号执行模块是 APEC 的第二个处理要素，它负责将 SAP 解析并执行符号执行，生成状态变化的约束条件。PPSEM 的核心功能包括：
- SAP 解析与预处理：解析 SAP，检查它的语法是否正确，是否有缺失的字段，是否有矛盾的内容，然后进行预处理（比如将时间戳转换为统一的格式，将地理位置转换为统一的坐标系）。
- 符号执行引擎：对 SAP 进行符号执行，跟踪计划执行过程中的状态变化，生成状态变化的约束条件。
- 约束条件绑定：将 ECKB 中的环境约束与计划的每个动作的前置条件和后置条件绑定起来，生成完整的约束条件集合。
2.3 约束求解与验证报告生成模块（CSVRGM）
约束求解与验证报告生成模块是 APEC 的第三个处理要素，它负责将所有约束条件输入到约束求解器中进行求解，然后根据求解结果生成验证报告。CSVRGM 的核心功能包括：
- 约束条件集合生成：将 CPCM 编译的约束条件和 PPSEM 生成的约束条件合并起来，生成完整的约束条件集合。
- 约束求解器调用：调用约束求解器对完整的约束条件集合进行求解。
- UNSAT Core 分析：如果约束条件集合是不可满足的，分析 UNSAT Core，定位违反的约束条件。
- 验证报告生成：根据约束求解的结果生成验证报告。
2.4 约束求解器
约束求解器是 APEC 的核心处理工具，它负责对约束条件集合进行求解。常见的约束求解器包括：
- SMT 求解器：比如 Z3、CVC4、Yices 等，适合处理**布尔逻辑、整数逻辑、实数逻辑、位向量逻辑、数组逻辑、量化逻辑等组合的约束条件。
- CP 求解器：比如 CPLEX、Gurobi、Choco、Google OR-Tools 等，适合处理组合优化、调度、路径规划等约束条件。
- SAT 求解器：比如 MiniSAT、Glucose、Lingeling 等，适合处理纯布尔逻辑的约束条件。
在 APEC 中，我们通常使用 Z3 作为主要的约束求解器——因为 Z3 是微软研究院开发的开源 SMT 求解器，它支持多种逻辑理论，功能强大，效率高，而且有 Python、Java、C++ 等多种语言的绑定，非常适合工程落地。
3. 输出要素
输出要素是可执行性验证报告（EVR）：
3.1 可执行性验证报告（EVR）
可执行性验证报告是 APEC 的输出要素，它包含验证结果、失败原因列表、约束满足度、优化建议等内容。EVR 的核心要素包括：
- 计划 ID：被验证的计划的唯一标识符。
- 验证结果：计划是否满足所有约束条件（Pass/Fail）。
- 失败原因列表：如果验证失败，列出所有违反的约束条件、违反的位置、违反的严重程度、建议的修复方案。
- 约束满足度：计划满足所有约束条件的百分比。
- 优化建议：即使验证通过，也会给出一些优化计划的建议。
概念之间的关系
1. 概念核心属性维度对比
我们用一个 Markdown 表格来对比 APEC 的三个输入要素的核心属性维度：
| 核心属性维度 | Agent 模型库（AML） | 环境约束知识库（ECKB） | 结构化 Agent 计划（SAP） |
|---|---|---|---|
| 来源 | Agent 开发者/部署者配置 | 环境管理员/部署者配置 | LLM/自动规划器生成 |
| 变化频率 | 低（通常只在 Agent 升级或更换时变化） | 中（可能会随着环境的变化而变化） | 高（每次生成计划时都会变化） |
| 是否可形式化 | 是（所有属性都是可量化、可形式化的） | 是（所有约束都是可量化、可形式化的） | 是（所有动作、状态、目标都是可量化、可形式化的） |
| 是否随计划执行而变化 | 部分是（状态属性 |
Agent 垂直技术社区，欢迎活跃、内容共建。
更多推荐
9
0- 0
已为社区贡献39条内容
所有评论(0)