Logic-Based Verification of Task Allocation for LLM-Enabled Multi-Agent Manufacturing Systems

1. 문제 정의 (Problem Definition)

• 배경: 개인화 제품 수요 증가로 인해 제조 업계는 높은 제품 다양성과 동적 운영 조건을 수용해야 합니다. 이를 위해 분산 의사결정을 지원하는 다중 에이전트 시스템 (MAS) 이 유연성을 높이기 위해 도입되고 있습니다.
• 한계점: 기존 MAS 는 사전 정의된 작업 모델에 의존하므로 새로운 제품 요구사항에 적응하는 데 한계가 있습니다.
• 새로운 도전: 대형 언어 모델 (LLM) 이 제조 시스템에 도입되어 적응형 작업 계획 및 조정을 가능하게 했지만, LLM 의 출력은 충돌 회피나 작업 순서와 같은 안전 제약 조건을 보장하지 못합니다.
• 핵심 문제: 새로운 제품 요구사항이 주어졌을 때, 사전 정의된 모델에 의존하지 않고 LLM 이 생성한 작업 계획을 안전 제약 조건 (안전성) 을 만족하도록 검증하고 수정하는 방법론이 필요합니다. 특히 단일 에이전트의 작업은 안전하더라도, 다중 에이전트 간의 자원 충돌이나 동기화 문제로 인해 전체 계획이 위험할 수 있습니다.

2. 제안된 방법론 (Methodology)

이 논문은 LLM 기반 다중 에이전트 시스템에서 생성된 작업 계획을 검증하기 위한 제어 아키텍처를 제안합니다. 이 아키텍처는 역대치 (Counterexample) 기반 유도 합성 (CEGIS) 아이디어를 차용하여, LLM 의 유연성과 논리 기반 검증의 안전성을 결합합니다.

A. 시스템 아키텍처 구성

1. 제품 에이전트 (Product Agent, PA):
   • 자연어 (NL) 로 된 제품 요구사항과 자원 능력을 LLM 을 통해 해석합니다.
   • 작업 의존성과 동시성을 표현하는 유방향 비순환 그래프 (DAG) 형태의 작업 계획을 생성합니다.
   • 이 DAG 를 이산 사건 시스템 (DES) 을 위한 유한 상태 오토마타 (FSA) 로 컴파일합니다.
2. 중앙 제어 에이전트 (Central Controller Agent, CCA):
   • 전체 시스템의 전역 관점을 유지하며 안전성을 보장합니다.
   • 자연어로 된 안전 요구사항을 선형 시계 논리 (LTLf) 로 변환하고, 이를 안전 오토마타 (Safety Automaton) 로 컴파일합니다.
   • 생성된 작업 계획 오토마타와 안전 오토마타를 결합하여 도달 가능성 분석 (Reachability Analysis) 을 수행합니다.

B. 검증 및 피드백 루프

1. 안전 검증 (Safety Validation):
   • CCA 는 DFS(깊이 우선 탐색) 기반 알고리즘을 사용하여 작업 계획 오토마타와 안전 오토마타의 곱 (Product) 상태를 탐색합니다.
   • 만약 탐색 과정에서 위반 상태 (Violation State) 에 도달하면, 해당 계획은 안전하지 않다고 판별합니다.
2. 재계획 (Replanning with Feedback):
   • 위반이 감지되면, CCA 는 위반된 안전 조건, 위반을 일으킨 증거 경로 (Witness Trace), 실행 컨텍스트 등을 구조화된 피드백으로 PA 에게 전달합니다.
   • PA 는 LLM 을 활용하여 이 피드백을 바탕으로 안전 제약 조건을 준수하는 새로운 작업 계획을 생성합니다.
   • 이 과정은 계획이 안전해질 때까지 반복됩니다.

3. 주요 기여 (Key Contributions)

1. 검증 지원 제어 아키텍처: LLM 이 생성한 작업 계획을 검증할 수 있는 새로운 제어 아키텍처를 제안했습니다. 이는 LLM 의 유연성을 유지하면서도 제조 현장의 안전성을 보장합니다.
2. 오토마타 기반 검증 프로세스: 작업 계획을 이산 사건 시스템 (DES) 모델로 변환하고, 이를 선형 시계 논리 (LTLf) 로 표현된 안전 제약 조건과 비교하여 공식적으로 평가하는 프로세스를 정립했습니다.
3. 피드백 기반 재계획 메커니즘: 검증 결과 (위반 정보) 를 구조화된 피드백으로 활용하여 LLM 이 작업을 수정하고 안전한 계획을 다시 생성하도록 유도하는 메커니즘을 구현했습니다.

4. 실험 결과 (Results)

• 실험 설정: 2 개, 3 개, 4 개의 로봇이 참여하는 3 가지 조립 시나리오 (S1, S2, S3) 를 설정하여 평가했습니다. 각 시나리오는 로봇 수, 부품 수, 안전 규칙 수를 점진적으로 증가시켰습니다.
• 비교 대상: 제안된 프레임워크 vs. 순수 LLM 기반 (안전 규칙을 자연어로만 입력받는 경우).
• 주요 성과:
  • 안전 규칙 준수율 향상:
    • S1: 50.00% (순수 LLM) → 92.50% (제안 프레임워크)
    • S2: 75.93% → 91.67%
    • S3: 50.00% → 86.25%
  • 결론: 순수 LLM 만으로는 안전 제약 조건을 일관되게 준수하는 계획을 생성하기 어렵지만, 논리 기반 검증과 재계획 루프를 도입하면 모든 시나리오에서 안전성 준수율이 크게 향상되었습니다.
  • 비용 분석: 문제 규모가 커질수록 (S3) 검증 시간과 재시도 횟수가 증가하는 경향이 있었으나, 이는 복잡한 다중 에이전트 환경에서의 필수적인 트레이드오프로 분석되었습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 안전성과 유연성의 조화: 이 연구는 LLM 의 적응형 계획 능력을 활용하면서도, 형식적 검증 (Formal Verification) 을 통해 제조 시스템의 치명적인 안전 사고를 예방할 수 있음을 입증했습니다.
• 실용적 적용 가능성: 사전 정의된 모델에 의존하지 않고 자연어 요구사항을 실시간으로 처리하면서도 안전을 보장하므로, 맞춤형 제조 (Mass Customization) 환경에 매우 적합합니다.
• 향후 과제:
  • 대규모 공장 환경으로 확장 시 단일 중앙 제어기의 병목 현상을 해결하기 위해 계층적 검증 아키텍처 도입 필요.
  • 예기치 않은 사건 발생 시 실시간 (Runtime) 안전 검증을 지원하도록 프레임워크 확장.
  • LLM 의 재계획 수렴성을 높이고 검증 시간을 단축하기 위한 심볼릭 및 구성적 검증 방법론 연구.

이 논문은 인공지능 (LLM) 과 형식 방법 (Formal Methods) 의 융합을 통해 차세대 지능형 제조 시스템의 안전성을 확보할 수 있는 중요한 방향성을 제시합니다.