기술 요약: 불확실성을 포함한 데모로부터 선형 시간 논리(LTL) 사양 학습

문제 정의

본 논문은 안전이 중요한 도메인(예: 로보틱스, 자율 주행 차량)에서 시스템 데모로부터 선형 시간 논리(Linear Temporal Logic, LTL) 사양을 추론하는 과제를 다룹니다. 양의 트레이스(positive traces)와 음의 트레이스(negative traces)로부터 LTL을 학습하는 기존 방식들은 트레이스 자체가 정확하게 캡처되었다고 가정하며 레이블 오분류 오류만을 고려하지만, 실제 환경의 데이터는 트레이스 불확실성(trace uncertainty) 문제를 겪는 경우가 많습니다. 이러한 불확실성은 센서 결함, 측정 오류, 데이터 손실 또는 통신 지연으로부터 발생하며, 이로 인해 트레이스가 오염되거나 불완전하거나 일관성이 없을 수 있습니다.

관측된 트레이스를 그라운드 트루스(ground truth)로 취급하는 기존 방법들은 트레이스 내용 자체가 불확실할 경우 정확한 사양을 복구하는 데 실패합니다. 저자들은 **강건한 LTL 학습 문제(Robust LTL Learning Problem)**를 정의합니다. 이는 관측된 트레이스가 완벽하게 정확하다고 가정하는 대신, 관측된 트레이스에 존재하는 유계된 불확실성에도 불구하고 시스템 동작을 설명할 수 있는 최소한의 LML 수식을 찾는 것입니다.

방법론

제안된 프레임워크는 트레이스 불확실성을 모델링하고 이를 의사 불리언 최적화(Pseudo-Boolean Optimization) 문제에 통합합니다. 방법론은 다음 단계들을 통해 진행됩니다.

1. 트레이스 불확실성 모델링

저자들은 관측된 트레이스와 잠재적인 "정확한" 트레이스 사이의 **해밍 거리(Hamming distance)**를 사용하여 불확실성을 정량화합니다.

• 트레이스 추정 그룹 ($C^k_{tr}$): 관측된 트레이스 $tr$과 불확실성 경계$k$가 주어졌을 때, 트레이스 추정 집합은$tr$로부터 해밍 거리가$k$ 이내인 모든 트레이스를 포함합니다.
• 가정: 실제 시스템 동작은 관측된 트레이스 자체가 아니라, 이 불확실성 그룹 내의 트레이스 중 하나라고 가정합니다.

2. 강건한 학습 정식화

학습 문제는 개별 트레이스가 아닌 이러한 그룹을 처리하도록 재정식화됩니다.

• 그룹 오분류: 모든 관측된 트레이스가 수식을 만족해야 하는 대신, 이 프레임워크는 각 불확실성 그룹 내에서 적어도 하나의 트레이스(양의 트레이스의 경우)가 수식을 만족하고, 각 음의 불확실성 그룹 내에서는 적어도 하나의 트레이스가 수식을 만족하지 않도록 요구합니다.
• 손실 함수: 그룹 오분류 손실 함수 $\ell_g$를 정의합니다. 이는 어떤 트레이스도 학습된 수식과 일치하지 않는 경우에 페널티를 부여합니다.

3. 알고리즘 구현 (의사 불리언 최적화)

이 문제는 명제식 $\Phi$로 인코딩되며 Max-SMT(구체적으로 의사 불리언 최적화)를 통해 해결됩니다. 이 수식은 네 가지 제약 범주로 구성됩니다.

