Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning

이 논문은 LLM 에이전트와 SMT 기반 검증이 결합된 'L4L' 프레임워크를 제안하여, 자연어의 유연성과 기호 논리의 엄밀함을 융합함으로써 법적 AI 의 신뢰성과 검증 가능한 논리적 근거를 확보하는 방법을 제시합니다.

핵심

이 논문은 **"법률 인공지능 (AI) 을 어떻게 하면 믿을 수 있고, 오류가 없으며, 논리적으로 검증 가능한 상태로 만들 수 있을까?"**라는 질문에 대한 해답을 제시합니다.

기존의 AI 는 법률 문서를 읽고 요약하는 데는 뛰어나지만, "왜 그렇게 판결했는지"에 대한 논리적 근거를 검증할 수 없거나, 사실과 다른 내용을 만들어내는 (할루시네이션) 문제가 있었습니다.

이 논문에서 제안한 **'L4L'**이라는 새로운 시스템을 한 편의 법정 드라마에 비유하여 쉽게 설명해 드리겠습니다.

---

🎭 L4L: "논리 검사관"이 있는 스마트 법정

이 시스템은 단순히 AI 가 판결을 내리는 것이 아니라, 세 명의 역할이 나뉜 AI 팀이 협력하고, 마지막에 엄격한 논리 검사관이 모든 것을 확인하는 구조입니다.

1. 역할이 나뉜 AI 변호사들 (검사 vs 변호인)

일반적인 AI 는 한쪽 입장만 보고 결론을 내리기 쉽습니다. 하지만 L4L 은 두 명의 AI 변호사를 투입합니다.

• AI 검사: 피고인을 유죄로 만들기 위해 가능한 모든 법 조항과 불리한 사실을 찾아냅니다. ("이건 중범죄야!")
• AI 변호인: 피고인을 무죄로 만들기 위해 유죄 조항을 피하고, 감경 사유를 찾아냅니다. ("아니요, 이건 경미한 사안이에요.")

비유: 마치 TV 법정 드라마처럼, 양쪽이 서로 치열하게 다투며 사실을 정리합니다. 하지만 여기서 중요한 건, 두 변호사가 서로 다른 편견을 가지고 있어도, 나중에 나오는 공통된 규칙을 따르도록 설계되었다는 점입니다.

2. "법률 번역기"와 "논리 검사관" (SMT 솔버)

두 변호사가 주장한 내용을 그대로 받아들이지 않습니다.

• 자동 번역기: 변호사들이 쓴 복잡한 법률 용어와 사실 관계를, 컴퓨터가 계산할 수 있는 **엄격한 수학적 논리 (코드)**로 번역합니다.
• 논리 검사관 (SMT 솔버): 이 번역된 논리가 실제 법전과 모순되지 않는지를 수학적으로 100% 검증합니다.
  • "약 10g 을 팔았다"고 주장했는데, 법전에는 "20g 이상이어야 중죄"라고 되어 있다면? 검사관은 "틀렸습니다"라고 즉시 차단합니다.
  • AI 가 "이 법조항이 적용된다"고 말해도, 논리적으로 맞지 않으면 절대 판결에 반영되지 않습니다.

비유: 두 변호사가 "이건 A 법을 위반했다!"라고 외쳐도, 논리 검사관이 "아니야, A 법은 B 조건이 충족되어야 적용돼. 너는 조건을 안 맞췄어. 다시 해!"라고 엄격하게 검열하는 역할을 합니다.

3. "판사" AI: 최종 판결문 작성

논리 검사관이 "이 주장은 논리적으로 맞다"고 승인한 내용만 최종 판사 AI 에게 전달됩니다.

• 판사 AI 는 검증된 논리 결과를 바탕으로, 실제 법원 판결문처럼 이유가 명확하고 설득력 있는 판결문을 작성합니다.
• 이때 과거의 비슷한 판례 (선례) 를 참고하여, 법이 가진 유연한 해석까지 더합니다.

비유: 논리 검사관이 "이건 안전하다"고 도장을 찍은 재료만 가지고, **명장 (판사)**이 최고의 요리를 만들어내는 것과 같습니다.

---

🌟 왜 이 방식이 특별한가요? (핵심 장점)

1. 거짓말을 못 합니다 (검증 가능성):

   • 기존 AI 는 "내가 생각하기에 이 법이 적용되는 것 같아"라고 막연하게 말할 수 있습니다.
   • L4L 은 "이 법이 적용된다는 수학적 증명이 있다"고 말합니다. 만약 증명 과정에 오류가 있으면, 시스템이 스스로 "오류가 있다"고 알려줍니다.

2. 공정한 경쟁 (적대적 학습):

   • 검사와 변호인 AI 가 서로 싸우게 함으로써, 한쪽의 편향된 주장을 걸러내고 사실 관계를 더 정확하게 파악합니다.

