기술 요약: Theoria – 비정형 추론 상태에 대한 재작성-수용성 검증 (Rewrite-Acceptability Verification over Informal Reasoning States)

1. 문제 정의

본 논문은 AI 추론의 "신뢰 문제(trust problem)"를 다룬다. 즉, AI가 생성한 답변이 언제 정당한 신뢰를 형성해야 하는지를 구별하는 문제이며, 특히 안전이 중요한 분야(과학, 법률, 금융, 의학)에서 중요하다. 현재의 접근 방식들은 다음과 같은 이분법적 한계에 직면해 있다:

• 형식적 증명 보조 도구 (예: Lean, Coq): 수학적 확실성을 제공하지만, 비정형 자연어 요구사항을 자동 형식화(autoformalizing)하는 데 드는 높은 비용과 의미론적 취약성 때문에 대부분의 문제 분포를 커버하지 못한다.
• 스칼라 LLM 판사 (Scalar LLM Judges): 넓은 범위를 커버하지만, 감사가 불가능한 불투명한 점수를 생성하며, LLM 자체의 일관성 문제를 상속받고, 왜 증명이 결함이 있는지(예: 숨겨진 전제, 조작된 인용)를 식별하지 못한다.

핵심 과제는 완전한 형식화를 요구하지 않으면서도 비정형 추론을 검증하는 동시에, 오류(특히 명시되지 않은 가정이나 논리적 비약)를 가시화하고 감사 가능하게 만드는 것이다.

2. 방법론: Theoria 아키텍처

Theoria는 솔버(solver)의 자연어 답변을 증명 증거(proof witness), 즉 타입이 지정된 상태 전이(typed state transitions)의 시퀀스로 재작성하는 검증 아키텍처를 도입한다.

2.1 재작성 프레임워크 (The Rewrite Framing)

Theoria는 증명을 하나의 산문 블록으로 취급하는 대신, 이를 상태 궤적 $(S_0, S_1, \dots, S_n)$으로 분해한다.

• 상태 (State, $S_i$): 확립된 사실들과 현재의 목표를 나타내는 문자열의 순서 있는 리스트.
• 전이 (Transition): $S_{i-1}$에서 $S_i$로의 단계는 특정 **정당화 유형(justification type)**에 의해 허가된다:
  1. 인용 (Citation): 정리(theorem), 정의(definition), 또는 추론 규칙.
  2. 연산 (Computation): 산술 또는 기호 조작.
  3. 문제 제시 (Problem Given): 문제 텍스트에 명시적으로 기술된 사실들.
• 변화 완결성 불변량 (The Completeness-of-Change Invariant): $S_{i-1}$과 $S_i$ 사이의 모든 의미론적 차이는 명시된 정당화에 의해 설명되어야 한다. 만약 어떤 전제가 새로운 상태를 도출하기 위해 필요하지만, 이전 상태에 존재하지 않거나 정당화에 포함되어 있지 않다면, 이는 **무허가 변이(unlicensed mutation)**로 간다.

2.2 검증 파이프라인

시스템은 Solve $\to$ Formalize $\to$ Judge $\to$ Filter $\to$ Repair의 루프로 작동한다.

1. Solver (솔버): 자연어 솔루션을 제안한다 (웹 검색 등 도구 증강 방식 활용).
2. Formalizer (형식화 도구): 솔루션을 상태-전이 증거로 재작성한다. 이는 전제가 사용되기 전에 반드시 명시적이어야 함을 강제한다.
3. 병렬 특화 판사 (Parallel Specialized Judging):
   • 연산 판사 (Computation Judges): 처음부터 단계를 재계산한다.
   • 인용 판사 (Citation Judges): 특정 상태 차이(diff)에 대해 인용된 정리의 존재 여부와 적용 가능성을 검증한다.
   • 문제 제시 판사 (Problem-Given Judges): 원문 텍고와 대조하여 사실을 확인한다.
   • 초기 상태 판사 (Initial-State Judge): $S_0$를 감사하여 시작 단계에서 정당화되지 않은 전제가 도입되지 않았는지 확인한다.
   • 모든 판사는 타당성을 확인하기보다 오류를 찾아내도록 적대적으로 프롬프트된다.
4. 편집증적 필터 (Pedantry Filter): 실질적인 오류와 비정형 표기법이나 압축에 대한 과도한 엄격함을 구분한다.
5. 관습 승격 (Convention Lift): 표준적이고 인용 가능한 도메인 관습이 거절 사유를 해결할 수 있다면, 해당 가정을 명시적으로 기록하는 조건 하에 단계를 수용한다.
6. 인증 또는 거절 (Certify-or-Decline): 시스템은 이진 결정을 출력한다. 모든 단계가 통과하거나(또는 관습 승격을 통해 해결되거나) 하면, 답변은 **인증(Certified)**된다. 만약 어떤 단계라도 실패하고 범위 내에서 복구될 수 없다면, 답변은 **거절(Declined)**된다.

3. 주요 기여

본 논문의 주요 기여는 단순히 여러 모델을 사용하거나 단계별 체크를 수행하는 것이 아니라, 구체적인 **증거 형식(witness format)**과 그 이론적 보장에 있다:

