확률을 넘어 결정론으로: 신경-기호적 법률 AI 설계

초록 본 칼럼에서는 거대언어모델(LLM)의 확률적 생성 한계로 발생하는 법률 수치 계산 및 조문 적용 환각을 극복하기 위해, 한국 형사사법의 약식절차에 특화된 신경-기호적(Neuro-Symbolic) AI 프레임워크를 제안합니다. LLM은 경찰 보고서 등 비정형 사실관계에서 양형 인자를 추출하는 의미론적 역할에 국한되며, 실제 형량 계산은 만족도 조건 솔버인 Z3 SMT를 통해 수학적으로 엄격하게 수행됩니다. 이 이중 구조는 법적 추론의 결정론적 정확성을 보장하며, 최종 기소장 초안 도출 과정에 인간 협업(Human-in-the-Loop) 검증 단계를 통합하여 법적 신뢰성을 극대화합니다. 결과적으로 본 아키텍처는 리걸테크 시스템의 무결성을 확보하는 강력한 기술적 해법을 제시합니다.

어느 날 늦은 밤, 일선 검찰청의 약식계 실무관이 음주운전 및 무면허 운전이 경합된 약식기소 사건의 형량을 산정하기 위해 AI 시스템을 가동한다고 가정해 봅시다. 기존의 생성형 LLM 기반 시스템은 관련 판례와 양형기준을 그럴듯하게 나열하지만, 가중·감경 요소를 종합하는 과정에서 미세한 수치 계산 오류나 조문 적용 순서의 뒤바뀜 같은 '치명적 환각'을 일으킬 위험이 상존합니다. 법을 다루는 AI에서 단 1만 원의 벌금 액수 오류나 단 하루의 면허정지 기간 오차는 사법 신뢰도를 송두리째 무너뜨리는 결과를 초래합니다. 이러한 한계는 LLM이 문맥의 '확률적 유사도'에 의존하여 텍스트를 생성하는 본질적 아키텍처에서 기인합니다. 따라서 우리는 비정형 데이터의 의미론적 이해는 LLM에 맡기되, 법률 적용과 수치 연산은 엄격한 기호적 논리 체계에 위임하는 하이브리드 접근법을 취해야 합니다. 이것이 바로 최근 학계와 실무에서 주목받는 한국 형사법 특화 신경-기호적(Neuro-Symbolic) AI의 핵심 문제의식입니다.

핵심 기술 개념

Neuro-Symbolic AI (신경-기호적 AI)

인공신경망의 패턴 인식 및 언어 이해 능력과 기호적 논리(Symbolic Logic)의 결정론적 추론 및 연산 능력을 결합한 하이브리드 인공지능 기술입니다.

Z3 SMT Solver (Z3 만족도 조건 솔버)

마이크로소프트가 개발한 고성능 만족도 조건(Satisfiability Modulo Theories) 솔버로, 복잡한 수학적 수식과 논리적 제약 조건을 만족하는 해가 존재하는지 판별하고 최적의 값을 결정론적으로 계산하는 도구입니다.

Sentencing Factors (양형 인자)

법관이 형을 정할 때 고려하는 범행의 동기, 수단, 결과, 피고인의 연령 및 전과 여부 등 형량의 가중·감경에 영향을 미치는 법적 요소를 의미합니다.

기술 심층 분석

1

의미론적 양형 인자 추출 파이프라인의 설계와 한계

첫 번째 단계는 경찰 보고서, 피의자 신문조서 등 비정형 텍스트에서 양형 인자를 정밀하게 추출하는 LLM 기반의 의미론적 추출(Semantic Extraction) 아키텍처입니다. 이 메커니즘은 구조화되지 않은 자연어 데이터에서 음주 측정 수치, 무면허 여부, 동종 전과 횟수 등의 핵심 메타데이터를 식별하여 JSON 스키마 형태로 정형화합니다. 그러나 이 과정에서 LLM은 문맥적 노이즈나 피의자의 변명 섞인 진술을 오인하여 양형 인자를 잘못 분류하거나 누락하는 한계를 보입니다. 이를 극복하기 위해 소스 텍스트의 구문 분석 트리와 개체명 인식(NER)을 결합한 다층 레이블링 검증 기법을 대안으로 적용하여, 추출된 인자의 정밀도를 극대화하고 후속 기호적 연산 레이어로 전달되는 데이터의 무결성을 선제적으로 확보해야 합니다.

