Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

기술 요약: 로컬 소형 언어 모델을 위한 자원 인식형 신경-기호 추론(Neuro-Symbolic Reasoning)

문제 정의
소형 언어 모델(SLM)은 개인정보 보호, 오프라인 가용성, 운영 비용 절감과 같은 로컬 실행의 이점을 제공한다. 그러나 제한된 용량으로 인해 신뢰할 수 있는 추론을 달성하기 위해 반복적인 샘플링(자기 일관성, self-consistency)과 같은 전략이 필요할 수 있으며, 이는 로컬 모델 호출, 토큰 생성 및 직렬 지연 시간을 배가시킨다. 신경-기호적 접근 방식이 존재하기는 하지만, 이들은 종종 일반적인 정리 증명(theorem-proving) 능력을 가정하거나 소비자용 하드웨어의 구체적인 자원 제약을 간과한다. 본 연구가 다루는 핵심 문제는, 구조화된 추론 작업에서 정확도를 희생하지 않으면서, 로컬 SLM의 제약 조건 내에서 경계가 정해진 검증 가능한 신경-기호 파이프라인이 반복적인 로컬 신경 샘플링을 대체할 수 있는지 여부이다.

방법론: VFR-LLM 파이프라인
저자들은 추론의 부담을 신경 모델에서 결정론적 솔버(deterministic solver)로 오프로드하기 위해 설계된 5단계 아키텍처인 VFR-LLM(Verifiable Formalization and Repair) 파이프라인을 제안한다:

1. 정형화(Formalization): SLM은 자연어 문제를 **타입이 지정된 유한 도메인 규칙 및 제약 표현식(typed finite-domain rule-and-constraint representation)**으로 번역한다. 이 중간 언어는 근거가 명확한 사실(grounded facts), 안전한 Horn 스타일 규칙, 그리고 유한 도메인 제약(예: 순서, 절대 위치)을 포함한다. 결정적으로, 모델은 추출된 모든 제약 조건을 원문과 연결하는 **소스 스팬(source spans)**을 제공해야 한다.
2. 커버리지 검사(Coverage Checking): 검증 레이어는 정형화된 내용이 소스 텍스트에 근거하고 있는지, 지원되지 않는 규칙이나 알 수 없는 엔티티가 존재하지 않는지 검사한다.
3. 솔버 실행(Solver Execution): 결정론적 솔버(평가된 작업에 대한 정확한 열거형 솔버)가 정형화된 프로그램을 처리하여 만족하는 할당(예: 엔티티의 전체 순서)을 찾는다.
4. 수정(Repair): 솔버가 실패하거나 진단 결과 정형화 오류(예: 인자 순서 역전 또는 구문 문제)가 나타나면, 결정론적 수정 모듈이 오직 소스 스팬과 솔버 진단에만 기반하여 로컬 편집을 적용한다. 이 단계에서는 추가적인 모델 호출이나 정답(gold answers)이 사용되지 않는다.
5. 답변 생성(Answer Generation): 최종 답변은 솔버의 출력으로부터 도출되며, 검증된 제약 조건과 연결된다.

대상 정형식은 의도적으로 겸손하게 설정되었다. 즉, 모델의 번역 부담을 관리 가능한 수준으로 유지하기 위해 함수 기호(function symbols)와 무한 양화(unbounded quantification)를 제외한 Datalog 스타일의 유한 도메인 언어를 사용한다.

주요 기여

1. 추적 가능한 표현(Traceable Representation): 모든 추출된 사실에 대해 소스 스팬을 요구하는 타입 지정 유한 도메인 규칙 및 제약 정형식을 정의하여, 번역 단계의 감사 가능성(auditability)을 확보하였다.
2. 검증 및 수정 루프(Verification and Repair Loop): 반복적인 샘플링에 의존하는 대신, 소스에 근거한 검증 및 결정론적 수정을 사용하여 솔버 실행 전 정형화 실패를 식별하고 수정하는 파이프라인을 구현하였다.
3. 로컬 평가 매트릭스: Apple Silicon (M3 Pro) 환경의 LM Studio에서 세 가지 모델 제품군(Qwen3-4B, Microsoft Phi-4-mini-reasoning, Gemma-3n-E4B)을 사용하여 종합적인 평가를 수행하였다. 벤치마크에는 생성된 순수 선후 관계(pure-precedence) 작업, 생성된 타입 지정 선후 관계 작업, 그리고 BIG-Bench Hard (BBH) 논리적 연역에서 파생된 두 가지 서브셋(쌍별 및 확장형)이 포함된다.
4. 자원 인식형 비교: 직렬 자기 일관성($k=5$) 및 비용 인식 적응형 자기 일관성 베이스라인과 비교하여 정확도, 모델 호출 횟수, 총 토큰 수, 직렬 지연 시간을 엄격하게 비교하였다.

