기술 요약: 이산 시스템의 전이 편차에 대한 신경-기호적 강건성 분석 (NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations)

문제 정의

이산 이벤트 시스템(Discrete-Event Systems, DES)의 감독 제어(Supervisory Control)에서, 제어기는 플랜트 모델에 대한 명세를 강제하도록 합성된다. 고전적인 방법들은 "설계에 의한 정당성(correct-by-construction)" 보장을 제공하지만, 이러한 보장은 공칭 모델(nominal model)의 정확성에 엄격하게 의존한다. 실제 환경에서는 미모델링된 역학, 센서 노이즈, 또는 추상화 오류로 인한 불일치가 발생하여 실제 시스템이 공칭 모델로부터 벗어나게 되며, 이는 잠재적으로 안전성을 저해할 수 있다.

최근 연구들은 **이산 강건성(discrete robustness)**을 (공칭 플랜트에 추가된 전이들을 포함하는) 가능한 모든 전이 편차의 집합으로 정의함으로써 이 문제를 다루어 왔다. 그러나 이러한 전이 기반 접근 방식은 두 가지 결정적인 한계에 직면해 있다:

1. 확장성(Scalability): 가능한 편차의 공간은 상태 및 액션 공간에 따라 기하급수적으로 증가하며, 이는 매우 작은 시스템을 제외하고는 전수 조사가 계산적으로 불가능하다.
2. 보수성(Conservatism): 수학적으로 가능한 편차의 대다수는 물리적으로 불가능하다 (예: 기계가 입력 없이 갑자기 부품을 출력하는 경우). 이러한 불가능한 편차를 포함하는 것은 탐색 공간을 팽창시키고, 실제 시스템의 동작을 정확하게 반영하지 못하는 강건성 결과를 낳는다.

불가능한 편차를 필터링하기 위해 물리적 시스템 제약($P_{sys}$)을 사용하는 기존의 시도들은, 도메인 전문가가 물리 법칙을 형식적 명세로 수동 코딩해야 하므로 상당한 부담과 분석 파이론의 오버헤드를 초래한다.

방법론

본 논문은 이러한 확장성 및 실현 가능성 문제를 해결하기 위해 **신경-기호적 컴퓨팅 프레임워크(neurosymbolic computing framework)**를 제안한다. 이 접근 방식은 물리적 실현 가능성에 대한 추론과 강건성 보장의 형식적 계산을 분리하여, 두 단계의 프로세스를 활용한다:

1. 신경 기반 실현 가능성 필터링 (LLM 계층)

첫 번째 단계는 대규모 언어 모델(LLM)을 활용하여 물리적으로 실현 가능한 편이 전이($D$)의 부분 집합을 추론한다.

• 입력: 프레임워크는 플랜트의 형식적 LTS 모델, 제어기, 시스템 상태 및 이벤트에 대한 자연어 설명, 안전 명세, 그리고 물리 법칙(예: "부품은 동시에 두 곳에 존재할 수 없다")에 관한 도메인 지식을 입력으로 받는다.
• 프로세스: 구조화된 프롬프트 템플릿이 LLM이 이러한 입력들을 추론하도록 유도한다. LLM은 시스템의 의미론 및 물리적 제약과 일치하는 현실적인 결함 또는 편차를 식별하는 과업을 수행한다.
• 출력: $(Q_E \times Act_E \times Q_E) \setminus R_E$ 보다 현저히 작은, 축소된 실현 가능한 편이 집합 $D$를 생성한다.

2. 기호적 강건성 검증 (기호 계층)

두 번째 단계는 축소된 집합 $D$에 대해 형식적 검증을 수행한다.

• 프로세스: 브루트 포스 알고리즘(Algorithm 1)이 가능한 모든 편이 부분 집합 $D$를 순회한다. 각 후보 편이 집합 $d$에 대해, 표준 모델 체킹을 사용하여 제어기 $S$에 의해 제어되는 편이 시스템 $E_d$가 안전 속성 $P$를 만족하는지(즉, $E_d/S \models P$) 확인한다.
• 정교화(Refinement): 알고리즘은 최종 강건성 집합 $\Delta_f$를 형성하기 위해 최대(maximal) 강건 편이(다른 강건한 편이에 포함되지 않는 것)만을 추출한다.
• 보장(Guarantee): 검증이 형식적으로 정의된 전이 시스템 상에서 기호적으로 수행되기 때문에, 추론된 집합 $D$에 대한 강건성 보장은 수학적으로 정확하게 유지된다.

