기술 요약: 트랜스포머 프로그램의 합성과 검증

문제 정의

대규모 언어 모델 (LLM) 의 기반 아키텍처인 트랜스포머는 공식적으로 분석하기 매우 어렵기로 유명합니다. 트랜스포머는 표현력이 풍부하고 병렬화가 가능하지만, 그 속성을 검증하는 것은 결정 불가능 (undecidable) 하며, 사고의 연쇄 (Chain of Thoughts) 를 추가하면 튜링 완전 (Turing-complete) 해집니다. 이를 해결하기 위해 연구자들은 트랜스포머의 행동을 정확한 의미론으로 포착하기 위해 RASP(제한된 접근 시퀀스 처리 언어) 와 그 변형인 C-RASP(계수 RASP) 와 같은 선언적 언어를 개발했습니다.

그러나 C-RASP 와 트랜스포머 간의 이론적 연결에도 불구하고, 두 가지 중요한 격차가 남아 있습니다:

1. 검증: C-RASP 프로그램을 자동으로 검증하는 방법이 없습니다. C-RASP 가 자명한 언어를 인식하는지 확인하는 것은 일반적인 경우 결정 불가능하며, 언어 동등성이나 포함성과 같은 속성을 분석할 수 있는 실용적인 도구는 존재하지 않습니다.
2. 합성: 예제로부터 C-RASP 프로그램을 자동으로 학습하거나 합성하는 알려진 방법이 없습니다. 기존 접근 방식은 신경망을 훈련하고 규칙을 추출하는 데 의존하는데, 이는 종종 구현 가능한 번역을 산출하지 못하거나 이상화된 가정을 요구합니다.

본 논문은 C-RASP 프로그램의 검증과 합성을 위한 최초의 자동 기술을 개발함으로써 이러한 과제를 해결합니다.

방법론

1. Lustre 로의 축소 (Reduction) 를 통한 검증

저자들은 임베디드 시스템에 사용되는 동기식 데이터플로우 언어인 Lustre와 C-RASP 간의 공식적 연결을 확립합니다.