• 노출 보장 (Exposure Guarantee, Proposition 4.4): 변화 완결성 불변량은 숨겨진 전제(글로벌 추론 공백)를 로컬하고 관찰 가능한 무허가 변이로 전환한다. 숨겨진 전제는 새로운 요소로서 상태에 나타나거나(라이선스 체크를 유발), 불변성을 위반해야 한다. 이는 오류를 로컬 판사들에 의해 탐지될 수 있는 표면 위로 끌어올린다.
• 오류 클래스 예측 (Error-Class Predictions, Proposition 4.5): 이 형식은 검증의 이점이 다음 영역에 집중될 것임을 예측한다:
  • 숨겨진 전제: 무허가 변이로 노출됨.
  • 조작된 인용: 증거가 명시적으로 타입화되어 차이(diff)와 대조되므로 노출됨.
  • 이점 없음: 산술 오류 및 정리 오적용(정리는 존재하나 잘못 적용된 경우)은 구조적 노출 이점을 얻지 못한다. 이는 오류가 구조적 문제가 아닌 의미론적 문제이기 때문이다.
• 실패의 분해 (Decomposition of Failure): 논문은 노출 실패(Exposure Failure)(형식이 오류를 숨기는 경우)와 판사 실패(Judge Failure)(판사가 노출된 오류를 놓치는 경우)를 구분한다. Theoria는 전자를 최소화하는 것을 목표로 하며, 후자는 경험적으로 해결하도록 남겨둔다.

4. 실험 결과

평가는 HLE-Verified Gold(전문가 문제 185개)와 GPQA Diamond(대학원 수준 과학 문제 65개)에서 수행되었다.

4.1 HLE-Verified Gold에서의 성능

• 인증 정밀도 (Certified Precision): 91.4% (96/105 정답)이며, 95% Wilson CI는 [84.5%, 95.4%]이다.
• 커버리지 (Coverage): 56.8% (185개 문제 중 105개 인증됨).
• 비대칭성 (Asymmetry): 거절된 답변은 인증된 답변보다 약 5.0배 더 많이 틀렸다 (오류율 42.5% vs 8.6%).
• 솔버 단독 모델과의 비교: 웹 증강 솔버는 100% 커버리지에서 83.8% 정확도를 달랐다. Theoria 파이프라인은 상당 부분의 오류를 걸러내어, 인증된 버킷 내의 오류율을 8.6%로 낮추었다.
• 전체론적 판사(Holistic Judges)와의 비교: 단일 신뢰 점수를 부여하는 전체론적 LLM 판사들은 매칭된 커버리지에서 유사한 정밀도(92.4–93.3%)를 보였다. 그러나 이들은 서로 다른 문제에서 실패했다 (Jaccard 지수 0.14–0.36). 이는 오류 커버리지가 상호 보완적임을 나타낸다.

4.2 적대적 강건성 (Adversarial Robustness)

95개의 독성 증명(특정 오류 유형을 주입함) 벤치마크에서:

• 전체 탐지율: Theoria는 94.7% (90/95)를 잡아냈으며, 이는 전체론적 판사의 83.2% (79/95)보다 높았다 ($p = 0.0017$).
• 오류 클래스별 세부 사항:
  • 숨겨진 전제: Theoria 90.6% vs 전체론적 판사 62.5% (28 pp 차이).
  • 조작된 인용: Theoria 100% vs 전체론적 판사 90%.
  • 산술/정리 오적용: 성능이 동일했다 (~95% 및 ~93% 각각). 이는 구조적 이점이 없다는 이론적 예측을 확인시켜 준다.

4.3 분포 외 데이터 (GPQA Diamond)

• 인증 정밀도: 97.1% (33/34).
• 커버리지: 52.3%.
• 다른 벤치마크에서도 높은 정밀도를 보인 것은 "인증 또는 거절" 경계가 벤치마크 특유의 캘리브레이션이 아니라 추론의 형식화 가능성에 의해 결정됨을 시사한다.

4.4 앙상블 잠재력

Theoria와 전체론적 판사가 서로 다른 문제 집합에서 실패하기 때문에, 앙상블 전략(예: 다수결)은 단일 방법론보다 뛰어난 58.9% 커버리지에서 93.6% 정밀도를 달성했다.

5. 의의 및 주장

본 논문은 Theoria가 가공되지 않은 LLM 출력과 형식적 검증 사이의 간극을 메우는 확장 가능한 오버사이트(scalable oversight) 메커니즘을 제공한다고 주장한다.

• 감사 가능성 (Auditability): 스칼라 점수와 달리, Theoria는 각 단계를 독립적으로 도전할 수 있는 인간이 읽을 수 있는 증명 트레이스를 생성한다.
• 구조적 이점 (Structural Advantage): 시스템은 판사가 산문으로부터 증명을 재구성하도록 의존하지 않는다. 대신, 검증 작업을 로컬 질문으로 축소한다: "이 정당화가 이 특정 상태 변화를 허가하는가?"
• 상호 보완성 (Complementarity): 논문은 Theoria가 전체론적 판사를 대체하는 것이 아니라 보완하는 접근 방식이라고 주장한다. 오류에 대한 낮은 Jaccard 중첩은 구조적으로 다른 검증 아키텍처를 결합하는 것이 더 높은 신뢰성을 낳는다는 것을 보여준다.
• 한계점 (Limitations): 저자들은 Theoria가 상태 변이를 일으키지 않는 오류(예: $S_0$에서의 미묘한 문제 해석 오류)를 탐지할 수 없음을 인정하며, 현재 LLM 판사에 의존하고 있으나 (Lean이나 SMT 솔버와 같은) 형식적 백엔드와 호환되도록 설계되었음을 밝힌다.

요약하자면, The via Theoria는 비정형 추론에 변화 완결성 불변량을 강제함으로써, 표준적인 전체론적 평가가 놓치는 숨겨진 가정과 조작된 증거를 표면화하여 AI 생성 추론에 대한 신뢰의 엄격하고 감사 가능한 경계를 제공할 수 있음을 입증한다.