智能体系统★ 评分 5.1
Logic-Based Verification of Task Allocation for LLM-Enabled Multi-Agent Manufacturing Systems
Jonghan Lim, Mostafa Tavakkoli Anbarani, Rômulo Meira-Góes, Ilya Kovalenko
2026年4月26日
关键词
大语言模型多智能体制造时序逻辑离散事件系统任务分配验证
核心发现
- 只靠LLM依据自然语言安全规则生成任务计划，规则满足率不稳定，说明语言推理本身不足以保证制造执行安全。
- 将安全约束形式化为LTLf并转成安全自动机后，可对LLM生成的计划做预执行DFS可达性检查，能在任务执行前定位违反顺序约束和互斥约束的路径。
- 引入“验证结果→结构化反馈→LLM重规划”后，三个场景的规则满足率分别从50.00%/75.93%/50.00%提升到92.50%/91.67%/86.25%，但仍未达到100%，且规模增大时验证代价急剧上升。
实验规模
在三个递增复杂度的多机器人装配场景S1/S2/S3中评估，规模分别为2/3/2、3/4/3、4/6/4（机器人/零件/安全规则）。每个场景进行20次试验，重规划循环最多5次修复尝试；使用GPT-5生成与修复任务计划。对比了仅用自然语言安全约束的纯LLM基线与本文框架；验证过程中遍历的计划状态数从170增至1,378和14,618，平均验证时间从0.10s增至1.53s和25.46s。
局限性
方法依赖人工专家先把自然语言安全要求正确翻译并审核为LTLf/自动机，这一步既不可扩展，也引入主观性。实验只覆盖三个小规模装配场景，基线也较弱，缺少与传统形式化规划、运行时监控或更强任务分配方法的系统比较。与此同时，重规划并无收敛保证，且S3中验证时间已明显膨胀，说明可扩展性仍是主要瓶颈。