3. 법적 근거가 명확합니다:

   • "왜 이 사람이 1 년 형을 받았나요?"라고 물으면, AI 는 "법률 제 347 조와 2016 년 해석 8 호에 따라, 약물의 양이 6g 이기 때문에..."라고 수치와 조항을 들어 명확하게 설명할 수 있습니다.

💡 결론: "믿을 수 있는 법률 AI"의 탄생

이 논문은 **"AI 가 법을 판단할 때, 인간의 직관이나 감이 아니라, 수학적으로 검증된 논리가 중심이 되어야 한다"**는 것을 보여줍니다.

마치 **스마트한 비서 (LLM)**가 법전을 읽고 초안을 작성하면, **엄격한 감사관 (논리 솔버)**이 모든 숫자와 조건을 다시 계산하여 오류를 잡은 뒤, 경험 많은 판사가 최종 결정을 내리는 시스템입니다.

이 way 로만 AI 가 법정에 서도 **"이 판결은 논리적으로 완벽하게 검증되었습니다"**라고 자신 있게 말할 수 있게 되는 것입니다.

기술 요약

1. 문제 정의 (Problem)

법적 결정은 단순히 법적 텍스트를 언어적으로 이해하는 것을 넘어, **형식적 합리성 (Formal Rationality)**을 충족해야 합니다. 즉, 판결은 명시된 법률, 해석, 판례와 논리적으로 일관되어야 하며 그 근거가 검증 가능해야 합니다.

현재의 대규모 언어 모델 (LLM) 기반 법적 AI 시스템은 다음과 같은 한계를 가집니다:

• 할루시네이션 (Hallucination): 권한 없는 법조항을 인용하거나 사실과 다른 결론을 도출하는 경향이 있습니다.
• 검증 불가능성: 신경망 (Neural) 기반의 추론은 '블랙박스' 성격을 띠어, 결론이 도출된 논리적 경로를 독립적으로 검증하거나 감사 (Audit) 할 수 없습니다.
• 논리적 일관성 부재: 서로 다른 교리적 요구사항을 혼동하거나, 법률적 논리의 유효성을 보장하지 못합니다.

기존의 검색 증강 생성 (RAG) 기반 시스템 (예: CHATLAW, LAWLLM 등) 은 사실 오류를 줄이는 데 도움을 주지만, 여전히 불투명한 생성 과정에 의존하며 논리적 보장을 제공하지는 못합니다.

2. 방법론 (Methodology: L4L Framework)

저자들은 L4L이라는 새로운 프레임워크를 제안합니다. 이는 LLM 의 유연성과 SMT (Satisfiability Modulo Theories) 솔버의 엄격한 형식적 추론을 결합한 솔버 중심 (Solver-Centric) 아키텍처입니다.

핵심 구성 요소 및 프로세스

L4L 은 네 가지 주요 단계로 운영됩니다.

1. 법률 지식 구축 (Statute Knowledge Building):

   • 자연어 형태의 법률 조항을 LLM 을 통해 논리적 제약 조건 (Logical Constraints) 으로 자동 형식화 (Autoformalization) 합니다.
   • 생성된 SMT 모델은 구문 검사, 의미적 린팅 (Semantic Linting), 그리고 실제 사례를 통한 테스트를 거쳐 검증됩니다.
   • 메타 스키마: Actor(행위자) - Action(행위) - Condition(조건) - Norm(규범)의 4 중 구조를 기반으로 하며, 형식적 지식 베이스 (KB) 를 구성합니다.

2. 이중 사실 및 법률 추출 (Dual Fact-and-Statute Extraction):

   • 역할 분화 에이전트: 검찰 (Prosecutor) 과 변호인 (Defense) 역할을 수행하는 두 개의 LLM 에이전트가 대립적으로 작동합니다.
   • 적대적 추출: 검찰 에이전트는 유죄를 최대화하도록, 변호인 에이전트는 무죄를 최대화하도록 프롬프트를 받아 사건 사실을 추출합니다. 이는 편향을 방지하고 사실과 법률 적용 가능성을 독립적으로 검증합니다.
   • 출력: 각 에이전트는 사실 튜플 (Fact Tuples) 과 후보 법률 조항을 생성합니다.

3. 솔버 중심 심판 (Solver-Centric Adjudication):

   • 자동 형식화 (Autoformalizer): 에이전트들의 출력을 SMT 솔버 (Z3) 가 이해할 수 있는 형식적 제약 집합 ($\Phi$) 으로 변환합니다.
   • 2 단계 검증:
     • 단계 1 (조항 적용성): 추출된 사실이 특정 법률 조항의 적용 범위 (Guard) 를 만족하는지 SMT 솔버가 검증합니다. (Unsat 일 경우 해당 조항 폐기)
     • 단계 2 (조항 자격): 적용 가능한 조항 내에서 어떤 세부 조항 (Clause) 이 사실에 의해 충족되는지 확인하여 법적 결과 (형량 범위 등) 를 도출합니다.
   • 피드백 루프: 일관성이 없으면 (Unsat Core 발생), 오류 원인 (사실 추출 오류 등) 을 식별하여 제약 조건을 수정하고 재검증합니다.

