기술 요약: 정형 검증된 마르코프 사용 모델의 뉴로-심볼릭 합성

1. 문제 정의

**모델 기반 통계적 테스팅(MBST)**의 광범위한 채택을 가로막는 주요 병목 현상은 **마르코프 체인 사용 모델(Markov chain usage models)**의 수동 구축 과정입니다. 이러한 모델은 테스트 목적을 절대적인 코드 커버리지에서 기대되는 필드 품질에 대한 통계적 추론으로 전환하는 데 필수적입니다. 그러나 모호하고 구조화되지 않은 자연어 요구사항을 검증된 상태 전이 토폴로지와 수학적으로 일관된 확률 행렬로 변환하려면 상당한 형식 방법론(formal methods) 전문 지식이 필요합니다.

대규모 언어 모델(LLM)이 구문 추출 능력은 입증했으나, 순수 신경망 접근 방식은 MBST 적용 시 네 가지 결정적인 한계점을 보입니다:

1. 확률적 변동성 및 환각(Stochastic Volatility & Hallucination): LLM은 중요한 엣지 케이스를 누락하거나, 불가능한 전이를 생성하거나, 시스템 불변량(invariants)을 위반하여 유효하지 않은 테스트 케이스를 생성할 수 있습니다.
2. 캘리브레이션 실패(Calibration Failure): LLM은 정밀한 수치 추론에 어려움을 겪으며, 행-스토캐스틱 제약 조건($\sum_j p_{ij} = 1$)이나 유효한 마르코프 체인에 필요한 복잡한 다변수 제약 조건을 충족하지 못하는 경우가 많습니다.
3. 상태 공간 폭발(State-Space Explosion): 유한한 컨텍스트 창 내에서 작동하는 LLM은 구조적 일관성을 잃으면서 고도로 동시적인 다중 스트림 전이 모델을 효과적으로 추적하거나 생성할 수 없습니다.
4. 의미적-실행 가능성 괴리(Semantic-Feasibility Divergence): LLM은 의미적 진행에는 뛰어나지만 물리적 및 논리적 실행 가능성 제약(예: 장바구니가 비어 있는 상태에서 결제 전이 실행)을 빈번히 위반하여, 의미적으로는 논리적이지만 물리적으로는 실행 불가능한 경로를 생성합니다.

기존 문헌에는 자동화된 모델 구축이 MBST의 결함 탐지 보증에 필요한 구조적 및 확률적 특성을 유지할 수 있는지에 대한 엔드 투 엔드 평가가 부족합니다.

2. 방법론: NeSy-MBST 프레임워크

본 논문은 의미론적 파싱과 수학적 제약 해결을 분리하는 하이브리드 프레임워크인 **뉴로-심볼릭 모델 기반 통계적 테스팅(NeSy-MBST)**을 소개합니다. 이 아키텍처는 밀접하게 결합된 5단계로 구성됩니다.

A. 진행-실행 가능성 이중 메모리 아키텍처 (Progress-Feasibility Dual-Memory Architecture)

시스템은 모델 구축을 두 개의 상호 보완적인 메모리 시스템으로 분할합니다:

• 신경 진행 메모리(Neural Progress Memory): 미세 조정된 LLM이 자연어 요구사항을 파싱하여 의도된 행동 토폴로지를 포착하는 의미적 흐름 그래프(the "what")를 초안합니다.
• 심볼릭 실행 가능성 메모리(Symbolic Feasibility Memory): 규칙 기반 엔진이 엄격한 논리적 불변량, 전제 조건 및 전이 가드(the "how")를 강제하여, 후보 전이가 수용되기 전 모든 전이를 검증합니다.

B. LLM 오라클을 통한 능동적 오토마타 학습 ($L^*$ with LLM Oracles)

프레임워크는 상태 공간을 발견하기 위해 특화된 $L^*$ 능동 오토마타 학습 알고리즘 변형을 사용합니다.

