2.1 추론 기반 주행과 추론 충실성

DriveLM은 지각·예측·계획의 질의응답을 그래프로 연결하고, DriveVLM은 장면 설명·분석·계층적 계획을 결합한다^{[1], [2]}. Alpamayo-R1은 CoC 추론과 궤적 예측을 결합하고, 지도 학습과 강화 학습으로 추론과 행동의 정렬을 높인다^[3]. 이 연구들은 주행 판단을 학습 가능한 언어 표현으로 만드는 데 초점을 둔다.

생성된 추론이 실제 판단을 반영하는지는 별개의 문제다. Turpin 등은 사고 과정 설명이 답에 영향을 준 요인을 빠뜨릴 수 있음을 보였고^[5], Lanham 등은 예측이 제시된 추론에 실제로 의존하는지를 측정했다^[6]. 주행 분야에서 Drive the Thoughts는 VLA 추론과 예측 궤적의 일관성을 실행 중에 감시하는 모니터를 제안했다^[7]. 언어 근거와 장면·궤적의 충실성 및 시각 교란에 대한 반응을 평가하거나^[8], 모순·환각 지표와 CoT 개입을 함께 사용하는 연구도 있다^[9].

이 연구들은 한 장면에서 설명이 행동과 맞는지, 또는 설명을 바꾸면 행동이 달라지는지를 묻는다. 본 연구는 모델을 다시 실행하거나 개입하지 않고, 저장된 연속 설명에서 앞선 의무와 뒤따르는 해제 근거를 연결한다. 따라서 생성 모델의 인과적 충실성을 검증하는 방법을 대신하지 않는다.

2.2 교통 규칙의 형식화와 검증

허용되는 주행 행동을 형식적으로 표현하려는 연구가 있다. Esterle 등은 교통 규칙을 선형 시간 논리(LTL)로 기술했고^[10], Maierhofer 등은 고속도로 규칙을 시간 논리로 형식화하여 준수 여부를 평가했다^[11]. RSS는 안전 행동과 책임의 수학적 조건을 정의한다^[20]. 형식화된 규칙 자체를 검증하는 연구도 있다. Wan 등은 등가성 검증과 모델 검사로 디지털 교통 규칙의 의미 일관성과 정확성을 확인했다^[12].

이 연구들의 검사 대상은 사람이 정한 규칙이다. 본 연구의 대상은 모델이 자동 생성한 주석에 암묵적으로 담긴 의무이다. 규칙이 미리 주어지지 않으므로, 의무가 언제 시작되고 무엇으로 해제되는지를 주석에서 읽어 내야 한다.

2.3 자연어 요구의 형식화

자연어 요구를 형식 명세로 옮기는 연구가 있다. NL2TL은 원자 명제를 추상화한 뒤 요구 문장을 시간 논리식으로 변환하도록 학습한다^[13]. nl2spec은 언어 구절과 하위 논리식의 대응을 보여 주어 사용자가 모호하거나 잘못된 번역을 고칠 수 있게 한다^[14]. 이 연구들의 주된 출력은 개별 요구 문장에 대한 형식 명세다.

연속 CoC에서는 한 문장이 만든 의무를 다른 문장이 해제하며, 해제 증거가 아예 없을 수도 있다. 본 연구는 원문 구절을 의무·해제 조건·증거에 연결해 남긴다는 점에서 nl2spec의 대응 추적과 목적이 비슷하다. 다만 범용 번역기를 제시하지 않으며, 본 평가의 프레임은 설계자가 작성했다.

2.4 실행 중 검증과 모델 검사

실행 중 검증(runtime verification)은 관측된 실행 경로가 주어진 명세를 만족하는지 검사한다^[15]. LTL/TLTL 모니터링은 유한 접두 경로에서 참·거짓·미결정을 구분하고 최초로 확정되는 시점을 다룬다^[16]. 따라서 이전 상태의 기억, 세 값의 판정과 최초 위반 추적 자체는 기존 기술이다. 본 논문의 미상 증거와 그에 따른 근거 부족 판정은 명시된 해제 증거가 없다는 뜻이며, 미래 연장 전체에 대한 LTL 세 값 의미론을 구현했다는 뜻은 아니다.

UPPAAL은 시간 오토마타의 상태와 도달 속성을 검사한다^{[19], [21]}. 본 연구의 모델은 사건 배열을 순서대로 처리하는 이산 관찰 모델이며, 시간 오토마타 도구를 사용했다고 해서 물리적 시간 제약을 검증한 것은 아니다. Scenic과 VerifAI는 상황을 생성하고 시뮬레이션하여 자율 시스템을 시험한다^{[22], [23]}. 본 연구는 환경을 탐색하지 않고 이미 기록되거나 작성된 사건 배열을 고정해 검사한다.

2.5 본 연구의 위치

기존 연구는 한 장면의 설명과 행동의 정렬, 사람이 정한 규칙의 형식화와 검증, 개별 요구 문장의 형식화, 그리고 형식 명세에 대한 경로 감시를 다룬다. 본 연구는 이들 사이에 남은 질문, 즉 자동 생성된 연속 주석에서 어떤 문장이 의무를 만들고 어떤 증거가 그것을 해제하는지를 연결하고 증거가 없는 경우를 모순과 구분하는 문제를 다룬다. 형식 검증 기술을 새로 만들었다고 주장하지 않으며, 다른 방법이 이러한 연결을 할 수 없다고 단정하지도 않는다. 단순 FSM도 같은 규칙을 실행할 수 있으며, UPPAAL은 이 규칙을 질의로 표현하고 진단 경로를 남기는 구현 수단이다.

선행 기술과의 구체적인 접점은 조건의 대응 관계다. 한 사건에 행동을 정당화하는 조건 B와 의무를 해제하는 조건 A가 함께 언급되면, 구절을 역할별로 분리해 같은 조건 ID의 증거만 해당 의무에 적용한다. 모델 질의의 결과는 그 대응을 전제로 한 실행 결과다. 이 구조는 “앞뒤 행동이 다르다”는 표시 대신 이전 요구가 아직 남았는지와 어떤 근거가 빠졌는지를 다시 읽게 한다. 표 1은 각 연구군의 입력·표현·출력과 본 논문의 범위를 정리한다.

3.1 평가 자료 개요

핵심 평가는 설계자가 구성한 시나리오와 유한 범위의 전수 사건열을 사용한다. 수집 CoC는 사람에 따른 해석 차이와 기록 궤적의 대응 범위를 살피는 자료이며, 수집 오류 정확도를 계산하는 정답집으로 사용하지 않는다. 표 2에 각 자료의 규모·작성 주체·역할과 결과 절을 정리했다.

144건은 영어 원문과 구조화 입력을 함께 작성했고, 81건은 원 자연어 구절 없이 대상·조건·경계 연결을 제공한 자료다. 81건은 경계 확장 모델과 함께 설계하여 검증 실행 전에 고정했으며, 모델 고정 이후 새로 작성한 독립 시험으로 보지 않는다. 전수 사건열은 두 모델과 생성 규칙을 고정한 뒤 모든 선언 조합을 열거했다. 구체적인 조합과 비교 방법은 6장에서 설명한다.

3.2 수집 자료의 출처와 선정