4. 사법적 렌더링 (Judicial Rendering):

   • 솔버가 검증한 논리적 결과 (형식적 합리성) 를 바탕으로, 판사 에이전트 (Judge LLM) 가 최종 판결문을 작성합니다.
   • 실체적 합리성 반영: 판사 에이전트는 솔버 결과에 더해 유사 판례 (Precedents) 와 법률 해석 원칙을 통합하여, 인간 판사의 재량 (Discretion) 이 필요한 부분 (형량 구체화 등) 을 자연어로 서술합니다.
   • 이 과정은 형식적 검증과 실체적 판단을 분리하면서도 통합하여, 감사 가능한 판결을 생성합니다.

3. 주요 기여 (Key Contributions)

• 법률 형식화 체계: 자연어 법률 조항을 실행 가능한 논리적 제약 조건으로 변환하는 체계적인 접근법을 제안했습니다.
• 형식적 추론 통합 프레임워크: SMT 솔버를 중심으로 한 법적 추론 프레임워크를 설계하여, 실체적 합리성 (LLM 의 유연성) 과 형식적 합리성 (솔버의 엄격함) 을 연결했습니다.
• 역할 분화 에이전트 아키텍처: 검찰과 변호인 역할을 하는 에이전트가 공유된 형식적 제약 하에서 독립적으로 사실을 추출하고 주장하는 구조를 도입했습니다.
• 검증 가능한 감사 가능성 (Auditability): 솔버가 검증한 심볼릭 증명을 통해 법적 결론의 근거를 투명하게 추적할 수 있게 했습니다.

4. 실험 결과 (Results)

저자들은 LeCaRDv2(중국 형사 사건), LEEC(법적 요소 추출), 그리고 인위적 교란 (Perturbation) 데이터셋을 사용하여 실험을 수행했습니다.

• 정확도 (Accuracy):

  • 법조항 예측: L4L 은 GPT-4o, Claude, DeepSeek 등 최신 LLM 및 기존 법률 특화 모델 (LexiLaw, DISC-Law) 보다 정밀도 (Precision) 와 F1 점수에서 일관되게 우위를 점했습니다. 특히 L4L 은 솔버 검증을 통해 논리적으로 일관되지 않은 주장을 걸러내어 정밀도를 크게 향상시켰습니다.
  • 형량 예측: 평균 형량 오차 (ASE) 와 RMSE 측면에서 L4L 이 가장 낮은 오차를 보였으며, 법적 유효성 (Valid Ratio) 이 가장 높았습니다.
  • 피의자 추출: 다중 피의자 사건에서 피의자 단위 분해 (Suspect-level decomposition) 정확도 (Suspect Extraction F1) 가 가장 높았습니다.

• 강건성 (Robustness):

  • 사실적 교란 (예: 나이, 경미한 사정 변경) 이 가해졌을 때, L4L 은 다른 모델들보다 **변화 정확도 (Change Accuracy, 62.56%)**가 가장 높았습니다. 이는 형식적 논리 검증이 사실 변화에 따른 법률 적용의 변화를 정확하게 포착함을 의미합니다.

• 성분 분석 (Ablation Study):

  • 형식적 추론 모듈을 제거했을 때 성능이 가장 급격히 저하되어, 솔버 기반 검증의 핵심적 역할을 입증했습니다.
  • 변호인 에이전트 제거 시 정밀도가 감소하여, 대립적 에이전트 구조의 중요성을 확인했습니다.

5. 의의 및 결론 (Significance)

• 신뢰할 수 있는 법적 AI: L4L 은 LLM 의 생성 능력과 형식적 논리의 검증 능력을 결합하여, "검증 가능하고 감사 가능한 (Auditable)" 법적 결정을 내리는 시스템을 실현했습니다.
• 형식적 vs 실체적 합리성의 균형: 솔버는 법적 일관성을 보장하고, LLM 은 법률 해석과 판례 기반의 재량을 담당함으로써, 법치주의 사회가 요구하는 엄격함과 유연성을 동시에 충족시킵니다.
• 향후 방향: 현재는 성문법 (Statutory Law) 에 집중되어 있으나, 판례법과 모호한 규범으로 확장할 경우 법적 AI 의 신뢰성을 더욱 높일 수 있을 것으로 기대됩니다.

이 연구는 법적 AI 가 단순한 텍스트 생성 도구를 넘어, 논리적 근거가 명확하고 신뢰할 수 있는 사법 보조 도구로 발전할 수 있는 중요한 방향성을 제시합니다.