2

Z3 SMT 솔버 기반의 결정론적 형량 계산 메커니즘

추출된 양형 인자는 LLM 내부에서 처리되지 않고, 엄격한 일차논리(First-Order Logic)와 산술 제약 조건식으로 변환되어 Z3 SMT 솔버로 즉시 이관됩니다. 예를 들어, 도로교통법 제148조의2에 따른 음주운전 처벌 기준과 대법원 양형기준의 가중·감경 요소를 솔버의 제약 조건(Constraints)으로 사전 정의해 둡니다. 솔버는 입력된 피고인의 음주 수치(예: 0.08%)와 전과 여부를 변수로 대입하여, 만족 가능한 형량 범위(Satisfiable Range)를 수학적으로 유도하고 최적의 벌금형 액수를 결정론적으로 산출합니다. 이 메커니즘은 확률적 무작위성을 배제하므로 동일한 입력에 대해 항상 동일한 법적 결론을 보장합니다. 다만, 법률 조문의 개정이나 새로운 판례 기준이 추가될 때마다 제약 조건 규칙 라이브러리를 수동으로 업데이트하고 정합성을 검증해야 하는 관리적 비용이 수반된다는 명확한 한계가 존재합니다.

3

이중 구조 아키텍처에서의 인터페이스 바인딩 및 타입 안전성

신경망 레이어와 기호적 레이어를 연결하는 인터페이스의 설계는 시스템 전체의 안정성을 결정짓는 핵심 병목 지점입니다. LLM이 출력한 비정형 JSON 데이터가 SMT 솔버가 요구하는 엄격한 데이터 타입(예: Integer, Real, Boolean)과 일치하지 않을 경우, 런타임 예외가 발생하거나 잘못된 논리식이 구성될 수 있습니다. 이를 방지하기 위해 두 레이어 사이에 강력한 타입 검증 스키마인 Pydantic 기반의 데이터 유효성 검증 레이어를 배치하고, 예외 발생 시 LLM에 피드백을 전달하여 자동 재시도(Self-Correction)를 수행하는 루프를 구현합니다. 그럼에도 불구하고 법적 개념의 모호성(예: '경미한 피해'의 기준)을 정량적 수치나 불리언 변수로 단순 변환할 때 발생하는 정보 손실은 기호적 모델링의 근본적 한계로 남으며, 이를 해결하기 위해 퍼지 논리(Fuzzy Logic)를 결합한 하이브리드 제약 조건 설계가 대안으로 논의되고 있습니다.

4

인간 협업(Human-in-the-Loop) 검증 게이트와 기소장 초안 생성

SMT 솔버가 계산한 무결한 형량 결과와 추출된 양형 인자는 최종적으로 인간 전문가(검사 또는 실무관)의 검증 게이트로 전달됩니다. 시스템은 솔버의 추론 경로(Proof Trace)를 자연어로 역번역하여 피고인의 혈중알코올농도에 따른 법적 조문 적용 및 가중 감경 사유를 설명 가능한 논리 구조로 시각화합니다. 사용자가 이 추론 과정을 승인하면, 시스템은 템플릿 기반 생성 엔진을 가동하여 법적 양식에 완벽히 부합하는 약식기소장 초안을 자동으로 빌드합니다. 이 방식은 LLM이 기소장 본문을 자유롭게 생성할 때 발생하는 문구 왜곡이나 허위 사실 기재를 원천 차단하지만, 인간 검증자의 피로도나 주관적 개입으로 인해 최종 의사결정의 일관성이 저해될 수 있어 검증 이력을 감사하는 별도의 로깅 시스템 구축이 필수적입니다.

