본 논문은 훈련된 트랜스포머 모델 $\mathcal{M}$이 주어진 토큰 문자열 $s$에 의해 "압도"(overwhelmed)되는 것을 증명하는 알고리즘을 개발합니다. 모델이 문자열 $s$와 추가 문자열 $t$에 대해 평가될 때 ($\mathcal{M}(s + t)$), $t$의 길이가 $n_{free}$ 이하일 경우 $t$의 값에 완전히 무감각해지는 경우를 $\mathcal{M}$이 $s$에 의해 "압도"되었다고 정의합니다. 알고리즘은 시간 및 공간 복잡도 $\widetilde{O}(n_{fix}^2 + n_{free}^3)$ 내에서 작동하며, "과도한 압축"(over-squashing)에 대한 강력한 최악의 경우 형태를 증명하는 데 컴퓨터 지원 증명을 사용합니다. 단일 레이어 트랜스포머(어텐션 헤드, 레이어 정규화, MLP/ReLU 레이어, RoPE 위치 인코딩 포함)에 대한 실험적 테스트 결과도 제시합니다. 이 연구는 훈련된 트랜스포머 모델에 대한 유용한 보장을 얻는 어려운 과제를 위한 발걸음이라고 주장합니다.