• 번역: C-RASP 프로그램은 Lustre 노드로 번역됩니다. 이 번역은 C-RASP 규칙을 Lustre 변수 (부울 및 정수 스트림) 로 매핑합니다.
  • 계수 연산자: C-RASP 의 계수 연산자 #φ(조건 φ가 성립하는 위치를 계수) 는 무한 스트림에 걸쳐 값을 누적하는 보조 정수 변수를 사용하여 Lustre 에서 시뮬레이션됩니다.
  • 유한 대 무한: C-RASP 는 유한 단어에서 작동하고 Lustre 는 무한 스트림에서 작동하므로, 입력은 특정 스트림 종료 마커 (#) 와 영구성 마커 (Ω) 를 가진 무한 스트림으로 인코딩됩니다.
• 모델 체킹: 번역이 완료되면, 언어 동등성, 포함성, 공허성과 같은 속성은 최신 모델 체커 (특히 Kind2) 와 최적화된 SMT 솔버 (CVC5, Z3) 를 결합하여 검증됩니다.
• 복잡도: #rs,re 연산자의 범위 매개변수가 단항 (unary) 으로 인코딩된다는 전제 하에, 번역의 크기는 다항식입니다.

2. 시뮬레이티드 어닐링을 통한 합성

본 논문은 양의 예제와 음의 예제로부터 C-RASP 프로그램을 합성하기 위해 시뮬레이티드 어닐링 기반의 지역 탐색 알고리즘을 제안합니다.

• 상태 공간: 탐색은 부울 규칙의 수 ($N_b$), 계수 규칙의 수 ($N_c$), 그리고 수치 상수의 상한 ($K$) 으로 정의된 고정된 "프로그램 형태"에 제한됩니다.
• 변이 연산자: 알고리즘은 현재 프로그램에 구문적 변이를 적용하여 상태 공간을 탐색합니다. 여기에는 다음이 포함됩니다:
  • 재샘플링: 규칙의 오른쪽 변을 완전히 교체합니다.
  • 마이크로 변이: 논리 연결사를 교체하거나, 부정을 토글하거나, 비교의 엄격함을 반전시키는 등의 국소적 변경입니다.
  • 제약: 변이는 계수 표현의 깊이 2 와 같은 얕은 구문 조각으로 제한되어, 단순하고 해석 가능한 모델을 향한 탐색을 편향시킵니다.
• 목적 함수: 점수 함수 $E(P)$는 오분류 최소화 ($\lambda_{mis}$) 를 최우선으로 하며, 그 다음 도달 불가능한 규칙 ($\lambda_U$) 과 추상 구문 트리 (AST) 의 총 크기 ($\lambda_S$) 에 대한 패널티를 부과합니다.
• 어닐링 역학: 알고리즘은 냉각 온도 스케줄에 의존하는 확률로 더 나쁜 해를 수용하여 지역 최적점에서 벗어날 수 있도록 합니다.

3. 통합 응용

저자들은 이 두 구성 요소를 두 가지 응용을 지원하는 통합 프레임워크로 통합합니다:

1. 트랜스포머 프로그램 최소화: C-RASP 프로그램이 주어지면, 시스템은 구조적으로 더 작고 동등한 프로그램을 합성합니다. 이는 지역 탐색과 동등성 검사를 번갈아 수행하며, 검증기에서 나온 반례가 탐색을 안내합니다.
2. 제약 학습: 부분 명세 (C-RASP 프로그램 $P_{spec}$) 와 레이블이 지정된 예제가 주어지면, 시스템은 예제에 적합하고 $P_{spec}$의 언어에 포함되는 ($L(P) \subseteq L(P_{spec})$) 프로그램을 합성합니다.

주요 기여

1. 최초의 자동 검증 방법: 본 논문은 C-RASP 프로그램을 Lustre 로 축소하고 모델 체킹을 활용하여 자동으로 검증하는 최초의 기술을 제시합니다. 이를 통해 언어 동등성, 포함성, 공허성을 검증할 수 있습니다.
2. 최초의 자동 합성 방법: 저자들은 중간 신경망 훈련 없이 예제로부터 직접 C-RASP 프로그램을 합성할 수 있는 지역 탐색 알고리즘 (시뮬레이티드 어닐링) 을 도입합니다.
3. 구현 및 벤치마킹: 통합된 Scala 툴체인이 구현되었으며, 정규 언어, 계수 기반 언어, 그리고 문맥 자유 언어 스타일을 포함한 문헌의 벤치마크 세트를 대상으로 평가되었습니다.

실험 결과

저자들은 Dyck-1, Majority, 그리고 다양한 Tomita 오토마타와 같은 언어를 포함한 벤치마크 세트를 사용하여 도구를 평가했습니다.

• 효율성: 도구는 300 초 타임아웃 내에서 대부분의 벤치마크에 대해 올바른 C-RASP 프로그램을 성공적으로 합성했습니다. 예를 들어, Dyck-1에 대한 프로그램 합성은 약 3.92 초가 소요된 반면, AnBnCn은 80.05 초가 소요되었습니다.
• 정확도: 합성은 C-RASP 의 표현력 내의 언어에 대해 높은 훈련 및 평가 정확도 (종종 100%) 를 달성했습니다.
• 트랜스포머와의 비교: 논문은 특정 벤치마크의 경우 올바른 언어를 달성하기 위해 트랜스포머 (예: HuggingFace 를 통한 GPT-2) 를 훈련하는 데 몇 시간이 걸릴 수 있는 반면, C-RASP 합성 도구는 몇 초 만에 작업을 완료했다고 지적합니다.
• 한계: 표현력 이론에서 예상된 바와 같이, C-RASP 의 능력을 초과하는 언어 (예: Parity, Tomita 3, Tomita 5) 는 높은 정확도로 학습할 수 없었으며, 최상의 훈련 정확도는 80% 미만으로 남았습니다.

중요성과 주장

본 논문은 C-RASP 를 단순히 트랜스포머의 표현력을 이해하기 위한 이론적 도구가 아니라, **해석 가능한 대리 모델 (interpretable surrogate model)**로 위치시킵니다. 검증과 합성을 위한 자동 방법을 제공함으로써, 저자들은 C-RASP 를 공식 방법 (FXAI) 을 사용하여 분석할 수 있으며, 신경망의 "블랙박스"적 성격과 설명 가능성 필요성 간의 격차를 해소할 수 있다고 주장합니다.

그 중요성은 다음과 같습니다:

• 실용적 결정 가능성: 일반적인 검증은 결정 불가능하지만, Lustre 로의 축소는 특정 실제 트랜스포머 행위를 검증하기 위한 실용적이고 자동화된 경로를 제공합니다.
• 직접 합성: 합성 방법은 심층 신경망 훈련의 불안정성이나 불투명성 없이 해석 가능한 프로그램을 생성하는 직접적인 경로를 제공합니다.
• 최적화: 기존 트랜스포머 프로그램을 최소화하고 제약 하에 학습할 수 있는 능력은 프로그램 정제 및 안전-중요 응용 분야를 위한 C-RASP 의 유용성을 보여줍니다.

저자들은 그들의 작업이 트랜스포머의 공식 분석을 위한 기초를 마련했으며, 향후 방향으로는 견고성 검증과 사고의 연쇄 (CoT) 메커니즘의 통합이 포함될 것이라고 결론지었습니다.