주요 기여

본 논문은 두 가지 주요 기여를 명시한다:

1. 신경-기호적 프레임워크: LLM을 사용하여 물리적으로 실현 가능한 편이 모델을 추론하고, 기호적 방법을 사용하여 강건성 보장을 계산하는 새로운 아키텍처를 제시한다. 이 접근 방식은 자연어와 도메인 지식으로부터 물리적 제약을 추출하는 과정을 자동화하여, $P_{sys}$를 수동으로 형식적 인코딩할 필요성을 제거한다.
2. 프로토타입 및 평가: 프로토타입 도구의 구현과 세 가지 뚜렷한 사례 연구(제조 시스템, Therac-25 방사선 치료 인터페이스, Alternate Bit Protocol (ABP))에 대한 실험적 평가를 수행한다.

실험 결과

프레임워크는 실현 가능성 필터링을 위한 LLM(GPT-5.2 및 Claude 3.5 Sonnet)과 Python 기반 기호 검증기를 사용하여 세 가지 사례 연구를 평가하였다.

• 제조 시스템: LLM은 18개의 실현 가능한 편이를 식별했다 (이론적 공간은 108개). 기호 계층은 하나의 최대 강건 편이 집합을 찾아냈으며, 시스템이 15개의 특정 전이에 대해서는 강건하지만 특정 버퍼 언로딩 결함에는 취약함을 확인했다.
• Therac-25: 분석 결과 9개의 실현 가능한 편이가 식별되었다. 시스템은 반복적인 운영자의 "enter" 입력에는 강건하지만, 전자 치료 선택과 관련된 특정 레이스 컨디션(race condition)에는 취약한 것으로 나타나, 역사적인 설계 결함을 정확히 포착했다.
• ABP 프로토ка: LLM은 16개의 실현 가능한 편이를 식별했다. 분석 결과 메시지 손실, 중복 및 손상에 대한 강건성을 확인하였으며, 이는 프로토콜의 설계 의도와 일치한다.

정량적 결과:

• 실현 가능성 감소: LLM은 탐색 공간을 크게 줄였다. 감소 폭은 전체 전이 공간 대비 Therac-25의 경우 67%에서 ABP의 경우 99%에 달했다.
• 실현 가능성 정확도: 제조 예제의 경우, GPT가 생성한 전이의 89%가 물리적으로 실현 가능했던 반면, Claude는 54%를 기록했다. ABP와 같은 더 복잡한 시스템에서는 두 모델 모두 실현 가능성 비율이 떨어졌으며(각각 63%와 36%), 이는 프롬프트 엔지니어링이나 도메인 온톨로지의 개선이 필요함을 시사한다.
• 강건성 등가성: 축소된 편이 집합에서 작동했음에도 불구하고, 프레임워크는 평가된 사례들에서 전체 전이 기반 분석으로부터 얻은 결과와 대등한 강건성 보장을 생성했다.

의의 및 주장

본 논문은 이 신경-기호적 접근 방식이 이산 강건성 분석에서 확장성과 불가능한 편이의 포함 사이의 트레이드오프를 성공적으로 해결한다고 주장한다. 의미론적 및 물리적 이해를 바탕으로 LLM을 사용하여 솔루션 공간을 필터링함으로써, 이 방법은 전수 조사가 불가능한 시스템에 대해서도 강건성 분석을 실행 가능하게 만든다.

저자들은 LLM 구성 요소가 실현 가능한 편이를 식별하는 데 있어 확률적 요소를 도입하지만, 후속 기호 검증이 추론된 집합 $D$에 대해 최종 강건성 보장이 형식적으로 정확함을 보장한다는 점을 강조한다. 본 연구는 훨씬 더 작고 물리적으로 유의미한 편이 부분 집합을 운용하면서도, 전체 공간 방법과 대등한 강건성 분석을 회복할 수 있음을 입증한다.

논문은 현재의 브루트 포스 알고리즘 구현이 더 큰 시스템을 위해 최적화가 필요하며, 향후 연구는 프롬프트 엔지니어링 개선, LLM 정확도를 높이기 위한 도메인 온톨로지 통합, 그리고 기호적 결과가 LLM 쿼리를 가이드하는 상호작용적 정교화 루프를 조사하는 데 집중할 것이라고 겸허히 결론짓는다.