컴팩트 증명으로 채점하는 기계적 해석 가능성: 제이슨 그로스가 말하는 증명 길이와 한계

핵심 메시지

• 기계적 해석 가능성을 '모델 설명의 압축'으로 보고, 증명의 길이로 압축률을, 한계값의 정확도로 충실도를 측정하자는 제안이다.
• 모든 입력을 직접 돌려보는 것이 기준선이며, 이해가 더해질수록 그보다 짧은 증명으로 더 나은 한계값을 얻을 수 있어야 한다는 가설을 검증한다.
• 가장 어려운 부분은 구조가 없는 잡음과 비선형성이며, 증명이 막히는 지점은 대개 연구자가 이해하지 못한 지점과 일치했다.
• 이 기준으로 보면 현재의 해석 가능성 연구 대부분은 데이터와 모델의 극히 일부만 다뤄 압축 이득이 거의 없다는 것이 그의 냉정한 평가다.
• 모델 자체보다 모델이 만들어 낸 코드에 대한 증명이 훨씬 현실적인 목표이며, 그는 이를 자동화하는 창업을 준비 중이라고 밝혔다.

쉽게 이해하기

AI 정렬 연구자 인터뷰 팟캐스트 AXRP 40화에 제이슨 그로스가 출연했다. 그는 박사 과정에서 HTTPS 암호화에 쓰이는 코드의 검증에 참여했고 증명 보조기 개발에도 관여한 연구자로, 이번 대화의 주제는 신경망 해석 연구를 증명으로 채점하는 '컴팩트 증명' 계열의 논문들이다. 그는 기계적 해석 가능성을 대형 모델에 대한 설명을 압축하는 작업으로 보고, 그 압축이 얼마나 잘 됐는지를 증명의 길이로 잰다고 요약했다.

구조는 단순하다. 어떤 모델이 특정 데이터 분포에서 얼마나 잘 작동하는지에 대한 한계값을 증명하되, 증명이 짧을수록 압축이 잘 된 것이고 한계값이 실제 성능에 가까울수록 충실한 설명이다. 아무 이해 없이 할 수 있는 기준선은 모든 데이터를 모델에 한 번씩 넣어 보는 것이다. 실험 대상은 층 하나에 어텐션 헤드 하나뿐인 아주 단순한 트랜스포머로, 입력된 수 가운데 최댓값을 고르는 과제를 학습했다. 네 개짜리 문제는 전수 확인에 1~2분이면 되지만 스무 개로 늘리면 대형 모델 학습에 맞먹는 비용이 들고, 토큰이 하나 늘 때마다 어휘 크기만큼 곱해지는 지수적 폭발이 일어난다.

여기서 흥미로운 결과가 나온다. '이 신경망은 단 하나의 토큰에 주목해서 정답을 낸다'는 아주 얕은 이해만 넣어도 지수적 비용이 어휘 크기의 세제곱 수준으로 내려간다. 반대로 끝까지 남는 난제는 이른바 구조가 없는 잡음이다. 어텐션의 쿼리·키 회로는 근사적으로 낮은 계수의 행렬로 설명되지만, 그 부분을 걷어내고 남는 나머지는 거의 무작위처럼 보이고, 그 값들이 계속 작게 유지된다는 사실을 모든 경우를 다 따져 보지 않고 증명하기가 어렵다는 것이다. 그는 이런 문제를 다루려면 무작위성을 제거하는 기법이 필요하다고 봤다.

현재 진행 중인 프로젝트는 여러 층의 잔차 스트림을 이어 붙여 학습한 희소 오토인코더, 이른바 크로스코더를 증명으로 바꾸는 작업이다. 크로스코더가 모델을 완벽히 대신한다고 가정하고 출력을 계산한 뒤, 실제와의 오차를 전파하고, 특징들이 선형적으로만 상호작용한다는 암묵적 가정을 검증하는 순서다. 마지막 단계에서 특징 쌍 사이의 상호작용을 재는 지표가 나오는데, 그는 이 지표가 곧 '어디에 해석 노력을 더 쏟아야 하는지'를 알려 준다고 설명했다. 여기서 압축하는 대상이 신경망 자체가 아니라 신경망을 데이터에 돌린 계산 과정이라는 점도 강조했다.

이 기준으로 매긴 현재 연구의 성적은 박하다. 그는 데이터셋의 극히 일부, 모델의 극히 일부만 골라 흥미로운 동작을 설명하는 연구는 그 부분을 그냥 돌려 보는 비용과 별 차이가 없어 압축 이득이 없다고 지적했다. 층별로 학습하는 희소 오토인코더도 층 사이의 연결이 없으면 계산을 줄여 주지 못한다. 다만 이는 목표가 다르기 때문이기도 하다며, 구조를 발견한다는 목적에서는 잘 진행되고 있다고 덧붙였다. 후반부에서는 배포 중인 대형 모델을 그대로 증명하기보다 증명 가능하도록 모델을 바꾸는 편이 현실적이라는 견해, 그리고 모델 자체보다 모델이 만든 코드를 증명하는 편이 훨씬 합리적이라는 판단을 밝혔다. 그는 이 형식 검증 자동화를 목표로 공동 창업을 준비 중이라고 전했다.

주요 인사이트

• 증명이 막히는 자리를 들여다보면 대개 자신이 이해했다고 착각한 지점이었다는 회고는, 증명 길이가 단순한 점수가 아니라 연구 방향을 가리키는 나침반으로 쓰인다는 뜻이다.
• '없는 행동'을 설명해야 한다는 비유가 인상적이다. 사람이 자라는 과정을 설명하려면 성장 기전만이 아니라 몸 안에 치명적인 독처럼 작용하는 것이 없다는 사실까지 보여야 하는데, 지금의 해석 연구는 이 몫을 거의 다루지 않는다는 것이다.
• 증명이라는 형식은 약한 명제라도 강한 함의를 가진다. 웹 브라우저가 인쇄 버튼을 누르지 않으면 절대 문서를 인쇄하지 않는다는 사실만 제대로 증명해도, 임의 코드가 원격에서 실행될 수 없다는 사실까지 함께 배제된다는 예가 제시됐다.
• 일부 전문가만 활성화되는 혼합 전문가 구조는 데이터 하나마다 모델의 일부만 쓰기 때문에, 같은 파라미터 수의 조밀한 모델보다 증명 관점에서 유리할 수 있다는 관찰이 나왔다.
• 형식 검증 자동화의 병목으로 증명 보조기용 학습 데이터 부족, '거의 맞은 증명은 틀린 증명'이라는 특성, 원본 코드의 10~100배에 이르는 검증 코드 분량, 그리고 40년 된 증명 보조기에 성능 담당 엔지니어가 사실상 없다시피 했다는 점이 지목됐다.

자주 묻는 질문

관련 AI 소식