기술 요약: 한국 형사법을 위한 뉴로-심볼릭(Neuro-Symbolic) AI

1. 문제 정의

한국의 형사 사법 체계는 단순 음주운전(DUI), 무면허 운전, 경미한 교통사고와 같은 대량의 경미한 위반 사례를 신속하게 처리하기 위해 약식 절차(guyaksik)에 크게 의존하고 있다. 이러한 메커니즘은 사법 처리량을 개선하지만, 검사가 비정형 법률 문서(예: 음주 측정 기록, 경찰 보고서, 피의자 신문 조서)를 결정론적인 법정 결과로 수동 변환해야 하는 상당한 행정적 부담을 지운다.

최 최근 거대언어모델(LLM)의 발전은 밀집된 법률 텍스트로부터의 의미론적 추출 능력을 입증했다. 그러나 순수 LLM을 **법적 판단 예측(LJP)**에 배치하는 것은 근본적인 한계를 가진다:

• 확률적 본질: LLM은 확률에 기반하여 텍스트를 생성하며, 이는 벌금 계산에 필요한 엄격한 산술 및 규칙 기반 추론에는 부적합하다.
• 환각(Hallucination) 위험: 책임성이 완결된 결정론을 요구하는 법적 맥락에서, LLM은 복잡한 수학적 제약이나 특정 법적 임계값에 직면했을 때 빈번하게 "환각"을 생성한다.
• 형식적 검증의 부재: 순수 신경망 구조는 판결 결과의 유효성을 수학적으로 증명할 수 없으므로, 확률적 오류가 용납되지 않는 직접적인 사법 적용에는 불충분하다.

2. 방법론

저자들은 비정형 법률 사실과 형식적 검증을 연결하는 뉴로-심볼릭 프레임워크를 제안한다. 이 아키텍처는 신경망의 의미론적 이해와 심볼릭 논리 추론 간의 과업을 엄격히 분리하며, 5단계 파이프라인으로 구성된다.

모듈 1: 원시 데이터 수집 (Raw Data Ingestion)

시스템은 이질적이고 레이아웃이 복잡한 증거 문서(음주운전 정황 진술서, 음주 측정 결과, 신문 조서, 사고 보고서 등)를 수집한다. 시스템은 사용자 정의 규칙 기반 OCR과 양방향 인코더 텍스트 세그멘테이션을 사용하는 하이브리드 레이아웃 인식 수집 프로토콜을 채택하여, 서사적 섹션을 표 형식의 인덱스 및 메타데이터로부터 분리하고 이를 깨끗한 텍스트 스트림으로 변환한다.

모듈 2: LLM 추출 (LLM Extraction)

LLM은 의미론적 파서로서 핵심 사건 요소(범죄 유형, 혈중알코올농도(BAC)와 같은 연속 변수, 이산 범주형 변수)를 추출한다.

• 제약 조건: LLM은 추출된 모든 요소를 정확한 텍스트 출처("참조 텍스트")에 직접 매핑하도록 구조적으로 제한되어 법적 삼단논법과 근거를 강제한다.
• 출력: 추출된 엔티티는 중간 단계인 JSON 스키마에 채워지며, 이는 확률적 추출과 결정론적 논리 사이의 가교 역할을 한다.

모듈 3: 인간 참여형(Human-in-the-Loop, HITL) 검증

법적 준수와 적법 절차를 보장하기 위해, 계산이 수행되기 전 필수적인 검증 단계가 도입된다.

• 인터페이스: 분할 화면 UI는 구조화된 JSON 출력과 강조 표시된 참조 텍스트가 포함된 원본 문서를 동시에 보여준다.
• 메커니즘: 모든 추출된 변수는 기본적으로 is_valid_by_human = false 상태이다. 법률 전문가는 각 요소를 명시적으로 검증하여 이를 true로 전환해야 한다.
• 데이터 출처(Data Provenance): 인간에 의해 명시적으로 검증된 파라미터만이 솔버(solver)로 전달되어, 시스템이 자율적 의사 결정자가 아닌 의사 결정 지원 도구로서 기능하도록 보장한다.

모듈 4: 논리 번역 및 Z3 SMT 솔버

이 단계는 핵심적인 뉴로-심볼릭 브리지이다. 검증된 JSON 필드는 Z3 만족도 모듈 이론(SMT) 솔버 내의 형식적 상태 변수(불리언 플래그 및 정수 제약 조건)로 매핑된다.