결과
실증적 결과는 VFR-LLM 접근 방식의 경계가 정해진 모델 의존적(bounded and model-dependent) 효용성을 보여준다:

• Qwen3-4B 성능:

  • 순수 선후 관계(Pure Precedence): 단 한 번의 모델 호출로 0.983의 정확도를 달성하였으며, 이는 자기 일관성(정확도 0.700, 5회 호출)을 크게 상회하며 총 토큰 수를 34.4% 감소시킨 결과이다.
  • BBH-Extended (공개 소스): 자기 일관성(0.283) 및 직접 답변(0.317)에 비해 0.933의 정확도를 달s성하였다. 정형화 과정으로 인해 총 토큰 수는 약간 증가했으나, 모델 호출(1회 vs 5회)과 직렬 지연 시간(11.32s vs 16.54s)을 줄였다.
  • 타입 지정 제약(Typed Constraints): 직접 답변 방식이 더 정확하고 저렴했기에, 이 계층에서는 성능이 "차단(blocked)"되었다.

• Gemma-3n-E4B 성능:

  • 순수 선후 관계 작업에서 강한 개선을 보였다 (0.683 vs 자기 일관성의 0.367).
  • BBH-extended 작업에서의 결과는 미미하였으며 (0.375 vs 직접 답변의 0.350), 정확도 향상이 통계적으로 유의미하지 않았다.
  • 타입 지정 제약 작업은 혼재된 결과를 보였으며, 지연 시간이 직접 답변보다 높은 경우가 많았다.

• Phi-4-mini-reasoning:

  • 타입 지정 제약에서 심각한 정형화 실패를 보였으며, 직접 답변 방식에 비해 부정적인 결과를 초래했다.

• 강건성 체크(Robustness Checks):

  • 적응형 베이스라인: 비용 인식 적응형 자기 일관성 베이스라인(호출 횟수를 5회에서 약 4.2회로 감소)과 비교했을 때도, Qwen의 경우 VFR-LLM은 선후 관계 및 BBH-extended 작업에서 상당한 정확도 우위를 유지했다.
  • 추적 가능성(Traceability): 높은 정확도는 높은 "완전 추적 가능(fully traceable)" 비율(소스에 근거한 제약 조건)과 강력하게 상관관계가 있었다. Qwen은 BBH-extended에서 0.942의 추적 가능률을 기록한 반면, Gemma는 0.292에 그쳐 성능 차이를 설명해주었다.
  • 결정론적 절제 실험(Deterministic Ablations): 타입 지정 유한 도메인 솔버는 BBH-extended 인스턴스의 100%를 해결한 반면, 선후 관계 전용 솔버는 20.8%만을 해결하였다. 이는 해당 작업들에 있어 확장된 정형식의 필요성을 확인시켜 준다.

의의 및 주장
본 논문은 신경-기호적 방식이 모든 작업에서 로컬 LLM의 성능을 보편적으로 향상시키거나 컴퓨팅을 줄인다고 주장하지 않는다. 대신, 다음과 같은 **경계된 주장(bounded claim)**을 제시한다:

1. 조건부 자원 절감: VFR-LLM은 명시적 제약(특히 순서 및 유한 도메인 논리)이 존재하는 구조화된 작업에서, 직접 답변 방식이 충분히 정확하지 않을 때 자기 일관성을 대체할 수 있는 유효한 자원 인식형 대안이다.
2. 모델 의존성: 파이프라인의 성공은 소스에 근거한 충실한 정형화를 생성하는 SLM의 능력에 크게 의존한다. 이 방법은 특정 계층의 Qwen에는 잘 작동하지만, 더 복적인 타입 시나리오의 Phi나 Gemma에서는 실패하거나 미미한 이득만을 제공한다.
3. 감사 가능성: 주요 기여는 단순히 정확도가 아니라, 반복적인 신경 생성의 오버헤드 없이도 추적 가능한 추론 궤적을 제공하고 실패(예: 번역 오류와 솔버 실패의 구분)를 진단할 수 있는 능력이다.
4. 일반적 컴퓨팅 감소 불가: 본 논문은 심볼릭 레이어를 추가한다고 해서 자동으로 컴퓨팅 비용이 낮아지는 것은 아니라고 결론짓는다. 예를 들어 타입 지정 작업의 경우, Qwen에서는 직접 답변 방식이 여전히 가장 효율적이고 정확한 옵션이다. 이 방법은 모든 경우를 위한 범용 도구가 아니라, 특정 범위의 문제 클래스에 대한 전문화된 대안이자 진단 도구로 보는 것이 적절하다.