(2025-10-05) AI 결과에 대해 강건성을 보강하는 방법 - Proof of Thought

2024년 NeurIPS 2024에서 발표된 사고 증명: 신경 기호 프로그램 합성을 통한 견고하고 해석 가능한 추론이라는 논문을 참고하여, 결과에 대한 추론 가정을 자체 검증하는 아키처가 Open Source로 공개되었습니다. 해당 논문에서 예기하는 주요 논점과, Github 저장소에 있는 지원 API 를 어떻게 사용할지 알아보도록 하겠습니다.

​

​

LLM의 한계를 넘어서는 새로운 시도

​

Large Language Models(LLM)은 놀라운 성능을 보여주지만, 복잡한 논리적 추론 과정에서 종종 일관되지 않은 결과를 내놓는 한계를 가지고 있습니다.

​

이는 높은 신뢰성이 요구되는 분야에 LLM을 적용하는 데 큰 장벽이 되어 왔습니다.

​

'Proof of Thought'(PoT)는 이러한 문제를 해결하기 위해 등장한 혁신적인 프레임워크입니다.

​

​

생각의 과정을 증명하다

LLM의 유연한 사고와 정형 논리의 견고함을 결합한 검증 매커니즘.

PoT의 핵심은 LLM이 생성한 추론 과정을 그대로 신뢰하는 것이 아니라, 이를 검증 가능한 논리적 형태로 변환하여 타당성을 증명하는 데 있습니다.

​

이 과정은 크게 두 단계로 이루어집니다.

​

첫째, LLM이 자연어로 제시된 문제에 대한 해결 계획을 JSON 기반의 도메인 특화 언어(DSL)로 생성합니다.

​

둘째, 이 DSL 코드는 사용자 정의 인터프리터를 통해 1차 논리(First-Order Logic) 프로그램으로 변환됩니다.

​

마지막으로, 변환된 논리 프로그램은 Z3와 같은 정리 증명기(theorem prover)에 의해 그 정합성이 엄격하게 검증됩니다.

​

이러한 신경-기호(Neuro-Symbolic) 접근 방식을 통해 PoT는 LLM의 창의적인 문제 해결 능력과 기호 논리의 정밀함을 결합하여 추론 결과의 신뢰도를 획기적으로 높였습니다.

​

​

실제 동작하는 방법 예시

​

질문: "A는 B보다 나이가 많고, B는 C보다 나이가 많다. 그렇다면 A는 C보다 나이가 많은가?"

​

이 간단한 자연어 질문이 PoT 프레임워크와 Z3를 통해 어떻게 검증되는지 단계별로 살펴보겠습니다.

​

1단계: LLM이 '설계도'를 만듭니다 (자연어 → DSL)

LLM은 이 질문을 분석해서 컴퓨터가 이해하기 쉬운 구조적인 데이터, 즉 JSON 형태의 DSL로 변환합니다. 여기서 DSL은 미리 정해진 약속(문법)에 따라 만들어집니다.

 

{
  "declarations": [
    { "name": "A", "type": "Int" },
    { "name": "B", "type": "Int" },
    { "name": "C", "type": "Int" }
  ],
  "facts": [
    { "op": ">", "args": ["A", "B"] },
    { "op": ">", "args": ["B", "C"] }
  ],
  "query": { "op": ">", "args": ["A", "C"] }
}

 

• declarations: "나이를 비교할 대상 A, B, C가 있고, 이들의 나이는 모두 정수(Integer)다." 라고 변수를 선언하는 부분입니다.
• facts: "A는 B보다 크다 (A > B)", "B는 C보다 크다 (B > C)" 와 같이 문제에 주어진 **명백한 사실(가정)**들을 기록합니다.
• query: "그렇다면 A는 C보다 큰가? (A > C)" 라고 우리가 검증하고 싶은 주장을 명시합니다.

​

2단계: '설계도'를 Z3의 언어로 번역합니다 (DSL → SMT-LIB)

이제 이 JSON '설계도'를 Z3가 직접 알아들을 수 있는 언어인 SMT-LIB 형식으로 번역합니다. 이 언어는 괄호를 많이 사용하는 LISP이라는 프로그래밍 언어와 비슷하게 생겼습니다.

​

; 변수 선언
(declare-const A Int)
(declare-const B Int)
(declare-const C Int)

; 사실(가정)을 추가
(assert (> A B))
(assert (> B C))

; 검증하고 싶은 주장이 '틀렸다'고 가정해봄
(assert (not (> A C)))

; 만족하는 해가 있는지 확인해줘!
(check-sat)

​

여기서 가장 중요한 부분이 (assert (not (> A C))) 입니다.

Z3는 직접적으로 "A > C가 참인가?"를 증명하지 않습니다. 대신 **"A > C 라는 주장이 거짓이라고 가정했을 때, 논리적으로 말이 되는 상황이 존재하는가?"**를 확인하는 귀류법(Reductio ad absurdum) 방식을 사용합니다.

