[Paper] 결정 트리의 근사 최적 액티브 러닝

Source: arXiv - 2512.03971v1

개요

이 논문은 심볼릭 능동 학습 프레임워크를 도입하여, 멤버십 쿼리(즉, “이 입력에 대한 출력은 무엇인가?”)만을 이용해 알려지지 않은 이진 결정 트리를 복원한다. 제한된 깊이의 트리 전체 공간을 SAT 공식으로 표현하고 근사 모델 카운팅을 활용함으로써, 모든 후보 트리를 열거하지 않고도 거의 최적에 가까운 쿼리를 선택할 수 있다. 그 결과, 매우 적은 수의 쿼리만으로 올바른 트리를 수렴시키면서도 검증이 중요한 분야에 적합한 형식적 보장을 제공한다.

주요 기여

• 가설 공간의 SAT 기반 인코딩: 주어진 깊이 이하의 모든 결정 트리를 CNF 공식으로 압축하여 명시적 열거를 피한다.
• 근사 모델 카운팅을 통한 쿼리 선택: ApproxMC를 사용해 각 잠재적 쿼리가 버전 공간을 얼마나 축소시킬지 추정함으로써, 정보 이론적으로 거의 최적에 가까운 쿼리를 선택한다.
• 증분 버전 공간 정제: 각 쿼리 후에 관측된 결과를 CNF에 추가하여, 처음부터 다시 구성하지 않고도 최신 상태를 유지한다.
• 함수적 동등성 폴백: ApproxMC가 더 이상 진행되지 않을 때, SAT 기반 동등성 검사를 통해 남은 가설들이 함수적으로 동일한지 확인하고, 조기 종료를 가능하게 한다.
• 실험적 검증: 합성 및 벤치마크 결정 트리 데이터셋에 대한 실험에서, 몇 개 안 되는 쿼리만으로 수렴함을 보여주며, 휴리스틱 기반 능동 학습자보다 우수함을 입증한다.

방법론

1. 심볼릭 가설 인코딩

   • 학습자는 최대 깊이 d를 고정한다.
   • 각 내부 노드는 어떤 특성을 테스트하는지와 어느 자식 분기로 갈지를 나타내는 불리언 변수들로 표현된다.
   • 가능한 모든 트리 집합은 현재 관측과 일치하는 트리만을 만족시키는 CNF 공식 Φ가 된다.

2. 쿼리 후보 생성

   • 가능한 모든 입력 벡터 x(또는 샘플링된 부분집합)마다, 학습자는 두 개의 조건부 공식—답이 0이라고 가정한 경우와 1이라고 가정한 경우—를 만든다.

3. 근사 모델 카운팅

   • ApproxMC는 각 가정 하에서 Φ의 만족 할당 수를 추정한다.
   • x에 대해 질문했을 때의 정보 이득은 카운트 감소량으로 근사한다. 예: |Φ| - max(|Φ ∧ answer=0|, |Φ ∧ answer=1|).

4. 쿼리 선택

   • 추정된 이득이 가장 큰 입력을 오라클(알려지지 않은 트리)에게 질문한다.

5. 버전 공간 업데이트

   • 관측된 답을 강제하는 절을 Φ에 conjunction하여, 허용 가능한 트리 공간을 축소한다.

6. 동등성 검사(폴백)

   • ApproxMC가 연속 여러 단계에서 동일한 카운트를 반환하면, SAT 솔버가 남은 모든 모델이 동일한 부울 함수를 계산하는지 확인한다. 그렇다면 구문적으로 여러 트리가 남아 있더라도 학습을 종료한다.

이 루프는 버전 공간이 단일 함수 모델로 수축될 때까지 반복된다.

결과 및 발견

실험을 통해 근사 카운팅이 실제 정보 이득에 대한 신뢰할 수 있는 대리 변수임이 확인되었으며, 정확한 카운팅의 조합 폭발 없이 거의 최적에 가까운 쿼리 전략을 가능하게 한다.

실용적 함의

• 보안 감사를 위한 모델 추출 – 공격자(또는 감사자)는 최소한의 탐색으로 독점적인 결정 트리 분류기를 복원할 수 있어, 블랙박스 모델을 역공학하면서도 추출 과정에 대한 형식적 보장을 제공한다.
• 소프트웨어 검증에서 테스트 케이스 생성 – 구성 요소의 동작이 제한된 깊이의 결정 트리로 표현될 수 있을 때, 이 방법은 논리를 완전히 특성화하는 최소 입력 집합을 자동으로 합성하여 회귀 테스트와 형식 증명 생성을 가속한다.
• 인터랙티브 디버깅 도구 – IDE 플러그인은 개발자에게 목표 “what‑if” 질문을 제시해 버그를 일으키는 정확한 결정 규칙을 찾아내며, 수동 테스트 실행 횟수를 크게 줄인다.
• 자원 제한 능동 학습 – IoT나 엣지 환경처럼 각 쿼리가 비용(센서 읽기, 네트워크 왕복 등)을 수반하는 경우, 이 접근법은 각 쿼리가 불확실성을 최대한 감소시키도록 보장하여 배터리 수명과 대역폭을 연장한다.

핵심 엔진이 SAT 솔버와 근사 카운터이므로, Z3, MiniSat, ApproxMC 등 기존 검증 파이프라인에 플러그인 형태로 쉽게 통합할 수 있다.

제한점 및 향후 연구

• 깊은 트리로의 확장성: CNF 크기가 깊이에 따라 지수적으로 증가한다. ApproxMC가 열거를 완화하긴 하지만, 깊이 > 7인 트리는 메모리 부담이 커진다.
• 특성 공간 가정: 본 방법은 유한하고 이산적인 불리언 특성 집합을 전제로 한다. 수치형이나 범주형 특성으로 확장하려면 이진화와 같은 추가 인코딩 기법이 필요하다.
• ApproxMC 보장에 대한 의존성: 근사 카운팅은 확률적 오류 한계를 갖는다; 특수한 경우에는 쿼리 선택이 최적이 아닐 수 있다.
• 향후 방향: 저자들은 (1) SAT 인코딩과 그래디언트 기반 학습기를 결합한 하이브리드 심볼릭‑통계 모델, (2) 혼합형 데이터에 대한 확장 등을 제안한다.