기술 요약: 가중 오토마타의 SMT 기반 능동 학습

문제 정의

Angluin 의 $L^\star$ 알고리즘이 선구자가 된 능동 오토마타 학습은 형식적 검증에서 알려지지 않은 구성 요소의 모델을 추론하는 표준 기법이 되었습니다. $L^\star$ 스타일 방법은 부울 오토마타 (결정론적 및 비결정론적) 에 대해서는 잘 정립되어 있지만, 이를 가중 유한 오토마타 (Weighted Finite Automata, WFAs) 로 확장하는 것은 훨씬 더 어려운 것으로 입증되었습니다. WFAs 는 전이에 반환환 (semiring) 에서의 가중치를 할당함으로써 부울 오토마타를 일반화하며, 비용, 확률, 자원 소비와 같은 정량적 특성을 모델링할 수 있게 합니다.

WFAs 학습에 대한 기존 접근법은 Hankel 행렬 또는 관찰 테이블의 일반화 (예: $WL^\star$) 에 의존합니다. 이러한 방법들은 기반 반환환의 대수적 구조에 대한 추론을 요구합니다. 결과적으로, 종료성과 최소성을 증명하는 것은 미묘하며 종종 특정 대수적 클래스 (예: 체, 주 아이디얼 정역) 로 제한됩니다. Tropical 반환환이나 Bottleneck 반환환과 같이 실제적으로 관련이 많은 많은 반환환의 경우, 종료성 보장은 알려지지 않았거나 최소 오토마타를 보장하지 않습니다. 또한, 기존 알고리즘들은 종종 비최소 모델을 생성하거나 무한 반환환 위에서 효과적으로 확장되지 못합니다.

방법론

저자들은 SMT (Satisfiability Modulo Theories) 솔버로 해결 가능한 만족도 문제로 학습 문제를 직접 변환하는 새로운 제약 기반 능동 학습 알고리즘을 제안합니다.

핵심 접근법

관찰 테이블을 정제하는 대신, 이 알고리즘은 주어진 반환환 $S$ 위의 방정식 시스템을 점진적으로 구성합니다. 이 시스템의 해는 관찰된 모든 쿼리에 대해 "교사" (대상 언어) 와 일치하는 비결정론적 WFA에 정확히 대응합니다.

학습 과정은 표준 능동 학습 루프 (알고리즘 1) 를 따릅니다:

1. 가설 생성: 알고리즘은 현재 관찰 집합 $O$와 일관된 $n$-상태 WFA 를 찾으려 시도합니다. 이는 getAutomaton 서브루틴에 위임됩니다.
2. 동치 쿼리: 일관된 가설 $H$가 발견되면, $H$가 대상 언어 $L$을 인식하는지 확인하기 위해 교사에게 질의합니다.
3. 반례 처리: 교사가 반례 $w$ ($H(w) \neq L(w)$) 를 제공하면, $w$가 $O$에 추가되고 강화된 제약 조건으로 루프가 반복됩니다.

getAutomaton 서브루틴

이 논문은 getAutomaton 에 대한 두 가지 구현을 제시합니다:

1. 순수 베이스라인: WFA 의 의미론을 직접 인코딩합니다. 초기 가중치, 전이 행렬, 최종 가중치를 미지 변수로 취급하고 모든 $w \in O$에 대해 $out(w) = \text{semantics}(w)$ 방정식을 풉니다.
2. 최적화된 (SWAL): 코대수적 관점과 상태 언어 개념을 활용합니다. 전체 언어를 직접 푸는 대신, 각 상태에서 받아들여지는 언어를 나타내는 중간 변수를 도입합니다. 그 결과 다음과 같은 방정식 시스템이 도출됩니다:
   • 안정화 제약 조건은 상태 언어가 전이 가중치와 일관되도록 보장합니다.
   • 스패닝 제약 조건은 초기 가중치가 상태 언어를 올바르게 결합하여 대상 출력과 일치하도록 보장합니다.
   • 핵심 통찰: 이 인코딩은 더 많은 변수와 방정식을 도입하지만, 관찰 간의 공유된 하부 구조 (접미사) 를 노출시킵니다. 이는 SMT 솔버가 중간 결과를 재사용할 수 있게 하여, 순수 접근법보다 확장성을 크게 향상시킵니다.

결정 가능성과 반환환

이 알고리즘은 반환환에 대해 매개변수화됩니다. 저자들은 결정 가능한 반환환 (유한 방정식 시스템의 만족도가 결정 가능한 경우) 의 경우 getAutomaton 서브루틴을 정연하고 완전하게 구현할 수 있음을 확인합니다.