수집 자료는 nuScenes의 영상·자차 움직임과 사후 자동 생성한 CoC-Nusc 주석이다^{[24], [4]}. 기록 궤적에서 계산한 행동 정보가 주석 생성에 쓰이므로 CoC와 궤적의 일치를 독립 정답으로 사용하지 않는다. 보관된 주석은 743장면·3,218사건이며, 이 중 자차 궤적 파일을 함께 보유한 94장면·403사건을 분석에 사용했다. CoC가 둘 이상인 90장면에서 만든 309인접쌍은 사람 검토의 후보 선정에 사용했으며 전체 쌍의 오류율을 산출하지 않았다.

CoC-Nusc의 배포 버전, 생성 실행별 모델 버전, 생성 지시문과 설정은 복원하지 못했다. 자료 설명서에서 모델 계열은 확인되지만 개별 문장의 정확한 생성 이력과 품질 점수의 계산식·통과 기준은 확인할 수 없다. 자료 선정에는 보관된 품질 통과 표시를 사용했다(표 3).

보조 반응 분석에서는 403사건 중 품질 표시를 통과한 290건을 먼저 남겼다. 이 중 복합 행동이나 방향이 불명확한 156건을 제외한 134건을 사용했다. 134건은 속도 변화 탐지 대상 130건과 사건 시점에 이미 정지·양보 조건을 만족한 4건이다. 이 선정은 309인접쌍의 사람 검토 후보 선정과 별개다.

후보 선택기는 첫 문장에 정지·양보(stop/yield), 둘째 문장에 가속·진행(accelerate/proceed) 표현이 있는 쌍을 찾는다. 23쌍·15장면에서 장면별 가장 이른 창 하나를 선정했다. 비교군은 후보 장면을 제외하고 첫 문장에 정지·양보 표현이 있으나 둘째 문장에는 가속·진행 표현이 없는 창이다. 장면당 가장 이른 창을 남긴 뒤, 후보와의 사건 수 차이·정지/양보 종류 차이·원 사건 위치 차이 순으로 대응시켰다. 동률은 난수 시드 20260806과 창 ID의 해시로 결정하고 비교 창을 중복 사용하지 않아 12장면을 얻었다. 보존된 원 선정 프로그램을 다시 실행하면 기존 27개 검토 ID와 장면·집단 구분이 재현된다. 이 표본은 특정 행동 전환을 더 많이 포함하는 비무작위 표본이다.

309는 후보 선정에 사용한 인접 문장 쌍의 수이고, 27은 사람이 검토한 장면 묶음의 수다. 여러 사건이 한 장면에 속하므로 사건·쌍·장면을 독립 시행으로 합산하지 않는다.

3.3 사람 검토 절차와 기록의 한계

보존된 검토 지침과 A/B 화면에 따르면, 1차 검토에는 CoC 원문과 첫 사건 기준 상대 시각을 제시하고 별도의 영상·궤적·객체/신호 상태 자료와 검사기 결과는 제공하지 않았다. 후보군·비교군 구분과 원 장면 ID는 화면에 표시하지 않고 집단 정보가 없는 검토 ID를 사용했다. 네 검토자는 시간 요구의 명시성, 요구 행동열과 문장 일관성을 판정했으며, 지침은 외부 객체 상태가 필요하면 미상으로 남기도록 했다. 원 판정과 최종 합의 기록은 보존되어 있으나 검토자 자격·교육 이력·독립 중재자 참여 및 당시 논의 절차는 확인할 기록이 부족하다. 합의 기록은 27장면 모두 텍스트 모순 없음이며 사유 메모는 0/27이다. 따라서 이 자료는 독립적인 수집 모순 정답이 아니라 주석 해석의 불일치와 모호성을 살피는 데 사용한다. 추가 사람 재평가는 수행하지 않았다.

작성 시나리오와 40개 기준–변형 쌍, 검사 코드와 합성 사례 생성기, UPPAAL 모델과 질의, 실행 결과, 보존된 검토 지침과 익명 범주 판정표 및 일치도 재계산 코드는 심사 기간에 익명 저장소로 제공하고 게재 시 공개한다. 원 CoC 문장, 영상과 자차 궤적은 원 배포처에서 확보해야 하며, 검토자 식별 정보·자유 메모·원 장면 ID와의 대응은 제공하지 않는다.

4.1 기호와 입력

장면 $s$의 사건열을 $E_s=(e_0,\dots,e_{n-1})$라 한다. 사건 $e_i$는 행동 $a_i$, 새 의무 집합 $O_i$, 조건별 해제 증거 $q_i(c)$, 진행 선행조건 증거 $p_i$와 각 항목의 원문 구절을 가진다. $\text{GO}_i$는 진행·가속 단계에서 참인 지시값이다. 실험 인코더는 사건당 새 의무를 최대 하나 등록한다. 의무 $o$는 ID, 대상과 해제 조건 ID $c(o)$를 가진다. 증거는 참($\mathsf{T}$), 거짓($\mathsf{F}$), 미상($?$) 중 하나이며 각각 조건 충족 확인, 미충족 확인, 판단 근거 없음을 뜻한다. 초기 상태는

이다. 아래첨자 $-1$은 첫 사건 $e_0$를 처리하기 전의 초기 상태를 나타낸다. $?$는 증거가 없어 조건 충족 여부를 참이나 거짓으로 정할 수 없는 미상(Unknown) 값이다. 아직 사건의 증거를 읽지 않았으므로 초기 해제 증거 $q_{-1}^*(c)$와 선행조건 증거 $p_{-1}^*$를 모두 $?$로 둔다. $A_i$는 사건 $i$를 처리한 뒤 남은 의무 집합이다.

증거는 같은 조건 ID에만 적용한다. 녹색 신호 B는 진행의 근거가 될 수 있지만 보행자 통과 조건 A의 해제 증거를 대신하지 않는다. 중간 사건에 A의 증거가 없다는 이유만으로 A를 지우지 않으므로, 검사 단위는 의무의 생성·유지·해제 증거·후속 행동의 연결이다.

두 모델의 최종 판정은 확정 모순, 근거 부족, 양립으로 나눈다. 양립은 검사한 사건열에서 확정 모순과 근거 부족이 모두 발견되지 않은 경우다. 증거 값이 미상($?$)이라는 사실만으로 근거 부족을 판정하지 않는다. 예를 들어 보행자 통과 여부가 미상인 채 기다릴 때는 문제를 기록하지 않지만, 정지 의무가 남아 있고 해제 여부도 미상인 채 진행하면 근거 부족을 기록한다.

4.2 주석 문제와 검사기 처리 오류

표 4는 문제 유형과 구현별 검사 범위를 요약한다. P1–P3은 입력의 행동·요구 관계에 관한 문제이고 P4는 검사기의 상태 처리 문제다. P5는 별도의 속도 반응 시간 검사다. 기존 40쌍을 이 구분으로 재집계한다.

$A_i^-$는 새 의무와 해제 증거를 반영한 뒤 현재 행동 직전에 남은 의무 집합이다. $q_i^*, p_i^*$는 최근의 알려진 증거다. $\text{release}_i(o)$는 의무 $o$의 해제를 선언·처리했음을 나타내는 개념적 기호이며, 기존 회귀 입력의 해제 조건 관측값과 구분한다.

P1은 미해제가 확인된 의무와 진행의 충돌, P2는 미충족 조건에서의 조기 해제, P3은 선행조건 미충족 상태의 진행이다. F4는 이전 활성 의무의 해제가 확인되었는데도 이를 처리 후 상태에 남기는 오류다. M은 진행 시 해제 근거 부족이며 확정 모순에 포함하지 않는다.