• 멤버십 쿼리(Membership Queries): 알고리즘은 (출력 제한: Yes, No, Unsure)을 갖는 문법 제약 LLM 오라클에 쿼리를 보내 특정 입력 시퀀스가 수용되는지 확인합니다.
• 동등성 쿼리(Equivalence Queries): 현재의 가설 오토마타를 실제 테스트 대상 시스템(SUT)과 비교합니다. 여기서 발생하는 편차는 가설을 정교화하기 위한 반례(counterexamples)로 사용됩니다.
• 에스컬레이션(Escalation): LLM이 "Unsure"를 반환하면, 해당 쿼리는 인간 전문가나 SUT 런타임 실행으로 에스컬레이션되어 학습 루프에 검증되지 않은 정보가 포함되지 않도록 보장합니다.

C. 경로 의존적 계층적 모델링 (Path-Dependent Hierarchical Modeling)

경로 의존성으로 인한 조합 폭발 문제를 해결하기 위해 NeSy-MBST는 2계층 구조를 사용합니다:

1. 상위 트리 구조(Upper Tree Structure): 빈번하고 경로 의존적인 시퀀스는 트리에 임베딩된 고차 마르코프 체인으로 모델링됩니다.
2. 하위 마르코프 모델(Lower Markov Model): 드물거나 예외적인 경로는 표준 1차 마르코프 체인을 사용하여 모델링됩니다.

D. 수학적 제약 최적화 (Mathematical Constraint Optimization)

LLM에게 직접 수치적 확률을 생성하도록 요청하는 대신, 프레임워크는 이를 심볼릭 솔버에 위임합니다:

1. 제약 추출(Constraint Extraction): LLM은 요구사항으로부터 비교 관계(예: $P(\text{checkout}|\text{cart}) > P(\text{browse}|\text{cart})$)를 추출합니다.
2. 볼록 최적화(Convex Optimization): 볼록 프로그래밍 엔진(SLSQP)이 추출된 모든 제약 조건, 행-스토카스틱성 및 도메인 특정 경계를 만족하면서, 부당한 편향을 피하기 위해 엔트로피를 최대화하는 전이 확률 행렬 $P$를 계산합니다.

E. 폐쇄 루프 모델 적응 (Closed-Loop Model Adaptation)

프레임워크는 사용 모델을 살아있는 산출물로 취급합니다. 런타임 텔레메트리(실행 로그, 커버리지 메트릭, 실패 데이터)가 모델링 엔진으로 피드백됩니다. LLM은 예측된 행동과 관찰된 행동 사이의 편차를 분석하고, 심볼릭 솔버는 확률을 재조정하여 모델이 실제 사용 패턴에 수렴하도록 보장합니다.

3. 주요 기여

• NeSy-MBST 프레임워크: $L^*$ 능동 학습, 문법 제약 LLM 오라클, 심볼릭 솔버 및 폐쇄 루프 피드백을 결ongs하여 사용 모델 합성을 자동화하는 새로운 아키텍처를 제시합니다.
• LLM 출력의 형식 검증: 구조적 위반(도달 불가능한 상태, 누락된 셀프 루프)을 감지하고 타겟팅된 재-프롬프팅을 트리거하는 심볼릭 검증 루프를 도입하여, 회상(recall) 제한적인 생성 문제를 검증 가이드형 완성 문제로 전환합니다.
• 오쏘고날한 오류 분해(Orthogonal Decomposition of Errors): 본 논문은 구조적 완전성(토폴로지)과 확률적 캘리브레이션(가중치)이 서로 독립적인 속성임을 입증하며, 이를 각각 심볼릭 루프와 볼록 최적화기를 통해 별도로 처리함을 보여줍니다.
• 실증적 검증: 자율주행 차량(AV) CPS 벤치마크와 두 가지 이커머스 명세를 대상으로 한 종합적인 평가를 통해, NeSy-MBST를 순수 신경망 베이스라인 및 전통적인 수동 방식과 비교하였습니다.

4. 실험 결과

