기술 요약: 검증기 기반 간섭 탐색 (Verifier-Grounded Interference Search)

문제 정의

언어 모델 추론 시스템은 동일한 환경 상태로 수렴하는 서로 다른 궤적(trajectories)에 상당한 계산 자원을 소비하곤 한다. 서로 다른 산술 유도 과정이나 프로그램 수정 시퀀스가 동일한 잔여 값 멀티셋(multiset) 또는 정형화된 프로그램 상태를 생성할 수 있음에도 불구하고, 기존의 추론 시스템은 이를 별개의 경로로 취급하여 중복된 탐색, 모델 평가 및 외부 실행을 초래한다. 핵심 과제는 추론 경로가 상태, 증거 또는 실패를 공유할 때, 어떻게 계산적 객체(환경 상태, 정책 제안, 실행 조건 등)를 혼동하지 않으면서 논리적 정확성을 유지하며 상호작용해야 하는지를 결정하는 것이다.

Chain-of-Thought, Tree of Thoughts, Graph of Thoughts와 같은 기존 방식들은 정보를 집계하거나 분기 구조를 탐색하지만, 목표 도달 가능성을 보존하는 '근사적 의미 유사성'과 '정확한 상태 등가성'을 구분하는 공식적인 메커니즘이 부족하다. 또한, 기존 방법들은 논리적 정확성, 해결 확률, 계산 작업량 및 실제 실행 시간(wall-clock latency)을 자주 혼동하며, 이로 인해 상태 공유, 학습된 가지치기(pruning), 또는 병렬 실행의 구체적인 이점을 분리해내는 데 어려움을 겪는다.

방법론

본 논문은 **검증기 기반 간섭 탐색(Verifier-Grounded Interference Search, IS)**을 제안하며, 이는 추론 상호작용을 각각의 구체적인 정당성 조건을 가진 네 가지 논리적으로 구별되는 연산자로 분해한다.

1. 정확한 상태 병합 (Exact State Merging): 궤적들은 그 상태가 *연속성 보존 등가 관계(continuation-preserving equivalence relation)*를 만족할 때만 병합된다. 이는 정형화된 매핑 $\kappa: S_x \to K_x$를 통해 공식화된다. 프레임워크는 환경 등가성(가정 1: 목표 및 전이 일치성 충족)과 정책 등가성(제안자가 정형화된 상태에만 의존하거나 제안 관련 정보를 모두 유지해야 함)을 구분한다. 산술 작업의 경우, 정형화된 키는 $(y, \text{sort}(V), \rho)$로 정의된다(여기서 $y$는 목표값, $V$는 값의 멀티셋, $\rho$는 규칙 명세이다). 결정적으로, 상태는 병합되지만, 실행 가능한 솔루션을 재구성할 수 있도록 증거(witnesses)(원래 피연산자의 출처)는 유지된다.
2. 인증된 배제 (Certified Exclusion): 검증기 기반 증거(예: 기호적 경계 또는 엑조스틱한 후속 상태 분석)가 목표에 도달할 수 없음을 확립할 때만 상태가 제거된다. 이는 유한 비순환 몫 그래프(finite acyclic quotient graphs)에서의 건전한 역방향 반박(backward refutation)에 의존하며, 특정 상태를 사멸된 것으로 인증하기 위해 법적 후속 상태에 대한 전수 조사를 요구한다.
3. 학습된 억제 (Learned Inhibition): 이전의 실패로부터 얻은 예측적 증거를 사용하여 관련 후보의 우선순위를 낮추되, 이를 불가능하다고 단정 짓지는 않는 휴리스틱 메커니즘이다. 이는 학습된 판단기 $J_\phi$와 억제 항 $I_\psi$를 통해 구현되며, 검증된 실패와의 임베딩 유사성에 따라 액션 로짓(action logits)을 수정한다. 본 논문은 이러한 가지치기로 인해 유효한 목표 궤적을 잃을 확률에 대한 경로별 경계(pathwise bound)를 도출한다.
4. 실행 스케줄링 (Execution Scheduling): 상태 처리 및 외부 연산의 타이밍을 제어한다. 이 프레임워크는 배리어 대기(barrier waiting)를 줄이고 불필요한 작업을 조기에 취소하기 위해 비동기 실행(파이프라인 DAG)을 지원하며, 이는 동기식 배리어 실행과 구별된다.

본 시스템은 다음 네 가지 실험 영역에서 평가되었다:

• Countdown (산술): 정형화된 상태 키와 전수 검증을 통해 제어된 테스트를 수행한다.
• 반례 유도 탐색 (Counterexample-Guided Search): 이진 결정 작업에서 ROBDD 및 캐시된 팩터 솔버를 사용하여 인증된 배제를 테스트한다.
• MBPP (프로그램 합성): 샌드박스 실행 환경 하에서 비동기 실행 및 공유 접두사 재사용을 평가한다.
• 고유 잠재 가설 (Native Latent Hypothesis): Qwen3-4B 모델의 지속적인 잠재 슬롯이 서로 다른 추론 가설을 인코딩하고 인과적으로 제어할 수 있는지 조사한다.

주요 기여

• 이론적 공식화: 본 논문은 목표 보존 상태 등가성을 위한 충분 조건(정리 1)과 증거 보존(명제 2)을 확립한다. 또한 전수 후속 상태 커버리지 하에서의 건전한 역방향 반박(정리 3)을 증명하고, 학습된 억제를 통한 유효 궤적 손실 위험에 대한 경로별 경계(정리 4)를 도출한다.
• 메커니즘 분리: 정확한 병합(논리적 정확성), 인증된 배제(논리적 일반화), 학습된 억제(휴리스틱 우선순위 지정), 스케줄링(지연 시간 최적화)을 명시적으로 분리하여, 이들이 서로 다른 가정 하에 작동하며 단일한 "병렬 추론" 이점으로 통합 평가될 수 없음을 주장한다.
• 경험적 분해: 연구는 실험 보고를 종합하여 이러한 메커니즘들의 효과를 격리한다. 정형화된 상태 키가 존재할 때 정확한 병합이 산술 탐색의 해결율을 개선함을 입증하는 동시에, 전체 아키텍처가 제한된 계산 예산 하에서 전통적인 최선 우선 탐색(best-first search)을 항상 압도하는 것은 아님을 보여준다.