조건 연결·경계 확장 모델은 별도 해제 명령을 입력받지 않으므로 P2 자체를 평가하지 않는다. 미해제 의무를 남긴 채 진행하는 충돌은 P1로 검사하지만 두 문제를 동치로 보지 않는다. 기존 회귀 경로의 P2 표시는 C2의 독립적인 의미 정답이 아니며 구현 규칙은 7.1절에서 설명한다. 조건 연결 모델의 144/144를 P1–P4 전체에 대한 새 성능으로 해석하지 않는다.

4.3 조건 연결 모델의 갱신과 판정

조건 연결 모델은 새 의무 등록, 증거 갱신, 해제, 진행 검사 순으로 처리한다. 미상 입력은 최근의 알려진 증거를 덮지 않는다.

정상 갱신에서는 진행 검사가 의무 집합을 바꾸지 않으므로 $A_i=A_i^-$이다. 실제 처리 후 상태를 대조할 때 F4는 참 해제 근거가 있는 이전 활성 의무를 잘못 남긴 고장을 뜻하며, 모든 상태 갱신 오류를 포괄하지 않는다.

유효 증거가 미상인 활성 의무는 유지한다. 정지·대기 중의 미상 자체는 문제로 기록하지 않고, 진행할 때 남은 의무의 증거가 거짓이면 확정 모순, 미상이면 근거 부족이다. 선행조건은 저장된 값 $p_i^*$가 거짓일 때만 P3으로 판정하며, 미상인 채 진행하는 경우를 별도 근거 부족 사유로 세지 않는다. 복수 의무는 자기 조건으로 각각 확인하고 하나의 해제가 다른 의무를 지우지 않는다. 모순과 근거 부족이 함께 생기면 두 기록을 모두 보존한다. 전체 판정은 누적 확정 모순이 있으면 확정 모순, 그것 없이 근거 부족이 있으면 근거 부족, 둘 다 없으면 양립이다.

이 보존 규칙은 같은 대상·조건과 증거 유효 구간이 유지된다는 가정에 의존한다. 실제 객체 추적·증거 만료는 모델링하지 않으며 새 의무 등록 때 이전 증거를 초기화하지 않는다. 따라서 생성 전에 받은 참 증거나 이전 생애주기의 참 증거가 새 의무에 재사용되어 즉시 해제될 수 있다. 144건에는 같은 ID의 재생성이 없지만 유한 전수시험에는 반복 생성이 포함된다. 불일치 0은 이 재사용 정책과 구현의 적합성이지 정책의 현실 타당성이나 두 모델의 동등성 근거가 아니다.

장면 끝에서 미래 해제를 보지 못했다는 이유만으로 모순을 추가하지 않는다. 미상 상태에서 진행하지 않고 끝난 대기열은 양립일 수 있다. 일정 시간 안에 의무가 반드시 끝나야 한다는 속성은 검사하지 않는다. 이 모델은 다음 장면과의 연결을 다루지 않고 장면마다 상태를 초기화한다.

4.4 경계 확장 모델

경계 확장 모델은 연결 상태·증거 만료·재활성화 초기화를 다루는 별도 구현이며 선행조건 검사는 포함하지 않는다. 경계에서 의무별 대상·적용 범위 연결 상태 $b_i(o)$와 증거가 경계를 넘어서도 유효한지를 입력받는다. VERIFIED는 같은 대상과 적용 범위가 확인된 연결, ENDED는 적용 범위의 명시적 종료, UNCERTAIN은 확인되지 않은 연결이다. 이 값은 설계자가 제공하며 모델이 영상에서 추론하지 않는다.

갱신 순서는 경계 정책, 새 의무 활성화, 대응 증거 갱신과 해제, 진행 판정이다. 같은 사건의 새 의무는 새 적용 관계를 시작하며 이전 해제값을 재사용하지 않는다. 알려진 미해제 상태의 진행은 확정 모순, 연결 미확인 또는 해제 미상의 진행은 근거 부족이다. 두 문제가 공존하면 기록을 모두 보존하고 확정 모순을 최종 판정으로 우선한다. 연결 미확인 상태에서 받은 관측은 반영하지 않으며, 이후 VERIFIED 입력이나 새 활성화로 연결이 확인되면 새 대응 관측을 사용할 수 있다. 범위 종료와 전체 사건열 종료는 다르며 단순 장면 변경만으로 의무를 버리지 않는다. 비교 초기화 모델은 매 경계에서 기존 의무를 종료한다.

경계 처리를 반영한 행동 직전 상태를 $A_i^{B,-}, q_i^{B,*}$, 그 시점의 연결 확인 여부를 $\ell_i(o)$라 하면

를 검사한다.

$q_i^{B,*}$는 표 5의 초기화·관측 수용을 거친 증거로, 조건 연결 모델의 무조건적 최근값 보존과 다르다.

다른 문제 기록이 없을 때, 해제된 A를 새 증거 없이 재생성한 뒤 진행하면 조건 연결 모델은 과거 참을 재사용해 양립, 경계 확장 모델은 근거 부족으로 판정한다. 최초 생성 전에 받은 참 증거도 같은 차이를 만들 수 있다. 또한 선행조건 거짓의 진행은 전자에서 P3이나 후자는 이를 검사하지 않는다. 모든 연결이 VERIFIED이고 증거가 지속된다는 조건만으로 두 모델의 판정이 같지는 않다.

두 모델의 갱신 코드에서 ID당 생성 한 번, 생성 전 증거 없음, 모든 경계의 VERIFIED 연결과 지속 증거, 선행조건 항상 충족을 가정하면 생성 시 초기화·경계 처리·선행조건 검사가 차이를 만들지 않는다. 이는 코드에 근거해 정리한 공통 적용 조건이며, 이 조건에서 두 모델의 실행 결과를 직접 대조한 시험은 수행하지 않았다. 두 시험의 결과를 서로 다른 모델의 성능으로 옮겨 해석하지 않는다. 현 경계 시험은 종류별 하나의 조건을 다루며 동종 다중 객체 추적이나 임의 제약의 동시 만족 가능성을 검증하지 않는다.

4.5 최초 문제 위치와 반응 시간 질문

조건 연결 모델의 확정 모순과 근거 부족 최초 사건은 따로 기록한다.

경계 확장 모델에서는 각각 $\min\{i : C_1^B(i)\}$와 $\min\{i : M^B(i)\}$를 쓴다. 해당 집합이 비면 최초 위치는 없다. 최종 확정 모순에는 최초 모순 사건을, 확정 모순 없이 근거 부족만 있으면 최초 근거 부족 사건을 대표 위치로 사용한다. 뒤의 정상 해제도 앞서 근거 없이 진행한 기록을 지우지 않는다. 현재 활성 의무와 전체 경로의 문제 기록은 서로 다르다.

보조 질문 P5는 사건 시각 $\tau_i$, 요구 행동 $a_i$, 선택한 제한 시간 $D$와 속도 반응 조건 $R_{a_i}$에 대해

를 확인한다. 속도 탐지 코드에 맞춰 제한 시각을 포함하며 $t_r$은 반응의 시작 시각이다. 기록 속도에서 찾은 $t_r$은 객체 해제 조건 A의 충족 증거가 아니다. P5는 조건 연결 모델의 정량 시계 속성이 아니라 기록 반응의 별도 분석이다. 문장열의 의무 양립성과 선택한 시간 설정에서의 자차 반응은 서로 다른 질문이다.

5.1 처리 절차