• 유한 반환환: 브루트포스 또는 SMT 를 통해 자명하게 결정 가능합니다.
• 무한 반환환: 이 논문은 Tropical 반환환 ($\min, +$), 유계 Tropical 반환환, 그리고 Bottleneck 반환환 ($\max, \min$) 을 Quantifier-Free Linear Integer Arithmetic (QF-LIA) 및 Quantifier-Free Bit-Vectors (QF-BV) 와 같은 결정 가능한 이론으로 인코딩하는 방법을 제공합니다.

주요 기여

1. 새로운 알고리즘: 반환환에 대해 매개변수화된 비결정론적 WFA 를 위한 새로운 SMT 기반 능동 학습 알고리즘.
2. 최소성 보장: 특정 대수적 구조 밖에서는 최소성 보장이 종종 결여된 $L^\star$ 스타일 방법과 달리, 이 알고리즘은 종료 시 최소 WFA 를 생성할 것임이 보장되며, 이는 반환환에 관계없이 적용됩니다.
3. 종료 조건: 저자들은 부분 정확성을 증명하고 종료에 대한 충분 조건을 제공합니다. 구체적으로, 모든 유한 반환환에 대해 알고리즘이 종료함을 증명합니다. 무한 반환환의 경우, 같은 기수론적 논거로는 이론적 종료 보장이 제공되지 않지만, 구현은 실제적인 성공을 보여줍니다.
4. 제약 기반 합성: 이 논문은 SMT 기반 합성을 가능하게 하는 최초의 WFA 를 위한 제약 기반 생성 알고리즘을 도입합니다. 이는 결과 제약 시스템이 결정 가능한 특정 반환환들을 식별합니다.
5. 실험적 평가: 제안된 방법 (SWAL) 을 순수 베이스라인 및 최첨단 $WL^\star$ 알고리즘과 비교한 포괄적인 평가.

실험 결과

저자들은 OCaml 로 Z3 솔버를 사용하여 알고리즘 (SWAL) 을 구현하고, 부울, Tropical, 유계 Tropical, 그리고 Bottleneck 반환환에 걸쳐 5,000 개 이상의 무작위 생성된 벤치마크에 대해 평가했습니다.

• 순수 베이스라인 대비: SWAL 은 런타임과 확장성 모두에서 순수 인코딩을 크게 능가합니다. 순수 접근법은 (반환환에 따라) 2~6 개 이상의 상태를 가진 오토마타 학습에 어려움을 겪는 반면, SWAL 은 최대 8 개 상태의 최소 오토마타를 성공적으로 학습합니다. 최적화된 인코딩 (상태 언어) 은 타임아웃/메모리 부족 오류 수를 수 차례 감소시킵니다.
• $WL^\star$ 대비: 주 아이디얼 정역을 위한 최첨단 알고리즘인 $WL^\star$와 비교했을 때:
  • 최소성: SWAL 은 일관되게 최소 오토마타를 생성하는 반면, $WL^\star$는 종종 10 배까지 큰 오토마타를 생성합니다.
  • 효율성: SWAL 은 $WL^\star$보다 적은 출력 쿼리 (교사와의 상호작용) 를 요구합니다.
  • 런타임: SWAL 은 런타임 면에서 경쟁력이 있으며, 종종 $WL^\star$보다 빠르게 종료하고 더 적은 자원 실패 (TO/OOM) 를 보입니다.
• 증분성: 증분 SMT 풀기를 활성화하면 학습 시간과 자원 사용량이 극적으로 감소하여, 제약 기반 접근법이 증분 학습에 적합함을 확인시켜 줍니다.

중요성과 주장

이 논문은 제약 기반 학습을, 특히 검증 지향적 설정에서 전통적인 Hankel/$L^\star$ 스타일 방법에 대한 실용적이고 견고한 대안으로 위치시킵니다.

• 견고성: 이 접근법은 $L^\star$ 스타일 방법에 대한 대수적 종료 증명이 어렵거나 존재하지 않는 더 넓은 범위의 반환환 (Tropical 과 같은 무한 반환환 포함) 을 처리합니다.
• 최소성: 최소성 보장은 효율적인 검증과 추상을 위해 필수적인 최소 모델이므로 중요한 장점입니다.
• 확장성: 실험 결과는 SMT 기반 합성이 기존 알고리즘으로는 현재 도달할 수 없는 복잡하고 최소인 가중 오토마타를 학습할 수 있을 정도로 확장 가능함을 보여줍니다.

저자들은 모든 무한 반환환에 대한 일반적인 종료 증명을 제공하지는 않지만 (알려진 미해결 문제), 이전 방법들이 실패하거나 비최적 모델을 생성하는 시나리오에서 최소 WFA 를 성공적으로 학습하는 실용적인 해결책을 제공한다고 결론지었습니다. 향후 작업으로는 더 많은 증분 가설 업데이트를 탐색하고 확률적 오토마타로 접근법을 확장하는 것을 포함합니다.