AI 환각의 치명적 오류, ‘수학(정형 기법)’으로 잡는 법

AI는 왜 자꾸 그럴듯한 거짓말을 할까요? ‘수학’으로 AI의 환각을 잡는 법

우리는 대규모 언어 모델(LLM)이 얼마나 놀라운지 매일 경험하고 있습니다. LLM은 멋진 글을 쓰고, 복잡한 대화를 이해하며, 심지어 코드까지 척척 만들어냅니다.

하지만 동시에 LLM의 치명적인 약점, 바로 ‘환각(Hallucination)’ 현상도 목격하고 있습니다. AI가 아주 그럴듯하게, 하지만 사실과 전혀 다른 정보를 자신 있게 내놓는 것이죠.

일상적인 정보 검색이야 ‘불편함’ 수준에서 그칠 수 있습니다. 하지만 이 AI가 자율주행차의 핸들이나 병원의 진단 장비를 잡고 있다면 어떨까요? 이때 ‘그럴듯한 거짓말’은 단순한 오류가 아니라 재앙이 될 수 있습니다.

이것이 바로 AI가 마주한 ‘신뢰성 위기’입니다. 그리고 이 위기를 해결하기 위해, 우리는 AI와 정반대에 있는 것처럼 보이는 아주 오래되고 깐깐한 학문, ‘정형 기법(Formal Methods, FMs)’에 주목해야 합니다.

정형 기법은 ‘아마 작동할 것’이 아니라, ‘수학적으로 올바름이 증명되었음’을 다루는 학문입니다. 이 글은 AI의 유연함과 정형 기법의 엄격함, 이 두 세계를 융합하여 ‘진짜 신뢰할 수 있는 AI’를 만드는 로드맵을 제시합니다.

핵심 딜레마: 왜 둘은 서로를 필요로 할까요?

이 두 기술은 각자 명확한 한계를 가지고 있습니다.

LLM: ‘창의적이지만 가끔 덤벙대는 신입사원’

강점: 언어 이해력, 문맥 파악, 유연한 적응력이 뛰어납니다.

약점: 신뢰성이 부족합니다. 확률에 기반하기에 논리적 일관성을 보장할 수 없고, ‘환각’을 일으킵니다.

정형 기법(FM): ‘깐깐하지만 일 처리가 완벽한 베테랑 감사팀장’

강점: 수학적 엄격함으로 시스템이 100% 정확하게 동작하는지 증명할 수 있습니다. (항공, 보안 분야 필수)

약점: 극악의 사용성. 너무 어렵고 복잡해서 전문가가 아니면 사용하기 거의 불가능합니다.

두 세계의 융합

이 둘을 합친다는 것은, ‘신입사원의 창의력’에 ‘감사팀장의 검증 능력’을 더하는 것입니다. AI가 창의적이면서도 동시에 검증 가능하도록 만드는 것이죠.

이 융합은 두 가지 방향으로 진행됩니다.

• FM for LLM: 정형 기법(감사팀장)이 LLM(신입사원)을 더 신뢰할 수 있게 만듭니다.
• LLM for FM: LLM(신입사원)이 정형 기법(감사팀장)의 복잡한 업무를 도와 사용하기 쉽게 만듭니다.

이제 각 방향을 자세히 살펴보겠습니다.

방향 1. 정형 기법으로 AI 길들이기 (FM for LLM)

AI가 스스로 “잠깐, 내 말이 논리적으로 맞나?” 하고 검증하게 만드는 것입니다.

SMT 솔버: AI에게 ‘논리 계산기’를 쥐여주다

LLM은 종종 논리 퍼즐이나 복잡한 제약 조건 문제를 풀 때 실수를 합니다. 이때 SMT(Satisfiability Modulo Theories) 솔버라는 강력한 ‘논리 계산기’가 조력자가 될 수 있습니다.

LLM 에이전트는 다음과 같은 방식으로 일합니다.

잘못된 사례와 올바른 사례 비교

요청: “David(월/화 가능), Emma(화/수 가능), Alex(화/목 가능) 셋 다 가능한 요일은?”

잘못된 사례 (LLM 혼자): LLM은 각자가 ‘가능한’ 날짜만 조건으로 추가합니다. 하지만 ‘David는 수요일이나 목요일에는 안 된다’는 핵심 제약 조건을 빠뜨릴 수 있습니다.

올바른 사례 (LLM + FM): LLM이 ‘자가 수정’을 통해 “David는 수/목 불가능”, “Emma는 월/목 불가능” 같은 부정 제약 조건을 모두 추가합니다. 이 완벽한 조건을 Z3 솔버로 실행하면 “모두가 자유로운 공통 요일: [‘Tuesday’]”라는 검증된 결과를 얻습니다.

핵심은 LLM이 직접 추론하는 것이 아니라, 자신의 추론 과정을 공식화하고 전문 솔버에게 ‘검증’을 맡기는 것입니다.

논리 기반 테스팅: AI의 ‘사실 충돌 환각’ 잡기

LLM의 환각 중 심각한 문제는 ‘사실 충돌 환각(FCH)‘입니다. AI의 답변이 외부의 검증된 사실과 충돌하는 경우죠.

정형 기법은 단순 문자 비교가 아닌 ‘논리적 추론’으로 테스트 케이스를 만듭니다.