제안 절차는 서론의 세 단계를 따른다(그림 2). 첫째, 같은 장면의 사건 순서를 고정하고 원 사건 ID, 원문, 자료 출처를 보존한다. 한 문장에 “정지한 뒤 진행”처럼 여러 단계가 있으면 같은 원문을 가리키는 단계들이 생기므로 사건 위치와 단계 위치를 함께 기록한다. 둘째, 각 사건의 행동, 의무, 해제 조건, 선행조건, 조건별 증거를 프레임에 담고 각 항목에 근거 구절을 연결한다. 셋째, 4장의 규칙으로 의무를 생성·유지·해제하며 진행 시점의 문제를 기록한다. 최종 판정뿐 아니라 최초 문제 사건, 관련 의무와 사유를 해당 원문 구절과 연결하여 제시한다.

그림 2 사건 고정–프레임 구성–판정과 기록의 세 단계. 자동 파서와 작성 프레임의 입력을 구분하고 판정 근거를 원문에 연결한다.

Fig. 2 Three stages: event ordering, frame construction, and checking with source-linked records

최초 시험, 개발 후 동일 사례 재시험, 수집 검토, 보조 반응 분석의 결과는 서로 다른 질문에 답하므로 따로 보고한다.

5.2 입력 표현: 자동 파서와 설계자 작성 프레임

144건 통제 시나리오의 주평가에는 설계자가 원문과 함께 작성한 프레임을 사용했다. 기존 자동 변환은 LLM 호출이나 수작업 정답 입력을 쓰지 않는 정규식 기반 영어 파서다. 이 파서를 거친 기존 자동 텍스트 경로는 144건 모두 미상 출력(UNKNOWN)을 반환했다(7.2절). 파서는 행동과 조건 구절의 후보를 찾지만 조건의 참·거짓 증거를 확정하지 않는다. 따라서 자연어로부터의 자동 의미 추출은 본 논문의 기여 범위에 포함하지 않는다. 파서의 규칙은 표 6과 같다.

파서의 네 행동은 기존 UPPAAL 경로에서 정지·정지 유지=0, 양보·감속=1, 가속·진행=2, 속도 유지=3으로 인코딩한다. 이는 표 8의 작성 프레임 코드와 구분한다.

수집 CoC에서 파서가 어디까지 처리하는지 확인하려고 사건이 둘 이상인 90장면의 원문 399건에 파서를 실행했다. 사건이 하나뿐인 4장면은 연속 사건 창에서 제외했다. 지원하는 행동을 인식한 원문은 230건, 인식한 행동이 없는 원문은 169건이었다. 추출한 행동 단계 265개 중 219개는 구문 해석을 마쳤고 44개는 대상 누락, 2개는 순서 모호였다. until 해제 조건은 0건, once/after 계기는 10건이었다. 이 수치는 구문 해석 단계의 집계이며 최종 판정 결과나 추출 정확도가 아니다.

표 7은 두 입력 경로를 나누어 보여 준다. (a)는 scene-0051의 실제 문장을 자동 파서와 기존 검사기로 처리한 사례이고, (b)는 설계자가 작성한 원문·프레임에서 조건 연결 모델의 인코딩·판정까지 이어지는 사례다. (a)에서 해제 증거가 미상이라는 것과 최종 판정은 다르다. 의무는 생성되었지만 이 문장 하나에는 진행 행동이 없으므로 확정 모순도 근거 부족도 기록되지 않는다. 이 의무가 언제 끝나는지는 원문에 없어서, 이 문장만으로는 이후 진행의 양립성이나 위반을 확정할 해제 근거를 얻지 못한다.

작성 프레임은 행동, 의무(ID·대상·조건 ID), 조건별 증거, 선행조건, 원문 구절 위치를 가진다. True/False는 작성 문장이 명시한 조건 상태이며 사람의 독립 센서 정답이 아니다. 같은 e1에 진행 구절, A의 상태 구절, B의 신호 구절이 있어도 각각 다른 역할과 조건 ID로 연결한다. A의 근거가 비어 있다고 해서 B를 A에 할당하지 않는다. 따라서 (b)의 세 변형은 GO와 B=참을 그대로 두고 A만 거짓·미상·참으로 바꾼 비교다. 판정의 차이는 이전 의무의 해제 근거에서 생긴다.

5.3 조건 연결 모델의 UPPAAL 구현

조건 연결 모델은 4.3절의 규칙을 하나의 관찰 템플릿으로 구현한다. 한 사례의 사건 수를 N, 의무 수를 K로 두고 의무 ID는 처음 등록된 순서대로 배열 인덱스에 대응시킨다. 표 8는 입력과 상태 변수를 정리한다.

그림 3 조건 연결 모델 XML의 두 위치와 전이. 의무 상태와 문제 기록은 변수로 관리 한다.

Fig. 3 The two locations and transitions in the condition-linked model XML. Obligation states and issue records are variables

active와 known은 역할이 다르다. 참 증거로 의무를 해제한 뒤에도 known은 기록으로 남는다. WAIT는 144건 작성 자료의 Maintain speed와 같은 유지·대기 단계를 나타내는 기호이며 실제 속도를 적분하지 않으므로 물리적으로 안전한 정지를 보장하지 않는다.

activate(creates[idx]);
update_known_precondition_if_present();
for j in obligation_registration_order:
    if observation(idx,j) >= 0: known[j] = observation(idx,j)
    if active[j] and known[j] == 1: active[j] = false
if actions[idx] == GO:
    record_bad_if(precondition == 0, PRECONDITION)
    for j in obligation_registration_order:
        record_bad_if(active[j] and known[j] == 0, j)
        record_missing_if(active[j] and known[j] == -1, j)

목록 1에서 증거 갱신과 해제가 진행 검사보다 먼저 일어난다. 같은 사건에서 선행조건 위반을 먼저, 의무 위반을 등록 순서대로 기록한다. 최초 의무 출력은 이 순서에 따라 하나만 선택되며 모든 관련 의무의 목록을 반환하지는 않는다. 미상 입력과 사건열 종료의 처리, 재생성 때 증거를 보존하는 정책은 4.3절의 정의를 따른다.

조건 연결 모델은 committed 위치 Run에서 idx<N이면 step()을 실행하고 인덱스를 늘리는 자기 전이를 하고, idx==N이면 Done으로 이동한다(그림 3). 시계와 환경 프로세스는 없다. 두 관찰 모델은 고정된 사건열을 결정적으로 처리하므로 입력마다 이산 상태 갱신 경로는 하나다. UPPAAL은 이 경로의 도달 상태에서 의무 위반, 근거 부족, 입력 처리 완료 속성을 검사한다. 이번 모델의 상태 공간이 선형으로 제한되었을 뿐이며 이 결과를 환경의 여러 가능한 행동이나 정량적 시간 속성을 검증한 것으로 확대 해석하지 않는다.

목록 2의 다섯 질의는 verifyta 5.0.0으로 실행했다. 표 9은 같은 순서로 각 질의의 뜻과 판정에서의 쓰임을 정리한다. 경로·상태 양화사의 의미는 공식 문서에 따른다^[21].

A[] not bad
A[] not missing
A<> Observer.Done
E<> Observer.Done && bad_hold
E<> Observer.Done && bad_pre

안전 속성의 반례가 알려 주는 최초 문제와 끝까지 처리한 뒤 누적된 사유는 범위가 다른 출력이므로 함께 읽는다. 진단 경로에서 얻은 최초 사건과 의무의 인덱스는 원래의 사건 ID와 의무 ID로 변환한다. 예를 들어 표 7(b)의 미해제 사례의 출력은 사건 e1, 의무 A, 미해제 의무 사유로 변환된다. 사건 ID를 원문 구절 위치와 연결하면 e1의 “Proceed”와 “The pedestrian is still crossing”, 그리고 e0의 “Stop until the pedestrian has passed”를 함께 제시할 수 있다. 원문 회수는 새 설명을 생성하는 과정이 아니라 보존된 대응을 따라가는 과정이다.