• 만약 A > C가 거짓인데도 주어진 사실(A>B, B>C)과 충돌하지 않는 해(解)가 존재한다면? → 원래 주장은 거짓일 수 있습니다.
• 만약 A > C가 거짓이라고 가정하니, 주어진 사실들과 명백한 모순이 발생한다면? → 그 가정 자체가 틀린 것이므로, 원래 주장은 참일 수밖에 없습니다.

​

3단계: Z3가 최종 판결을 내립니다 (증명 결과)

위 SMT-LIB 코드를 Z3에게 입력하면, Z3는 내부의 강력한 알고리즘을 사용해 이 논리식들을 분석합니다.

그리고 다음과 같은 결과를 내놓습니다.

​

unsat

​

이 unsat이라는 한 단어가 바로 Z3의 최종 판결입니다. unsatisfiable의 줄임말로, "당신이 제시한 모든 조건을 동시에 만족시키는 해(解)는 이 세상에 존재하지 않습니다" 라는 뜻입니다.

​

다시 말해,

1. A는 B보다 나이가 많고,
2. B는 C보다 나이가 많으면서,
3. 동시에 A가 C보다 나이가 많지 않은 경우는 논리적으로 불가능하다는 것을 증명한 것입니다.

이 모순을 발견했기 때문에, 우리는 A > C 라는 원래의 주장이 **참(True)**이라는 결론을 확신할 수 있게 됩니다.

​

만약 우리가 "A는 B보다 나이가 적은가?" (< A B)를 검증했다면, Z3는 다음과 같이 답했을 것입니다.

sat

satisfiable의 줄임말로, "조건을 만족하는 해가 존재합니다" 라는 의미입니다. 그리고 친절하게 그 예시(모델)까지 보여줍니다.

(model (define-fun C () Int 0) (define-fun B () Int 1) (define-fun A () Int 2))

"예를 들어 C=0, B=1, A=2 이면 모든 조건을 만족시킬 수 있습니다." 라고 구체적인 반례를 찾아준 것이죠.

​

이처럼 Z3는 LLM의 창의적인 추론을 수학적이고 논리적인 '사실'로 뒷받침해주는 매우 강력하고 신뢰할 수 있는 '구조 기술사' 역할을 수행합니다. 추상적인 비유가 아니라, 실제로 이렇게 엄격한 논리 검증 과정을 거치기 때문에 PoT의 결과가 신뢰도가 높은 것입니다.

​

​

숫자로 증명된 압도적 성능

​

PoT 프레임워크의 효과는 다양한 벤치마크 데이터셋을 통해 객관적으로 입증되었습니다.

특히 복잡한 다단계 추론을 요구하는 StrategyQA 벤치마크 등에서 기존의 다른 방법론들을 능가하는 성능을 보여주었습니다.

평가 항목	성능 지표
컴파일 성공률	82.4%
F1 Score	71.13%
Reddit-OSHA 컴파일 오류	0%
Reddit-OSHA Win Rate	81.55%

이러한 결과는 PoT가 단순히 이론에 그치지 않고, 실제 문제 해결에서 더 정확하고 일관된 답변을 생성할 수 있음을 명확히 보여줍니다.

​

​

이제 당신의 프로젝트에 적용할 시간

​

PoT는 오픈소스로 공개되어 누구나 자신의 프로젝트에 적용해 볼 수 있습니다.

Github 저장소에 공개된 API는 매우 직관적인 인터페이스를 제공하여 복잡한 설정 없이도 PoT의 강력한 추론 검증 기능을 활용할 수 있도록 지원합니다.

다음은 API를 사용한 간단한 예시 코드입니다.

 

from openai import OpenAI
from z3dsl.reasoning import ProofOfThought

# OpenAI 클라이언트 설정
client = OpenAI(api_key="...")

# PoT 객체 생성
pot = ProofOfThought(llm_client=client)

# 질문 쿼리
result = pot.query("Would Nancy Pelosi publicly denounce abortion?")

# 결과 출력
print(result.answer)
# 출력: False

​

이처럼 몇 줄의 코드만으로 LLM의 답변을 논리적으로 검증하고, 더 신뢰할 수 있는 결과를 얻을 수 있습니다.

​

​

해석 가능한 AI를 향한 새로운 발걸음

​

PoT는 LLM의 '블랙박스'와 같았던 추론 과정을 투명하게 들여다볼 수 있는 창을 제공합니다.

​

단순히 결과만을 제시하는 것을 넘어, 그 결과에 이르는 모든 논리적 단계를 증명하고 검증할 수 있게 된 것입니다.

이는 AI의 결정 과정을 인간이 이해하고 신뢰할 수 있도록 만드는 '해석 가능한 AI(XAI)' 분야의 중요한 이정표가 될 것입니다.

​

앞으로 PoT와 같은 신경-기호 접근법이 어떻게 발전하여 더 복잡하고 중요한 문제들을 해결해 나갈지 기대해 봐도 좋지 않을까요?

​

이런 LLM + Static Framework 구조는 반복적으로 나타나고 있습니다. Agent AI도 MCP와 Prompt를 이용하는 구조에서 LLM + Workflow 구조의 하이브리드 구조를 이용하여 강건성을 보장하고 있습니다.