Introduction
최근 Large Language Model(LLM)이 자연어 추론에서 놀라운 성능을 보였으나, 복잡한 Logical Reasoning 문제에서는 여전히 한계를 드러내고 있다. 이 논문에서는 LLM을 Symbolic Solver와 결합하여 보다 정교하고 신뢰할 수 있는 논리 추론을 수행하는 방법을 제안한다. 이를 위해 LOGIC-LM이라는 프레임워크를 제안했으며, 논리적 문제를 자연어에서 Symbolic Form으로 변환하고, 이후 Symbolic Solver가 정확하고 해석 가능한 방식으로 추론을 수행하도록 했다. 결과적으로 LLM이 단독으로 문제를 풀이할 때 발생하기 쉬운 “불성실한 추론” 문제를 완화하고, 복잡한 논리 문제 해결 능력을 크게 향상시켰다.
Background and Problem
LLM은 Prompting 기법이나 Chain-of-thought 등을 통해 사람과 유사한 추론 과정을 모방해왔다. 하지만 실제로는, LLM 내의 추론 과정이 체계적으로 검증되지 않으므로, “이전에 제시한 reasoning과 최종 결론이 일치하지 않는” 문제가 발생하기 쉽다. 반면에 전통적인 Symbolic Solver는 논리 공리나 수학적 규칙에 의해 진행되는 추론이므로, 한번 세워진 공식(Formula)에 기반한 결과는 항상 논리적으로 타당함이 보장된다. 이 장점을 LLM과 결합하여, LLM의 자연어 이해(Natural Language Understanding) 능력과 Symbolic Solver의 논리적 엄밀함을 함께 누리고자 하는 것이 본 논문의 핵심 아이디어다.
LOGIC-LM의 세 단계
LOGIC-LM은 크게 세 단계로 구성된다.
- Problem Formulator
LLM이 자연어 형태의 문제와 Goal(질문)을 입력받아, 특정 Symbolic Language 형태로 문제를 변환한다. Deductive Reasoning, First-Order Logic(FOL), Constraint Satisfaction Problem(CSP), 그리고 Boolean Satisfiability(SAT) 등 4가지 유형에 맞추어, 문제를 적절한 Formal Language로 바꾸도록 Prompting을 설계했다. - Symbolic Reasoner
변환된 Symbolic Form을 해당 도메인에 맞는 Symbolic Solver에 입력한다.- Logic Programming(예: Pyke)
- FOL Prover(예: Prover9)
- CSP Solver(예: python-constraint)
- SAT Solver(예: Z3)
- Result Interpreter
Symbolic Reasoner가 반환하는 결과(Ex. “True/False/Unknown” 혹은 Value Assignments)를 해석하여, 최종적으로 사람이 이해할 수 있는 자연어 정답 또는 Multiple Choice 정답으로 만든다.
Self-Refinement 기법
논문에서는 Self-Refinement을 추가로 제안했다. LLM이 처음에 Symbolic Form을 생성했을 때 Syntax 오류나 논리적 구문 오류로 Symbolic Solver가 해석할 수 없을 수 있다. 이때 Solver가 반환하는 오류 메시지를 LLM에게 전달하면, LLM이 해당 오류 정보를 바탕으로 Symbolic Form을 재수정하여 다시 Solver에 전달한다. 이렇게 최대 몇 번 반복함으로써, 더 정확한 Symbolic Form을 얻는다.
실험 결과
문제 세팅
- Deductive Reasoning: 참으로 가정되는 일련의 전제로부터 필연적으로 참인 결론을 도출하는 논리적 과정입니다.
- First-Order Logic: 양화사와 술어를 포함하여 객체와 그 관계에 대한 진술을 표현.
- Constraint Satisfaction Problems: 모든 제약 조건을 만족하는 변수 값의 할당을 찾는 문제.
- Analytical Reasoning: 정보를 구성 요소로 분해하고, 그 구조를 이해하며, 구성 요소 간의 관계를 분석하여 복잡한 문제를 해결하는 문제
데이터셋
- PrOntoQA: Deductive Reasoning 문제.
- ProofWriter: Deductive Reasoning 문제, 다양한 추론 깊이(depth)로 구성.
- FOLIO: First-Order Logic 기반의 복잡한 지식 추론 문제.
- LogicalDeduction: CSP 형태, 서열(순서) 추론 문제를 담고 있음.
- AR-LSAT: Analytical Reasoning 문제, SAT 형태로 표현 가능.
주요 비교 대상
- Standard LLM: 단순 few-shot Prompting만 사용.
- Chain-of-Thought(CoT): Reasoning 과정을 단계별로 생성하여 최종 정답을 유도.
요약 성능
- LOGIC-LM이 모든 데이터셋에서 Standard/CoT 대비 큰 폭으로 성능이 향상되었다.
- GPT-3.5 기준, CoT 대비 평균 18.4%p, Standard 대비 39.2%p 더 높은 정확도를 보였다.
- GPT-4에서도 CoT 대비 평균 10.44%p, Standard 대비 24.98%p 성능 우위를 보였다.
Analysis
- Reasoning Depth가 깊어질수록 LOGIC-LM의 상대적 강점이 두드러졌다. ProofWriter에서 reasoning depth가 증가함에 따라 CoT와 Standard는 오답률이 치솟는 반면, LOGIC-LM은 Solver가 깊은 추론을 담당하기 때문에 정확도를 크게 유지했다.
- Self-Refinement은 Syntax 오류 등으로 인해 Solver가 실행 불가능한 Logical Form을 수정함으로써, Symbolic Form 생성 성공률(Executable Rate)을 의미 있게 올렸다.
Limitation and Future work
- Symbolic Solver의 표현력 한계
논리 형태가 너무 복잡하거나, 확률적 논리(Probabilistic Soft Logic) 같은 영역에서는 현재 Solver가 대응하기 어려울 수 있다. - Logical Form 변환의 어려움
자연어 문제를 정교한 논리 언어로 변환하는 과정 자체가 쉽지 않다. In-context Learning만으로는 완전한 대응이 어려우며, Fine-tuning이나 추가 모듈도 고려될 수 있다.
그럼에도 불구하고, 자연어 처리 측면에서 LLM이 “문제를 Symbolic Form으로 변환”하는 데 특화하고, 깊은 논리 추론은 Symbolic Solver에 오프로딩(offloading)하는 방식은 뛰어난 해석 가능성과 높은 정확도를 모두 달성하는 유망한 접근법으로 보인다.
Conclusion
논문에서는 LLM과 Symbolic Solver를 결합한 LOGIC-LM 프레임워크를 제안했다. 이 방법은 LLM이 문제를 Symbolic Language로 변환하고, Symbolic Solver가 논리적 추론을 담당하도록 분업함으로써, 복잡한 논리 문제에서도 신뢰도 높은 해답을 얻을 수 있음을 보였다. 다양한 데이터셋 실험에서 LOGIC-LM은 체계적인 추론 능력과 높은 정확도를 달성했다. 앞으로 확률적 논리나 다양한 Symbolic Solver 지원 등 확장이 기대된다.