5.4 경계 확장 모델의 구현

경계 확장 모델도 Run/Done 구조와 사건 인덱스를 쓴다. 조건 연결 모델과 달리 의무별 연결 상태 linked[K]를 두고, 경계 입력 carry[N*K](같은장면=2, VERIFIED=1, ENDED=0, UNCERTAIN=−1)와 증거 지속 여부 persist[N*K]를 받는다.

경계에서 연결을 갱신한다. ENDED인 의무는 종료하고 확인되지 않았거나 만료된 증거는 미상으로 초기화한다. 새 의무를 생성하면 연결은 확인 상태로, 증거는 미상으로 시작한다. 이어서 연결이 확인된 의무의 관측만 갱신과 해제에 사용한다. 진행 시 활성 의무에 대해 연결이 확인되고 증거가 거짓이면 확정 모순이며, 연결이 미확인이거나 증거가 미상이면 근거 부족이다. 선행조건, P2 해제 명령, P4 고장 주입은 다루지 않는다.

질의는 목록 2의 앞 세 질의와 E<> Observer.Done && bad, E<> Observer.Done && missing이다. 마지막 두 질의로 종료 시점에 확정 모순과 근거 부족이 함께 있는지 확인한다. 이 모델의 의미와 조건 연결 모델과의 차이는 4.4절에서 설명했다.

5.5 비교 경로

비교 경로는 서로 다른 표현과 정책을 실행한다(표 10). 기존 두 구현은 최초 실패를 보존하려고 동결했다. 조건별 FSM은 별도의 단순 구현이며 144건의 조건별 의무를 처리한다.

기존 UPPAAL의 최초 반례 경로가 뒤에 생긴 미상 사유를 담지 못한 24건은 종료 상태에서 추가 질의를 실행해 진단했으며 원 파서는 바꾸지 않았다. 두 기존 구현의 일치는 고정 규칙을 똑같이 구현했다는 뜻이지 그 규칙이 독립적으로 타당하다거나 자연어 해석이 옳다는 뜻은 아니다. 보조 반응 모델은 질문과 입력이 다르므로 그 성공을 중심 문장 검사의 안전 검증으로 합치지 않는다.

6.1 기존 40쌍 회귀시험

기존 40개의 기준–변형 쌍은 유형별 10쌍을 직접 생성하고 검사기 자체로 기대 사후조건을 확인한 규칙 실행 회귀시험이다. 결과에 따른 후보 선별은 없지만 기대 판정의 확인에 검사기를 사용했으므로 독립 성능 평가로 보지 않는다. P1–P3의 주석 문제 시험 30쌍과 P4 처리 시험 10쌍을 나누어 보고한다. 현재 사건만 보는 검사는 이전 의무를 제거하여 기억의 효과를 확인하는 제거 비교(ablation)다.

6.2 144개 통제 시나리오의 최초 실행

통제 시나리오는 보행자, 자전거, 선행 차량, 교차 교통, 버스, 장애물의 6개 상황에 8개 변형(표 11)을 적용하고 중간 사건 0/2/6개와 교차시킨 144건이다. 각 변형은 18건이며 기대 분포는 확정 모순 72건, 양립 36건, 근거 부족 36건이다. 기대 판정, 최초 사건, 관련 의무, 사유는 최초 실행 전에 고정했고, 결과에 따라 사례를 선별하지 않았으며, 첫 결과에 맞지 않은 48건도 모두 보존했다.

간격은 초 단위 시간이 아니라 사이에 끼운 사건의 수다. 현재 미해제 변형은 진행 사건에 A=F가 다시 명시되지만, 이전 미해제 변형은 앞서 확인된 A=F를 중간 사건 뒤까지 보존해야 판정할 수 있다. 다른 대상 해제와 복수 의무 변형은 한 조건의 참 증거가 다른 의무를 지우거나 남기지 않는지 확인한다.

비교 경로. 같은 144건에 기존 전체 이력·현재 사건·이전 1/3/5개 사건 창·조건별 FSM·자동 텍스트·기존 UPPAAL 경로를 적용한다(표 10). 보조 반응 모델은 이 비교에 포함하지 않는다. 사건 창 비교는 기존 검사기에 잘린 이력을 제공한 제거 비교이며 독립된 경쟁 알고리즘이 아니다. 기존 전체 이력과 현재 사건·사건 창에는 단일 의무로 투영한 프레임을, FSM에는 조건별 프레임을 제공하므로 두 경로의 차이에는 기억 길이뿐 아니라 의무 표현 용량과 미상 누적 정책도 포함된다. 단일 의무만 지원하는 경로도 복수 의무 사례를 분모에서 빼지 않는다. 기존 자동 경로에는 원문만 제공했다. 전체 문장열을 입력받는 LLM 판정기와의 비교는 수행하지 않았다.

지표. 세 분류 일치는 기대 판정과 최종 판정이 같은 사례 수이며, 기존 출력 코드의 범주 대응은 7.2절을 따른다. 최초 위반 일치는 기대 확정 모순 72건 중 정확한 사건을 돌려준 수로, 분류를 맞혀도 위치가 다르거나 미상 출력으로 남기면 실패로 센다. 문제 위치·관련 의무·사유 일치는 확정 모순 72건과 근거 부족 36건을 합친 108건에서 각각 대조하여, 수정에 필요한 위치 정보를 실제로 돌려주는지 확인한다.

6.3 동일 사례 재시험과 기존 구현의 일치성

최초 불일치 48건의 원인을 분석한 뒤 조건 연결 모델을 개발하고, 기존 코드와 기대 판정을 바꾸지 않은 같은 사례 파일로 다시 시험했다. 따라서 이 시험은 개발 후 동일 사례 재시험이며 개발에 쓰지 않은 독립 시험이 아니다. 비교 항목은 6.2절의 세 지표와 같다.

기존 Python–UPPAAL 비교는 판정, 오류 종류, 최초 위치, 미상 사유를 항목별로 대조한다. 사유가 다른 사례는 최초 반례와 종료 상태를 따로 읽어 모델 의미의 문제인지 출력 범위의 문제인지 구분한다. 이는 구현 일치성 시험이며 규칙 자체의 독립 타당성을 검증하지 않는다.

6.4 장면 경계 시험

경계 시험 81건은 보행자 통과, 신호의 진행 허용, 장애물 해소라는 세 조건의 참·거짓·미상 전 조합 3³을 2장면과 3장면 구성에 적용한 54건과, 조건 종류마다 의무 유지, 다음 장면 해제, 근거 누락, 다른 대상 해제, 동일성 미확인, 근거 만료, 범위 종료, 재활성화 후 미해제·미상의 9개 변형을 적용한 27건이다. 입력, 기대 판정, 모델 파일은 검증 실행 전에 고정했고 결과에 따라 선별하지 않았다. 같은 입력을 유지 모델과 매 경계에서 의무를 버리는 초기화 모델에 넣어 총 162개 모델과 810개 질의를 verifyta로 실행했다. 초기화 모델은 기억의 효과를 보는 제거 비교다.

6.5 선별 없는 유한 범위 전수 시험