AV CPS 벤치마크(9개 상태, 13개 전이) 및 이커머스 모델(최대 42개 상태, 218개 전이)에 대해 평가한 결과, NeSy-MBST는 다음과 같은 성과를 거두었습니다:

• 추출 정확도 (RQ1): 시스템 레벨 F1 점수 0.9125를 달성하여, 안전 필수 임계값인 0.90을 초과했습니다. 이는 가장 강력한 단일 모델 베이스라인인 Claude 3.5 Sonnet보다 14.8%, 하이브리드 SMF(GPT-4o 기반)보다 39.1% 향상된 수치입니다.
• 결함 탐지 커버리지 (RQ2): 85.7%의 전이 커버리지를 달성하였으며, 이는 순수 신경망 베이스라인(50%) 대비 35.7 퍼센트 포인트 상승한 수치입니다. 이는 결함 유발 경로의 다양성이 크게 증가했음을 시사합니다.
• 확률적 캘리브레이션 (RQ3): Jensen–Shannon 발산(JSD) 0.012를 달성하여(순수 신경망 베이스라인 0.157 대비), 볼록 최적화기가 운영 테스트 할당의 충실도를 보존함을 확인했습니다. 정규화된 프로베니우스 거리(Frobenius distance)는 0.0654로, 참조 분포와 높은 구조적 유사성을 보였습니다.
• 효율성: 최대 42개 상태를 가진 모델에 대해 6분 이내에 전체 모델 커버리지 테스트 스위트를 생성했습니다.
• 절제 연구 (Ablation Study, RQ4):
  • 심볼릭 루프가 구조적 완전성(전이 F1을 0.78에서 0.96으로 증가)의 핵심 동인임을 확인했습니다.
  • 볼록 최적화기는 구조적 메트릭을 변경하지 않고 확률적 캘리ibr레이션을 제어하는 역할을 수행했습니다.
  • 폐쇄 루프 피드백은 분포 충실도 측면에서 미미한 개선을 제공했으며, 주로 장기적인 테스트 캠페인에서 가치가 있었습니다.

5. 의의 및 주장

본 논문은 NeSy-MBST가 안전 필수 사이버 물리 시스템(CPS)이 요구하는 통계적 엄밀성을 훼손하지 않으면서도 수동 모델링의 병목 현상을 제거한다고 주장합니다.

• 격차 해소: 결과는 뉴로-심볼릭 통합이 순수 신경망 접근 방식이 달성하지 못한 구조적 충실도(F1 $\ge$ 0.90)와 확률적 캘리브레이션을 달성할 수 있음을 입증합니다.
• 결함 탐지의 대리 지표: 본 연구가 직접적인 결함 주입 코퍼스에 대한 결함 탐지율을 측정하지는 않았으나, 관찰된 35.7%의 전이 커버리지 증가는 결함 탐지에 대한 강력한 대리 지표이며, 이는 산업적 MBT 배포 문헌에서 보고된 25~40%의 개선 수치와 일치합니다.
• 엔지니어링 표준: 저자들은 LLM을 통한 형식 테스트 모델 생성이 단순한 연구적 호기심을 넘어 표준 엔지니어링 관행으로 전환되어야 한다고 제안하며, 이를 위해 두 가지 조건이 충족되어야 한다고 명시합니다: (1) 환각을 방지하기 위해 LLM이 구조적 제약(문법 제약 출력, 심볼릭 검증) 하에 작동해야 하며, (2) 수치적 파라미터는 LLM이 직접 생성하는 것이 아니라 인증된 솔버에 의해 할당되어야 합니다.

결론적으로, 이 접근 방식은 엄격한 통계적 테스팅을 전문적인 안전 필수 팀을 넘어 더 넓은 소프트웨어 개발 관행으로 확장 가능하게 만들며, 향후 더 큰 규모의 산업 시스템 및 다양한 요구사항 스타일에 대한 검증이 필요함을 인정하며 마무리됩니다.