• 검증된 지식베이스에서 (서울, 수도, 대한민국)이라는 사실을 가져옵니다.
• 여기에 ‘역’ 관계 같은 추론 규칙을 적용해 (대한민국, ~수도, 서울)이라는 새로운 사실을 만듭니다.
• 이 지식으로 벤치마크를 구축합니다. (Q: “대한민국의 수도는 서울인가요?” → A: “YES”)
• LLM의 답변이 이 논리적 벤치마크와 일치하는지 검증합니다.

방향 2. AI로 정형 기법 사용하기 (LLM for FM)

정형 기법이 아무리 강력해도, 전문가가 아닌 이상 사용하기 거의 불가능했습니다. LLM은 이 장벽을 허무는 ‘지능형 조수’ 역할을 합니다.

오토포멀라이제이션: 인간의 언어를 기계의 언어로

가장 흥미로운 분야는 ‘오토포멀라이제이션‘, 즉 자연어를 기계가 읽을 수 있는 공식 사양이나 증명으로 자동 변환하는 것입니다.

수학 교과서의 ‘비공식적 증명’을 생각해 봅시다. 전문가에겐 명백한 단계들이 생략되어 있습니다. LLM은 이 증명을 공식 증명 도구(Coq 등)가 이해하는 코드로 변환합니다.

하지만 여기서도 LLM의 약점이 드러납니다.

잘못된 사례: LLM(ChatGPT-3.5)은 증명의 전체적인 구조(개요)는 잘 파악했지만, 2*(n+2)-(n+1)을 n+3이 아닌 2n+3으로 잘못 계산하는 치명적인 ‘대수학적 실수’를 저질렀습니다.

올바른 사례: LLM이 전체적인 ‘증명 개요’를 생성하게 하고, 복잡한 계산(상징적 추론)은 컴퓨터 대수 시스템(CAS)과 같은 외부 전문 도구에 위임하는 협업을 합니다.

더 스마트한 모델 체킹: AI가 설계하고 전문가가 검증하다

모델 체킹은 시스템이 가질 수 있는 모든 상태를 탐색해 오류(교착 상태 등)가 없는지 확인하는 기술입니다. ‘PAT 에이전트’ 예시는 LLM과 모델 체커의 환상적인 협업을 보여줍니다.

목표: “자동차 키가 차 안에 잠기지 않도록 하는 시스템” 설계

• LLM (1차 설계): LLM(GPT-4o)이 시스템 모델을 빠르게 생성합니다. 하지만 여기엔 상식에 어긋나는 논리적 결함이 있었습니다. (예: ‘이미 잠긴’ 차 문을 통해 키를 안으로 넣는 동작을 허용)
• FM (검증): 모델 체커(PAT)가 이 모델을 검증하고, “키가 차 안에 잠길 수 있다”는 오류를 발견해 피드백합니다.
• LLM (2차 수정): LLM은 이 피드백을 받아 논리적 결함을 수정합니다. (‘문이 열려 있을 때만’ 키를 차 안에 둘 수 있도록 제약 조건을 강화)
• FM (최종 검증): 수정된 모델은 PAT의 검증을 통과합니다.

이처럼 LLM은 개발을 가속화하고, 정형 기법 도구는 LLM이 놓친 논리적 결함을 잡아내어 시스템의 신뢰성을 보장합니다.

통합된 미래: ‘신뢰할 수 있는’ 프로그램 합성

이 두 세계가 완전히 융합되면, ‘신뢰할 수 있는 프로그램 합성‘이 가능해집니다.

현재 GitHub Copilot 같은 LLM은 코드를 훌륭하게 생성하지만, 우리는 그 코드를 신뢰하지 못합니다. (실제로 ChatGPT의 프로그래밍 답변 중 절반 이상이 부정확했다는 연구도 있습니다.)

이 문제를 ‘프로그램 정제(Program Refinement)‘라는 정형 기법으로 해결할 수 있습니다. 이는 ‘LLM 조수’와 ‘FM 감독관’이 함께 일하는 방식입니다.

이 과정을 반복하면, 최종적으로 생성된 코드는 ‘그럴듯한’ 코드가 아니라 ‘처음의 추상적 명세와 일치함이 수학적으로 증명된‘ 코드가 됩니다.

결론: ‘인상적인 AI’를 넘어 ‘신뢰할 수 있는 AI’로

LLM과 정형 기법의 융합은 단순한 기술적 호기심이 아닙니다. 이는 AI를 ‘인상적인 장난감‘에서 ‘신뢰할 수 있는 도구‘로 격상시키기 위한 필수적인 여정입니다.

• 정형 기법은 LLM에게 ‘책임감‘과 ‘검증 가능성‘을 부여합니다.
• LLM은 정형 기법에게 ‘접근성‘과 ‘효율성‘을 부여합니다.

물론 자연어를 공식적인 표현으로 정확하게 번역하는 문제, LLM의 환각을 근본적으로 제어하는 문제 등 해결해야 할 과제는 많습니다.

하지만 분명한 것은, AI의 유연한 지능과 정형 기법의 엄격한 추론 능력이 하나가 될 때, 우리는 비로소 복잡하고 치명적인 실제 문제들을 AI에게 안심하고 맡길 수 있게 될 것이라는 점입니다.