결과

• 정확한 상태 병합: 200개의 5개 숫자 Countdown 인스턴스에 대한 네이티브 온라인 평가에서, 정확한 병합은 해결율을 16.5%(병합 없음)에서 27.0%(병합 + 학습된 억제)로 향상시켰으며, 22회의 이득과 단 1회의 손실을 기록했다 ($p = 5.72 \times 10^{-6}$). 이는 적절한 정형화된 표현이 있을 때 수렴하는 상태를 식별하는 것이 탐색 효율성을 높임을 확인시켜 준다.
• 학습된 억제: 정확한 병합은 유지하되 학습된 결합(learned coupling)을 비활성화했을 때, 해결율은 22.5%(45/200)로 떨어졌다. 학습된 억제의 점진적 이득은 4.5 퍼센트 포인트(15회 이득, 6회 손실)였으며, 이는 통계적으로 유의미하지 않았다 ($p = 0.0784$). 또한, 최종 훈련된 정책은 초기화 대비 능력 퇴보(regression)를 보였는데, 이는 보조 메커니즘 목적 함수를 최적화하는 것이 부모 모델의 추론 능력을 보존하는 것을 보장하지 않음을 시사한다.
• 예산 민감도: 1,000개 인스턴스의 더 큰 규모의 Countdown 실험에서, 전통적인 최선 우선 탐색은 엄격한 상태 작업 예산 하에서 전체 폭 16의 IS 프런티어를 실질적으로 압도했다 (예산 100에서 72.3% vs 0%). IS 시스템은 훨씬 높은 예산(500 이상)에서야 대등한 수준에 도달했다 (98.8% vs 100%). 이는 그래프 유지 관리 및 동기화의 오버헤드가 계산 자원이 부족할 때 해로울 수 있음을 나타낸다.
• 인증된 배제: 반례 유도 탐색에서 ROBDD와 캐시된 팩터 표현 모두 검증 실패를 인증된 무효 영역으로 일반화함으로써 90개의 태스크를 모두 해결했다. 반면, 완전한 실패 후보만을 기억하는 전략은 하나도 해결하지 못했는데, 이는 점 단위의 메모리보다 논리적 일반화의 가치를 입증한다.
• 비동기 실행: 64개의 MBPP 태스크에서 비동기 파이프라인 실행은 평균 완료 지연 시간을 2.265초에서 2.064초로 줄였으며(8.9% 감소), 배리어 실행과 동일한 해결 횟수(47/64)를 유지했다. 이러한 지연 시간 이득은 주로 총 추측 작업의 감소가 아니라, 조기 검증 및 불필요한 형제 작업의 취소를 통해 달성되었다.
• 잠재 가설: 지속적인 잠재 슬롯은 기하학적 다양성을 증가시켰으나(유효 랭크가 1.00에서 3.05로 상승), 후보 디코딩 정확도는 68.5%에 그쳐 사전 선언된 80% 기준을 충족하지 못했다. 이는 기하학적 다양성만으로는 추론 대안의 의미적 분리를 보장할 수 없음을 시사한다.

의의 및 주장

본 논문은 검증기 기반 간섭 탐색이 특정 추론 메커니즘이 언제 유효하고 유익한지를 결정하기 위한 모듈형 프레임워크를 제공한다고 주장하며, 협력적 추론이 전통적인 탐색을 보편적으로 압도한다고 주장하는 것이 아님을 밝힌다.

• 정확한 병합은 정형화된 상태 키를 사용할 수 있는 검증된 산술 탐색을 개선하는 데 가장 강력한 메커니즘임이 입증되었다.
• 인증된 배제는 검증 실패가 논리적으로 일반화될 수 있을 때 구조화된 가설 공간을 효과적으로 압축한다.
• 비동기 스케줄링은 조기 취소를 가능하게 하여 지연 시간을 줄이지만, 이 이점은 작업 종료 패턴에 따라 달라지며 본질적으로 해결 확률을 높이지는 않는다.
• 학습된 억제는 조건부 효과에 머물러 있다. 현재 실험에서 이는 작고 통계적으로 모호한 이득만을 제공했으며, 훈련 과정에서의 능력 퇴보 문제를 극복하지 못했다.
• 잠재 가설 추적은 아직 미완성이다. 기하학적 다양성의 증가가 신뢰할 수 있는 의미적 디코딩이나 별개의 가설에 대한 인과적 제어로 이어지지는 않았다.

저자들은 이 프레임워크의 주요 가치가 논리적 정확성, 예측 품질, 계산 작업량 및 지연 시간을 분리해내는 능력에 있다고 결론짓는다. 그들은 "병렬 추론의 우월성"에 대한 광범위한 주장은 근거가 부족하다고 주장하며, 대신 상태 공유, 검증기 기반 배제, 그리고 동시 실행의 이점은 특정 태스크 구조, 정확한 등가 관계의 가용성, 그리고 계산 예산에 크게 의존한다는 점을 강조한다. 향후 연구는 메커니즘 훈련 시 부모 모델의 능력을 보존하고, 잠재 표현과 별개의 추론 대안 사이의 인과적 연결을 확립하는 데 집중해야 한다.