사례 선별의 순환성을 줄이기 위해 두 모델의 소스, 실행 당시의 판정 명세, 생성기, 수식 판정기를 저장소 커밋과 함께 해시로 고정한 뒤 유한 조합을 모두 열거했다. 행동은 STOP/WAIT/GO/YIELD(YIELD는 STOP과 같은 비진행 코드로 투영), 의무 생성 여부와 조건 ID, 조건별 참·거짓·미상을 조합한다. 조건 연결 모델에는 선행조건의 참·거짓·미상을, 경계 확장 모델에는 이후 사건의 경계 없음 또는 조건별 VERIFIED(순간 관측·증거 지속), ENDED, UNCERTAIN을 추가한다. 조건 연결 모델은 의무 1·2개에서 길이 1–3, 경계 확장 모델은 의무 1개에서 길이 1–3, 2개에서 길이 1–2를 실행 전에 고정한 범위로 열거한다. 여기서 의무 수는 사용할 수 있는 의무 ID의 수이며 모든 사건열에서 그 의무가 모두 생성되거나 동시에 활성화된다는 뜻은 아니다.

기대 판정은 손으로 부여하지 않았다. 별도의 수식 판정기는 접두열 전체에서 최근 알려진 증거, 마지막 의무 생성, 그 이후의 해제를 검색해 활성 상태와 모델별 판정식(C1,C3,M 또는 C1B,MB) 및 최초 문제를 계산하며, 모델의 상태 갱신 함수를 공유하지 않는다. 비교 대상은 고정된 모델 파일에서 변경 없이 추출한 갱신 함수를 C++로 실행한 경로다. 모든 접두열에서 의무·증거·연결 상태, 누적된 확정 모순과 근거 부족 기록, 각각의 최초 사건과 의무를 대조한다. P2의 해제 명령은 이 입력 형식에 없어 평가하지 않았다. P4는 참 증거가 있어도 의무 해제를 막는 처리 고장을 별도 대조군으로 넣고 길이 1–2를 전수 실행했다. 결과에 따라 사례나 기대값을 바꾸지 않았고 모든 불일치를 보존했다. 이 시험은 UPPAAL 탐색기를 새로 실행한 것이 아니며, 같은 연구진이 두 계산 경로에 관여했으므로 외부의 독립 의미 정답을 확보한 시험도 아니다.

6.6 수집 검토의 일치도 분석

3.3절의 27장면에 대한 네 검토자의 원 판정을 바꾸지 않고 시간 요구, 행동열, 텍스트 일관성 범주를 다시 집계한다. Fleiss κ, 평균 쌍별 일치율, 검토자별 분포를 보고하고, 범주 편중의 영향을 보기 위해 Gwet AC1을 함께 산출한다^[25]. 범주는 시간 요구 3개, 텍스트 일관성 5개, 행동열은 원 문자열 그대로 관측된 39개이며 “해당 없음”과 “미상”도 원 범주로 유지했다. 따라서 행동열 AC1은 관측된 범주에 한정한 요약이다. 다수결 라벨이나 합의 기록을 새 외부 정답으로 삼지 않는다.

6.7 궤적 대조와 반응 시간 분석

궤적 대조. 27장면의 각 사건에서 CoC가 요구한 행동(정지, 감속·양보, 속도 유지, 가속·진행)을 기록된 종방향 속도와 비교한다. 정지와 감속·양보는 같은 비진행 행동군으로 비교하므로 완전한 정지 여부는 확인하지 않는다. 지원 행동이 없거나, 문장 해석에 실패했거나, 복합 행동의 단계별 시점이나 관측 행동이 불명확하면 미상으로 둔다. 정지·양보 문장 뒤에 가속이 관측되어도 해제 근거가 없으면 미상으로 두며, 속도 변화로 해제 조건을 추정하지 않는다. 장면은 불일치 사건이 하나라도 있으면 불일치, 불일치 없이 미상 사건이 있으면 미상, 모든 사건이 일치하면 일치로 집계한다. 이 세 범주는 기록된 움직임과 문장 행동의 대응이며 4장의 확정 모순, 근거 부족, 양립과 다른 판정이다.

반응 시간 분석. 정지·양보 사건 시점의 속도가 $v \le 0.5\text{ m/s}$이면 먼저 이미 만족한 것으로 분류하고, 나머지 130건에서 속도 반응을 탐지한다. 기본 설정은 시작점 이후 관찰 구간 $W=0.5$초 안에서 속도 변화량이 $\delta=0.1\text{ m/s}$ 이상이고 방향이 일치하는 속도 증분의 비율이 $\rho=0.7$ 이상인 최초 시작점을 반응으로 본다. 시작점은 사건 시각부터 $D=3$초까지 경계값을 포함해 찾는다. 확인에 쓰는 관측 구간은 시작점 뒤까지 이어지므로 사후 분석이며 실시간 판정 지연을 평가하지 않는다. 이미 만족 규칙은 초기 후보를 검토한 뒤 추가했으며, 이 값들은 법규나 차량 안전 기준에서 가져온 것이 아니라 탐색 설정이다.

민감도 분석은 두 부분이다. 130건 전체에는 $D=3$초로 고정하고 $W \in \{0.25, 0.5, 1.0\}$초, $\delta \in \{0.05, 0.1, 0.2\}\text{ m/s}$, $\rho \in \{0.5, 0.7, 0.9\}$의 27개 조합을 적용해, 반응을 찾은 설정 수에 따라 항상 검출, 설정 의존, 항상 미검출로 나눈다. 기본 설정에서 제한 시간 안에 반응을 확인하지 못한 5건에는 $D=1, 2, 3, 4, 5$초와 위 27개 조합을 교차한 사건당 135개 조합을 추가로 적용했다. 반복 CoC는 최초 판단 시각부터 시간을 재는 방식과 반복 판단마다 시계를 다시 시작하는 방식을 비교한다.

7.1 기존 40쌍의 규칙 실행 결과

먼저 이전 의무를 기억하는 것이 필요한지를 문제 유형마다 한 항목만 바꾼 회귀 쌍으로 확인했다. 표 12에서 두 검사의 차이는 이전 사건의 정보가 있어야 판단할 수 있는 P1과 P4에서만 나타났고, 현재 사건에 판정 근거가 있는 P2와 P3은 두 검사가 모두 판정했다. 기준 사례에 확정 모순을 표시한 경우는 없었다. 합계 40/40과 20/40을 일반 오류 검출 정확도로 해석하지 않는다. 기존 검사기의 P2 표시는 진행 사건의 해제 조건 관측값 release=false에서, P4 표시는 같은 대상의 정지·양보 반복과 release=true가 함께 주어진 처리 변형에서 발생하므로, 명시적 해제 명령을 검사하는 C2나 사람의 실제 조기 해제를 확인한 결과와는 다르다.

7.2 최초 144개 작성 시나리오

기억이 필요하다는 것만으로 충분하지는 않았다. 의무가 여럿이거나 사건 간격이 길거나 해제 근거가 빠진 144개 시나리오에서는 전체 이력을 기억하는 기존 검사기도 96/144만 기대 판정과 일치했다(표 13). 이 집계는 기존 경로의 최종 출력 CONTRADICTION, UNKNOWN, CONSISTENT를 각각 확정 모순, 근거 부족, 양립에 대응시켜 센 것이다. 이하 UNKNOWN은 “미상 출력”이라 부르며, 구문 모호성·복수 의무·대기 중 미상까지 누적하므로 4장의 해제 근거 부족과 같은 의미는 아니다.

