Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning

논문 개요

대규모 언어 모델(LLM)은 광범위한 자연어 이해 과제에서 인상적인 성능을 보이지만, 엄밀한 논리적 추론이 요구되는 과제에서는 여전히 취약하다. LLM은 확률적 패턴 매칭으로 동작하기 때문에, 논리적으로 반드시 성립해야 하는 연역적 추론(deductive reasoning)을 수행할 때 오류를 범하는 경우가 많다. 예를 들어 삼단논법 추론이나 제약 충족 문제(CSP)에서 작은 오류가 연쇄 오류로 이어지는 경우가 빈번하다.

Pan et al.(2023)이 EMNLP 2023에서 발표한 Logic-LM은 이 문제를 신경-기호 통합(neuro-symbolic integration) 방식으로 해결한다. LLM은 자연어를 이해하고 형식 논리 프로그램으로 변환하는 역할을 수행하고, 실제 추론은 수학적으로 완전한(complete) 기호 추론기(symbolic solver)에 위임하는 두 단계 파이프라인이다. 이 접근법은 LLM의 언어 이해 능력과 기호 시스템의 논리적 완전성을 결합한다.

핵심 기여

신경-기호 논리 추론 파이프라인: 문제 형식화(Problem Formulation), 기호 추론(Symbolic Solving), 결과 해석(Result Interpretation)의 세 단계로 구성된 통합 프레임워크를 제안한다.
다중 형식 논리 지원: 1차 논리(First-Order Logic), 제약 최적화(Constraint Optimization), SAT 풀이 등 다양한 추론 형식을 단일 프레임워크에서 처리한다.
자기 수정(Self-Refinement) 메커니즘: 기호 추론기 실행 시 오류가 발생하면 LLM이 오류 메시지를 참고하여 형식 프로그램을 자동으로 수정하는 기능을 포함한다.
광범위한 벤치마크 검증: FOLIO, ProntoQA, ProofWriter, LogicalDeduction, AR-LSAT 등 5개 벤치마크에서 기존 LLM 프롬프팅 기법을 크게 상회하는 성능을 보였다.

방법론 상세

전체 파이프라인

Logic-LM은 세 단계로 구성된다:

$자연어 문제 LLM 형식 프로그램 기호 추론기 결과 LLM 자연어 답변$

1단계: 문제 형식화 (Problem Formulation)

LLM은 퓨샷 프롬프팅(few-shot prompting)을 통해 자연어 문제를 형식 논리 표현으로 변환한다. 지원하는 형식은 다음과 같다:

1차 논리 (FOL, Z3 사용):

전제: 모든 개발자는 커피를 좋아한다. Alice는 개발자다.
질의: Alice는 커피를 좋아하는가?

변환 결과 (Python Z3 형식):

dev = Function('developer', IntSort(), BoolSort())
likes_coffee = Function('likes_coffee', IntSort(), BoolSort())
alice = Int('alice')
s = Solver()
s.add(ForAll([x], Implies(dev(x), likes_coffee(x))))
s.add(dev(alice))
goal = likes_coffee(alice)

Prolog (귀납적 논리 프로그래밍): 규칙 기반 추론에 Prolog 문법을 사용하며, 연쇄 추론(chain reasoning)에 강점이 있다.

제약 최적화 (Python 기반): 수치적 제약이 포함된 문제(스케줄링, 퍼즐 등)에 PuLP나 OR-Tools를 활용한다.

2단계: 기호 추론 (Symbolic Solving)

형식 프로그램이 생성되면 해당 추론기를 실행한다. 예를 들어 Z3 SMT 솔버는 1차 논리 식의 충족 가능성(satisfiability)을 결정론적으로 판별하며, 이는 LLM의 확률적 추론과 달리 논리적으로 완전하다(complete).

$Z3 (ϕ) \to {SAT, UNSAT, UNKNOWN}$

$ϕ$ 가 SAT이면 모델(할당 값)을, UNSAT이면 추론 결과를 반환한다.

기호 추론기가 오류(파싱 에러, 실행 에러 등)를 반환하면, LLM에게 다음 프롬프트로 수정을 요청한다:

“다음 프로그램에서 오류가 발생했습니다: [오류 메시지]. 문제를 수정하여 올바른 형식 프로그램을 다시 생성하세요.”

이 과정을 최대 $k$ 번(보통 $k = 3$ ) 반복하며, 이는 형식화 오류로 인한 실패를 크게 줄여준다.

결과 해석

기호 추론기의 출력(예: True, False, 숫자 등)을 원래 자연어 문제의 답변 형식에 맞게 매핑한다.

실험 결과

주요 벤치마크 성능

벤치마크	CoT (GPT-4)	Logic-LM (GPT-4)	향상
FOLIO	70.3	79.8	+9.5%p
ProntoQA	82.1	97.0	+14.9%p
ProofWriter	65.0	79.9	+14.9%p
AR-LSAT	28.5	36.8	+8.3%p
LogicalDeduction	67.6	81.3	+13.7%p

특히 ProntoQA처럼 엄밀한 연역 추론이 필요한 과제에서 Chain-of-Thought(CoT) 대비 15%포인트 가까운 큰 향상을 보였다.

GPT-3.5 기반 결과

GPT-3.5를 기반으로 할 때 Logic-LM은 GPT-4 기반 CoT와 유사하거나 더 나은 성능을 보이는 경우가 있었다. 이는 기호 추론기의 결합이 더 작은 LLM의 추론 한계를 효과적으로 보완할 수 있음을 시사한다.

자기 수정 효과

자기 수정 없이 Logic-LM을 실행했을 때 약 15~25%의 케이스에서 형식 프로그램 실행 오류가 발생하였다. 자기 수정을 적용하면 이 오류율이 5% 이하로 감소하여 전체 성능이 크게 개선되었다.

의의 및 한계

의의

신뢰할 수 있는 논리 추론: 기호 추론기는 주어진 전제에서 올바른 결론을 반드시 도출한다(논리적 완전성). LLM 단독으로는 불가능한 수준의 논리적 신뢰성을 제공한다.
설명 가능성: 기호 추론기는 추론 과정을 명시적인 논리 식으로 표현하므로, 결과에 대한 설명이 자동으로 생성된다.
LLM 역할의 분리: LLM이 논리 자체를 수행하는 대신 번역기(translator) 역할에 집중하게 되어, 각 구성 요소가 자신이 잘하는 일에 특화된다.

한계

형식화 오류: LLM이 생성하는 형식 프로그램이 항상 의미론적으로 정확한 것은 아니다. 특히 복잡한 문제에서는 전제를 잘못 형식화하는 경우가 있다.
지원 추론 유형 제한: 현재 지원하는 추론 형식(FOL, Prolog, 제약 최적화)을 벗어나는 문제 유형에는 적용이 어렵다.
상식·맥락 추론 한계: 기호 논리는 명시적으로 주어진 전제에만 의존하므로, 암묵적 상식 지식을 필요로 하는 추론은 처리하기 어렵다.
계산 비용: LLM 호출에 더해 기호 추론기 실행과 잠재적인 자기 수정 반복이 추가 지연을 유발한다.
오픈소스 LLM 성능: 논문의 주요 결과는 GPT-4/GPT-3.5 기반이며, 오픈소스 LLM을 사용할 경우 형식화 품질이 저하될 수 있다.

도형준 지식 볼트

탐색기