• 구문 제약 ($\Phi_{syn}$): 학습된 수식이 유효한 LTL 문법(구문 트리로 표현됨)을 준수하도록 보장합니다.
• 의미론적 제약 ($\Phi_{sem}$): 트레이스와 LTL 수식 사이의 만족 관계를 인코딩합니다.
• 선택 제약 ($\Phi_{sel}$): 특정 불확실성 그룹에서 학습에 사용할 구체적인 트레이스 추정치를 선택하기 위해 이진 변수 $z_{tr}$을 도입합니다. 만약 특정 트레이스가 선택되면($z_{tr}=1$), 해당 트레이스는 수식을 만족하거나 만족하지 않아야 합니다.
• 그룹 제약 ($\Phi_{grp}$): 모든 관측된 트레이스에 대해, 해당 불확실성 그룹 내의 적어도 하나의 트레이스 추정치가 선택되어야 함($z_{tr'}=1$)을 강제하는 소프트 제약 조건입니다.

목표는 모든 하드 제약 조건을 만족하면서 (트레이스 수에 따라 가중치가 부여된) 그룹 오분류 손실을 최소화하는 것입니다. 이는 의사 불리언 목적 함수를 최소화함으로써 해결됩니다.

주요 기여

1. 새로운 문제 정식화: 본 논문은 레이블 노이즈뿐만 아니라 트레이스 내용(오염/불완전성)의 불확실성을 명시적으로 다루는 "강건한 LTL 학습 문제"를 도입했습니다.
2. 불확실성 모델링: 해밍 거리를 사용하여 트레이스 추정 그룹을 정의함으로써, 시스템이 주어진 관측값에 대한 다양한 가능한 "실제" 동작을 고려할 수 있게 합니다.
3. 그룹 기반 제약: 학습 알고리즘이 오염된 데이터 포인트에 의해 잘못 유도되는 것을 방지하기 위해, 각 불확찰성 그룹당 적어도 하나의 트레이스가 일관성을 유지해야 함을 강제합니다.
4. 최적화 접근 방식: 강건한 학습 문제를 SMT 솔버(예: Z3)를 통해 해결 가능한 동등한 의사 불리언 최적화 문제로 환원했습니다.

실험 결과

저자들은 두 가지 벤치마크를 사용하여 제안된 방법론을 최신 SAT 기반 학습 방식(특히 "Flie" 알고리즘과 사용자 제약 사항을 포함하는 "Modified Flie" 변형 모델)과 비교 평가했습니다.

1. HVAC 제어 시스템: 온도, 점유 여부, 에어컨 상태를 나타내는 원자적 명제(atomic propositions)를 포함한 실제 시나리오입니다.
2. 합성 LTLf 패턴: 불확실성이 주입된 다양한 그라운드 트루스 LTL 수식을 사용한 실험입니다.

결과:

• 정확도: 제안된 강건한 학습 방법은 기존 방법들보다 그라운드 트루스 수식에 더 밀접하게 부합하는 사양을 복구했습니다.
• 시간적 관계: 표준 방식(Flie)은 불확실성 하에서 종종 시간적 의존성을 포착하지 못하거나 가짜 관계를 학습했으며, Modified Flie는 관계를 부분적으로 복구했으나 인과 방향을 반대로 학습하는 경우가 있었습니다. 반면, 강건한 방법은 핵심적인 시간적 구조(예: 전역 조건 및 즉각적 의존성)를 일관되게 보존했습니다.
• 계산 비용: 강건한 방법은 베이스라인 모델들보다 더 많은 계산 시간을 필요로 했습니다. 저자들은 이를 표준 Max-SAT에 비해 의사 불리언 최적화의 복잡도가 높기 때문이라고 설명했습니다.

의의 및 주장

본 논문은 제 프레임워크가 이론적인 LTL 학습과 데이터가 불완전한 실제 시나리오 사이의 간극을 메운다고 주장합니다. 입력 트레이스가 노이즈가 있거나 불완전할 때도 실제 시스템 동작을 반영하는 최소한의 해석 가능한 LTL 수식을 효과적으로 포착함으로써, 이 방법은 사양 학습 과정에서 불확실성을 효과적으로 다룰 수 있게 합니다.

저자들은 이 연구를 안전이 중요한 시스템을 위한 강건한 형식 검증 및 컨트롤러 합성으로 나아가는 단계로 위치시킵니다. 또한, 결과가 예비적인 단계임을 겸허히 인정하면서도, 이 접근 방식이 트레이스 무결성을 가정하는 현재의 최신 기술들에 비해 "더 원칙적이고 유망한 방향"을 제시한다고 밝히고 있습니다. 향후 과제로 학습된 사양을 그라운드 트루스와 정량적으로 비교하기 위한 공식적인 거리 척도 개발을 꼽았습니다.