• 공리 모델링: 2026년 교통 범죄 양형 기준은 수학적 공리로 공식화된다. 예를 들어, BAC 임계값은 조건부 제약 조건(예: $0.08 \le BAC < 0.20 \implies Crime\_Category = 3$)으로 모델링된다.
• 구간 도출: 솔버는 감경 및 가중 요인의 불리언 배열을 평가하여 양형 구간(기본, 감경 또는 가중)을 결정한다.
• 징역형 강제 논리: 솔버는 복합 논리 제약 조건을 체크하여(예: 전과 $\ge 3$ 이거나 가중 요인이 지배적인 경우), 벌금 계산을 무시하고 징역형 권고를 우선하도록 한다.
• 만족도 체크 (Satisfiability Check): 결과를 출력하기 전, Z3는 SAT 체크를 수행하여 논리적 모순이 없는지 확인한다(예: 하나의 사건이 "감경"인 동시에 "가중"일 수는 없다). 만약 UNSAT 상태가 감지되면, 파이프라인은 충돌 해결을 위해 HITL 인터페이스로 되돌아간다.

모듈 5: 시각화 및 문서 생성

Z3 솔버로부터 도출된 결정론적 출력은 실행 가능한 결과물로 변환된다.

• 양형 트리 시각화: 시스템은 논리적 결정 경로(BAC 범주화부터 최종 벌금까지)를 시각적 트리로 렌더링하여 해석 가능한 감사 추적(audit trail)을 제공한다.
• 문서 초안 작성: 엄격하게 구조화된 프롬프트를 사용하여 LLM은 법적으로 준수되는 문서(경찰 수사 보고서, 송치 의견서, 약식 기소 요청서)를 생성한다. 결정적으로, 벌금 액수는 Z3 솔버의 출력값으로부터 그대로 주입되어, LLM이 숫자를 재계산하거나 환각을 일으내는 것을 방지한다.

3. 주요 기여

본 논문은 세 가지 주요 기여를 기술한다:

1. 뉴로-심볼릭 파이프라인 설계: 비정형 경찰 및 검찰 기록을 결정론적인 법적 결과로 변환하는 프레임워크로, 특히 벌금 계산 중 발생하는 환각 위험을 완화하기 위해 LLM을 의미 추출에만 국한시킨다.
2. 인간 참여형(HITL) 검증: 추출된 법률 변수를 소스 참조 텍스트에 고정하는 투명한 체계를 통해, 검사의 최종 법적 권한을 유지하면서 인간의 감독과 해석 가능성을 보장한다.
3. 형식적 법률 논리 프레임워크: 확률적 생성을 대신하여 수학적 증명을 사용함으로써, 2026년 양형 기준에 부합하는 정밀한 양형 범위를 계산하기 위해 Z3 SMT 솔버를 이용한 논리 프레임워크를 구축하였다.

4. 결과 및 주장

본 연구는 아키텍처의 이론적 공식화와 논리적 매핑에 집중하므로 경험적 성능 지표(예: 테스트 세트에 대한 정확도 백분율)를 제시하지 않는다. 대신, 저자들은 설계를 바탕으로 다음을 주장한다:

• 결정론: 통계적 정리를 정리 증명기(theorem prover)로 오프로딩함으로써, 시스템은 LLM 고유의 확률적 오류로부터 자유로운 양형 결과를 보장한다.
• 강건성(Robustness): SAT 체크 메커니즘은 판결이 생성되기 전에 논리적 모순을 탐지하고 해결하여 유효하지 않은 법적 결과가 나오는 것을 방지한다.
• 책임성: HITL 통합은 시스템이 검증 가능한 보조 도구로 남게 하여, "블랙박스" AI 모델에 내재된 투명성 문제를 해결한다.

5. 의의

저자들은 이 연구를 고위험 환경에서의 법적 판단 예측(LJP)에 있어 필수적인 진화로 규정한다. LLM이 산술 및 엄격한 규칙 준수에 부적합함을 인정함으로써, 본 논문은 신경망의 의미론적 강점과 법의 "하드" 제약 조건에 대한 심볼릭 논리의 신뢰성을 결합한 하이브리드 접근 방식을 제안한다.

이 연구의 의의는 사법적 무결성을 훼손하지 않으면서 한국의 경미한 검찰 사건의 행정적 병목 현상을 완화할 수 있는 잠재력에 있다. 이 프레임워크는 모든 수학적 결과가 형식적으로 검증되고 인간에 의해 확인된 사실에 근거하도록 보장하면서, 약식 기소(yaksik-gongsojang) 작성을 자동화할 수 있는 경로를 제공한다. 저자들은 현재 초점이 교통 범죄에 맞춰져 있으나, 이 아키텍처가 약식 절차로 종결되는 다른 경미한 범죄(예: 단순 폭행, 명예훼손, 절도 등)로 확장 가능하도록 설계되었음을 언급한다.