기존 전체 이력 경로에서 기대 확정 모순 72건은 확정 모순 54건과 미상 출력 18건으로, 기대 양립 36건은 양립 6건과 미상 출력 30건으로 나뉘었다. 기대 근거 부족 36건은 모두 미상 출력이었다. 따라서 세 분류 일치는 54+6+36=96건이다.

기존 경로의 실패는 잘못된 확정 모순이 아니라 판정하지 못한 미상 출력이었다. 기대 양립 사례에서 모순 오탐은 없었지만 대부분을 미상 출력으로 남겼으므로, 오탐이 없다는 사실만으로 성능을 판단할 수 없다. 사건 창은 간격이 길어질수록 이전 증거를 잃었지만, 창을 늘려도 전체 이력의 결과를 넘지 못했다. 즉 더 긴 문맥만으로는 복수 의무와 미상 누적의 문제가 해결되지 않는다. FSM은 144/144, 최초 위반 72/72였다. UPPAAL이 단순 비교기보다 정확하다는 근거는 없다. 원문만 입력한 기존 자동 텍스트 경로는 모든 사례에서 미상 출력을 반환했으므로 구조화 입력의 성공을 자동 추출의 성공으로 볼 수 없다.

7.3 실패 분석과 개발 후 동일 사례 재시험

7.2절의 불일치 48건은 기억의 길이가 아니라 의무를 표현하는 방식과 미상을 다루는 정책에서 생겼으며 세 유형으로 나뉜다(표 14). 동결된 기존 검사기는 활성 의무 하나와 6개 상태(INACTIVE, ACTIVE, SATISFIED_WAIT_RELEASE, RELEASED, VIOLATED, UNKNOWN)로 동작한다. 복수 의무는 하나의 채널에 담을 수 없어 미상으로 처리되었고, 대기 중의 해제 미상은 누적되어 뒤에 명시적으로 해제되어도 지워지지 않았다. 이는 작성한 의미와 기존 표현·정책의 불일치이며 수집 오류가 아니다.

조건 연결 모델은 의무별 활성 상태와 조건별 증거값을 나누어 복수 의무를 각각 판정한다. 또한 “해제 정보를 기다리는 단계”와 “해제 근거 없이 진행한 단계”를 구분해 후자에서만 근거 부족을 기록하고, 한 번 기록한 문제는 이후의 해제로 지우지 않는다(목록 1). 같은 144건의 재시험에서 이 모델은 판정뿐 아니라 최초 위반과 문제 위치·관련 의무·사유를 모두 기대대로 돌려주었다(표 15). 다만 같은 실패 사례를 모델 개발에 사용했으므로 개발에 쓰지 않은 독립 시험의 결과가 아니며, 자동 추출의 개선을 뜻하지도 않는다.

7.4 기존 Python–UPPAAL 출력 대조

7.2절의 불일치를 해석하기 위해 기존 두 구현의 출력을 대조했다. 같은 규칙을 구현한 기존 Python 검사기와 UPPAAL 모델은 모든 사례에서 판정, 오류 종류, 최초 위치가 같았다(표 16). 미상 사유가 일부 달랐던 것은 최초 반례의 접두 경로에 뒤에서 누적된 사유가 담기지 않기 때문이었고, 종료 상태의 추가 질의로 모두 일치했다. 따라서 이 차이는 출력 범위의 문제이며 7.3절의 의미 불일치와는 별개다.

7.5 장면 경계 결과(81건)

같은 질문은 장면 경계에서 다시 생긴다. 경계에서 의무와 증거를 버리면 장면을 넘어 이어지는 의무 위반을 판정할 수 있는가? 표 17에서 경계에서 상태를 유지하는 경계 확장 모델(이하 유지 모델)은 모든 사례를 기대대로 판정했지만, 경계마다 의무를 버리는 초기화 모델은 확정 모순과 근거 부족 사례의 대부분을 양립으로 판정했다. 예를 들어 세 장면에 걸쳐 마지막 진행 시점에 보행자 조건만 거짓이면 유지 모델은 남은 보행자 의무로 확정 모순을 기록하지만 초기화 모델은 양립으로 끝난다. 확정 모순과 근거 부족이 함께 생긴 사례에서는 두 기록을 보존하고 확정 모순을 최종 판정으로 택했다. 근거 만료 뒤의 진행은 근거 부족이 되고, 재활성화된 의무에는 과거 해제값을 쓰지 않는다. 재활성화 사례는 초기화 모델도 판정하므로 상태 유자의 이점으로 세지 않았다.

7.6 유한 범위 전수 적합성 결과

7.3절과 7.5절의 결과는 모두 설계자가 만든 사례에서 나왔다. 사례 선별의 순환성을 줄이기 위해 선언한 범위의 모든 사건열에서 구현과 수식 판정을 비교한 결과, 두 모델 모두 불일치가 없었다(표 18). 같은 비교에 P4 해제 고장을 넣은 대조군에서는 상태 불일치가 다수 나타나, 이 대조가 처리 오류를 구분할 수 있음을 확인했다. 표의 사건열 수는 열거한 조합의 수이며 수집 표본 수나 탐지 정확도의 분모가 아니다.

이 시험은 선언한 유한 범위를 전수 열거하여 사례 선별의 순환성을 줄이고 두 계산 경로를 비교한다. 그러나 수식과 구현이 공유하는 명세의 오류는 함께 남을 수 있다. 유한 상한 밖의 사건열이나 수집 문장의 의미 정답은 입증하지 않는다.

7.7 수집 검토의 일치도

작성 시나리오와 달리 실제 자동 생성 CoC에는 독립적인 기대 판정을 확보하지 못했다. 네 검토자의 원 판정도 크게 엇갈렸다.

표 19에서 텍스트 일관성의 κ는 0에 가까웠고 대부분의 장면에서 네 명의 판정이 달랐다. 표 20의 검토자별 분포도 모순이나 해당 없음을 고르는 경향이 크게 달라, 라벨 적용과 해석이 불안정했음을 보여 준다. 그 원인이 전문성이나 교육의 차이라고 확정할 수는 없으며, 분석 단위는 27장면이므로 판정 수를 독립된 정답 수로 세지 않는다.

AC1 추가 재분석은 세 항목 모두에서 Fleiss 계수보다 높았다. 범주 편중에 따른 보정 민감도이며 지침의 안정성이 개선됐다는 뜻이 아니다. 특히 시간 요구는 “있음”에 판정이 몰려 있어 같은 쌍별 일치율에서도 두 계수의 우연 일치 기대값이 크게 달랐다. 텍스트는 원시 일치 자체가 낮으므로 계수를 바꾸어도 해석이 달라지지 않는다. 기존 κ를 대체하지 않고 함께 보고한다.

원 메모에는 시간 요구가 없는 행동 조절, 해제 조건과 행동 순서의 구별, 선행 관계를 연결할 정보 부족 같은 해석이 남아 있다(표 21). 이는 개별 의견이며 합의 원인을 전수 분석한 것이 아니다. 합의 기록은 모두 모순 없음이지만 사유 기록이 없으므로 이를 객관적인 수집 정답으로 쓰지 않는다.

7.8 궤적과 보조 반응 결과

문장끼리의 일관성과 별개로 CoC가 요구한 행동이 기록된 자차 움직임과 맞는지도 확인했다. 그러나 대부분의 장면은 판단할 근거가 부족했고 반응 판정은 탐지 설정과 제한 시간에 따라 달라졌다.