기술적 트레이드오프

긴장 관계 LLM의 자연어 이해 유연성과 SMT 솔버의 결정론적 제약 조건 간의 긴장 관계입니다. LLM의 유연성을 높이면 비정형 문서에서 다양한 양형 인자를 포착할 수 있으나 정형 데이터로의 변환 오류율이 상승하며, 반대로 SMT 솔버의 제약 조건을 지나치게 엄격하게 설정하면 법률의 예외 조항이나 모호한 정황적 요소를 유연하게 반영하지 못하는 한계가 발생합니다.

실무적 해소 이러한 긴장은 다층적 신뢰도 임계값(Confidence Threshold) 설계와 동적 폴백(Fallback) 메커니즘으로 해결합니다. LLM이 추출한 양형 인자의 신뢰 점수가 기준치 미만일 경우 즉시 인간 검증자에게 판단을 위임하는 세미-오토매틱(Semi-automatic) 모드로 전환합니다. 또한, 정량화하기 어려운 정성적 양형 요소는 SMT 솔버의 변수 범위 내에서 가중치 구간(Interval)으로 처리하여 법관의 재량권을 수학적 마진으로 모델링함으로써 시스템의 유연성과 정확성의 균형을 확보합니다.

법마디 OS에 적용한다면

법마디 OS의 형사법 지원 모듈에 이 신경-기호적 아키텍처를 이식하기 위해, 우선 한국 교통범죄 및 경미 형사사건의 약식절차를 타깃으로 한 'Z3-Lawmadi 통합 추론 엔진'을 설계할 것입니다. 경찰 조서와 피의자 진술서가 시스템에 입력되면, 고성능 임베딩 모델과 미세조정된 LLM이 1차적으로 양형 인자를 식별하여 엄격히 정의된 JSON 스키마로 변환합니다. 변환된 데이터는 법마디 OS 내부의 'Rule-to-SMT 컴파일러'를 거쳐 Z3 SMT 솔버의 논리식으로 자동 변환됩니다. 이때 변환 과정의 정합성을 보장하기 위해, 컴파일러 엔진 전후단에 정적 분석 도구와 유효성 검증 게이트를 배치하여 타입 오류를 완전히 통제합니다. 최종적으로 솔버가 도출한 형량 범위와 법적 근거는 법마디 OS의 에이전틱 RAG 파이프라인과 결합되어, 실제 판례 인용의 진위 검증과 동시에 무결한 법률 의견서 및 기소장 초안을 생성하는 파이프라인으로 고도화될 것입니다. 이는 단순한 텍스트 생성을 넘어, 연산과 법리 적용의 논리적 무결성을 동시에 달성하는 법마디 OS만의 독보적인 기술적 차별점이 될 것입니다.

기술적 함의

생성형 AI의 고질적인 수치 계산 및 법률 적용 환각을 기호적 솔버와의 결합을 통해 원천적으로 해결할 수 있음을 입증했습니다.
약식절차와 같이 정형화된 형사사법 프로세스의 자동화를 통해 사법 행정의 효율성을 극대화하고 실무자의 업무 부담을 획기적으로 경감합니다.
설명 가능한 AI(XAI)의 구현을 통해 AI의 법적 판단 과정과 결론 도출 경로를 투명하게 공개함으로써 사법 신뢰도의 기틀을 마련합니다.

"법률을 다루는 인공지능에게 타협 가능한 오차 범위란 존재하지 않으며, 오직 엄격한 논리와 수학적 무결성만이 기술의 사법적 신뢰를 담보합니다."

참고 자료

칼럼니스트

지유

최고기술책임자 (CTO · Chief Technology Officer)

실리콘밸리 유니콘 창업 멤버급 / AI 무결성 검증 분야 세계적 석학급