27장면의 궤적 비교는 일치 2, 불일치 7, 미상 18이며 보존된 결과를 다시 실행해도 장면별 판정은 같았다. 표 22와 부록 표 25의 사유에서 보듯 미상의 주된 원인은 지원하지 않는 행동과 단계 시점·해제 근거의 부족이었다. 미상 장면 중 다수에는 일치 사건도 있었지만 다른 사건의 근거가 부족해 장면 판정을 확정하지 못했다. 따라서 현재 자료에서 궤적 대조를 확정할 수 있는 범위는 지원 행동과 관측 행동을 해석할 수 있고 단계 시점이 주어진 사건으로 제한된다. 불일치 장면은 문장 사이의 모순이나 위험 주행의 독립 정답이 아니다.

행동 방향이 분명한 보조 반응 분석 대상 134건은 기본 설정에서 반응 확인 125건, 사건 시점에 이미 만족 4건, 제한 시간 내 미확인 5건이었다. 탐지 대상 130건을 27설정에서 재집계하면 항상 검출 72, 설정 의존 57, 항상 미검출 1이다. 확인되지 않은 5건에서 반응이 검출된 조합은 $D=1, 2, 3, 4, 5$초에서 각각 3, 3, 18, 80, 103개였다(각 분모는 $5\text{사건} \times 27\text{설정} = 135$). 한 장면은 5초에서도 기본 설정으로 검출되지 않았다. 반복 판단마다 시계를 다시 시작하면 두 장면의 3초 판정이 통과로 바뀌었다. 이 수는 탐지 설정의 집계이며 UPPAAL 질의를 통과한 건수가 아니다. 이 결과는 판정에 사용한 설정을 함께 기록해야 함을 보여 주며 차량 안전 기준을 세우지 않는다.

8.1 결과가 뜻하는 것

두 연구 질문에 대한 답은 같은 방향을 가리킨다. RQ1의 작성 시나리오에서 이전 의무의 기억은 필요했지만 충분하지 않았다. 기존 검사기의 실패는 기억의 길이가 아니라, 여러 의무를 하나의 채널에 담고 대기 중 미상을 누적하는 표현과 정책에서 생겼다. 의무마다 해제 조건과 증거를 따로 연결하자, 새 행동의 근거 B가 앞선 의무 A를 해제하는지, 그리고 A가 미해제로 확인된 것인지 판단 근거가 없는 것인지를 구분할 수 있었다. RQ2의 작성 경계 시험에서는 장면을 넘어 유지되는 의무와 그 증거를 연결해야 해당 위반을 판정할 수 있었다. 다만 그렇게 하려면 대상 동일성, 적용 범위, 증거 유효성에 대한 근거가 함께 필요했다.

이전 상태의 기억, 참·거짓·미결정의 3값 판정, 최초 위반의 추적은 실행 중 검증과 LTL 모니터링에서 이미 확립된 기법이다^{[15], [16]}. 본 연구가 더한 것은 그 기법을 적용하기 위한 입력 쪽의 표현이다. 자동 생성된 CoC를 검토하기 위해 의무, 해제 조건, 조건별 증거를 원문 구절과 연결하는 프레임을 두고, 해제 근거가 없는 경우를 모순과 구분하여 기록한다. 교통 규칙 형식화나 자연어–시간 논리 변환 연구가 다루는 규칙·개별 요구 문장과 비교하면, 본 연구의 초점은 연속된 주석 사이의 의무–해제 관계에 있다.

조건별 FSM이 같은 사례를 모두 판정했다는 사실은, 이 범위의 규칙이 단순한 상태 기계로도 실행된다는 것을 보여 준다. 따라서 UPPAAL의 의의는 정확도 우위에 있지 않다. 판정 규칙을 상태와 전이로 명시하고, 검사 속성을 질의로 표현하며, 최초 문제까지의 진단 경로와 모델 파일을 재현 가능한 형태로 남기는 데 있다. 관찰 모델은 결정적이어서 입력마다 경로가 하나이므로, 이 결과를 환경의 여러 가능한 행동에 대한 검증으로 확대하지 않는다.

수집 자료의 결과는 다른 층위의 문제를 보여 준다. 사람의 판정이 엇갈렸고, 궤적 대조는 대부분 근거 부족으로 미상이었으며, 반응 판정은 설정에 따라 달라졌다. 이는 이 검사를 실제 CoC에 적용하려면 판정 규칙보다 앞서 입력의 의미 연결과 증거 확보가 해결되어야 함을 뜻한다.

8.2 검토 절차에서의 활용

판정 결과는 자료를 자동으로 채택하거나 삭제하는 데 쓰지 않는다. 검토자가 무엇을 다시 읽고 무엇을 보충해야 하는지 정하는 데 쓴다(표 23). 같은 “검토 필요” 표시라도, 판정에 따라 문장 수정, 증거 보충, 검사기 점검이라는 서로 다른 조치로 이어진다.

검토 기록에는 원문 구절, 조건 ID, 사건 순서, 모델과 규칙의 버전, 질의, 최초 위치와 사유를 남긴다. 규칙이나 탐지 설정에 따라 결과가 달라지면 두 결과와 바뀐 설정을 함께 기록한다. 장면 연결 근거가 없으면 판정 범위를 장면 안으로 한정한다. 이 절차가 학습 자료의 품질이나 학습 성능을 개선하는지는 본 논문에서 측정하지 않았다.

8.3 결과의 적용 범위와 한계

본 결과는 명시한 판정 규칙 아래에서 세 가지를 보인다. 의무와 해제 증거를 조건별로 연결하면 확정 모순과 근거 부족을 구분하고 최초 문제의 위치와 사유를 돌려줄 수 있다. 장면 경계에서는 연결 근거가 주어질 때 상태 유지가 판정에 필요하다. 이 규칙의 구현은 선별 없는 유한 범위에서 수식 판정과 일치한다. 반면 이 결과는 실제 CoC에서의 오류 검출 성능을 보이지 않으며, 그 이유와 후속 과제를 표 24에 정리했다.

보관된 장면 연결 기록에는 대상 동일성, 적용 범위, 해제 상태를 잇는 근거가 없어 수집 장면 간 의미 검증은 수행하지 않았으며, 서론의 장면 연결 예시는 동기 사례로만 사용한다. 따라서 본 결과는 판정 규칙이 실행 가능하고 근거를 추적할 수 있음을 보이는 적용 가능성 실증이다. 수집 CoC의 오류 검출 성능, 다른 자료와 생성 모델로의 일반화, 차량 안전과 학습 성능의 개선은 8.4절의 후속 연구로 남는다.

8.4 후속 연구

위 한계는 다음 순서로 보완할 수 있다.

• 독립 시험: 판정 명세만 공유받은 외부 작성자가 입력과 기대 판정을 만들고, 모델을 고정한 상태에서 실행한다.

• 수집 정답: 검토 지침을 보완하고 독립 중재를 두어 수집 CoC의 의미 정답을 구축한다. 그 위에서 정밀도, 재현율, 신뢰구간을 산출한다.

• 자동 추출: 원문에서 의무, 해제 조건, 증거를 연결하는 단계를 자동화하고, 작성 프레임과 비교해 추출 정확도를 평가한다.

• 비교 대상 확장: 전체 문장열을 입력받는 LLM 판정기와 같은 입력·같은 기대 판정에서 비교한다.

• 장면 연결과 학습 효과: 실제 장면 연결에 필요한 대상 동일성과 증거 유효 구간을 영상과 객체 기록에서 확보하고, 검토 결과를 반영한 자료가 학습 성능에 주는 영향을 측정한다.