0. Summary

기본 정보 : ArXiv,2026.10.18, Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention
연구 배경 : Multi-head attention은 Transformer의 핵심 부품이지만, 표현력(expressivity)이 head 수에 어떻게 의존하는지는 아직 제대로 이해되지 않았다. 이론적 mechanistic interpretability 연구(Elhage et al. 2021 등)는 경험적 해석 연구에 유용한 추상화를 제공해 왔지만, 그런 이론을 세우려면 전문가가 수학을 오랫동안 붙잡고 있어야 한다. 이 논문의 문제의식은 Nanda et al. (2023)의 modular addition 1-layer transformer에서 나온 경험적 관찰에서 출발한다. 그 모델에서 parity는 개별 head 출력으로부터는 거의 선형 디코딩되지 않았지만 head 출력을 합치면 거의 완벽하게 디코딩되었다. 이는 parity가 여러 head에 분산된 계산으로 구현된다는 것을 시사하며, 저자들은 “단일 head attention에 구조적 표현력 장벽이 있는가?”를 묻게 되었다. 동시에 최근 LLM의 수학적 추론·형식 정리 증명 능력이 급격히 발전하면서, frontier 모델에게 이런 이론을 세우게 하고 형식 검증으로 그 결과를 보증할 수 있는지가 또 하나의 질문이 되었다.
제안 방법 : 입력 $n$비트와 전용 query 토큰 $q$로 이루어진 시퀀스를 받는 1-layer, attention-only transformer(additive positional embedding, MLP·LayerNorm 없음, query 위치에서 선형 threshold readout)를 고정하고, Boolean 함수 $f$를 정확히 표현하는 데 필요한 최소 head 수를 head complexity $H^{\ast}(f)$ 로 정의한다. 연구 자체는 GPT-5.6 Sol 에이전트 하나가 Codex Desktop 샌드박스 안에서 /goal 프롬프트 한 번을 받고 약 9.5시간 동안 사람의 추가 개입 없이 수행했다. 에이전트는 각 head의 readout 기여가 Boolean cube 위에서 정확히 하나의 linear-fractional atom(아핀/아핀 비율)이 된다는 정규형(Theorem 1)을 유도하고, 이로부터 threshold degree 하한(Theorem 2)과 대칭 함수에 대한 정확한 특성화(Theorem 5)를 증명한 뒤, 별도 세션의 counterexample 탐색으로 하한이 strict한 10비트 함수(Theorem 3)를 찾았다. 모든 결과는 Lean 4 + Mathlib으로 기계 검증되었고, 사람은 고수준 질문을 정의하고 Lean 명제가 자연어 주장과 일치하는지 검토하는 역할을 맡았다.
발견 사실 : $H^{\ast}(f)$는 $f$를 sign-represent하는 linear-fractional atom의 최소 개수 $L_{\mathrm{frac}}(f)$와 정확히 같다(Theorem 1). 따라서 $H^{\ast}(f)\le 1$인 함수는 정확히 linear threshold function이며, parity가 단일 head에서 선형 디코딩되지 않았던 것은 구조적 필연이다(Corollary 1). 모든 Boolean 함수에 대해 threshold degree $\deg_{\pm}(f)\le H^{\ast}(f)$ 가 성립하지만(Theorem 2), 10비트 함수 $f_{10}$에서 $\deg_{\pm}(f_{10})=2<3\le H^{\ast}(f_{10})$이므로 이 하한은 항상 tight하지 않다(Theorem 3). 대칭 Boolean 함수에 대해서는 positional embedding을 허용하더라도 $H^{\ast}(f)=\deg_{\pm}(f)=C(F)$, 즉 Hamming weight 프로파일 $F$가 값을 바꾸는 횟수와 정확히 같고(Theorem 5), 특히 $n$비트 parity는 정확히 $n$개 head가 필요하다(Corollary 2). 이는 positional embedding이 없는 모델에서 동시 연구된 Hsu and Xu (2026)의 결과와 일치한다. 모든 Boolean 함수는 $2^n-1$개 head로 표현 가능하다(Theorem 4).
핵심 기여 :
1. head complexity의 정확한 수학적 특성화 : linear-fractional normal form(Theorem 1), 일반 threshold-degree 하한(Theorem 2), 하한이 strict한 명시적 10비트 separation(Theorem 3), weighted-sum interpolation 상한(Theorem 4), 대칭 함수의 정확한 특성화 $H^{\ast}(f)=C(F)$(Theorem 5)를 제시했다. positional embedding을 허용한 설정이라 Hsu and Xu의 대칭 결과를 넘어 비대칭 함수까지 다룰 수 있다.
2. 형식 검증으로 뒷받침된 autoresearch 사례 연구 : 정리들을 frontier 모델이 conjecture 생성 → 증명 → Lean 4 형식화의 흐름으로 발견했고, 사람은 질문을 던지고 결과를 검토했다. 에이전트의 run 기록(949회 tool call, 약 142.4M input token, 13개 approach family 등)과 사람 개입 지점을 투명하게 메타 분석했다.
3. 재사용 가능한 공개 아티팩트 : Lean 4 형식화, 자연어 정리·증명, 익명화된 research trace를 공개 저장소로 제공하여, mechanistic interpretability에서 agent-assisted theorem proving과 형식 검증의 출발점을 만들었다.

Abstract 쉬운 설명(Gemini)

🏗️ 1. 트랜스포머와 ‘어텐션 헤드’란 무엇일까?

챗GPT 같은 인공지능의 두뇌를 ‘트랜스포머(Transformer)’라고 부릅니다. 이 두뇌 안에는 글을 읽고 문맥을 파악하는 아주 중요한 일꾼들이 들어있는데, 이 일꾼들의 이름을 ‘어텐션 헤드(Attention Head)’라고 합니다.

쉽게 말해, 글을 읽을 때 어떤 헤드는 ‘주어’에 집중하고, 어떤 헤드는 ‘동사’에 집중하며, 어떤 헤드는 ‘대명사(그, 그녀 등)’가 누구를 가리키는지 집중해서 분석합니다.
하지만 지금까지 연구자들은 “이 일꾼(헤드)들이 몇 명이나 있어야 인공지능이 복잡한 문제를 완벽하게 풀 수 있을까?”에 대한 명확한 수학적 답을 내리지 못하고 있었습니다.

🧩 2. 이 논문이 밝혀낸 수학적 비밀

연구진은 이 문제를 풀기 위해 “특정 논리 퀴즈를 풀려면 최소 몇 명의 일꾼(헤드)이 필요할까?”를 수학적으로 계산하는 공식을 만들어냈습니다.

최소 필요 인원 공식 개발: 어떤 복잡한 퀴즈를 풀기 위해 필요한 ‘최소한의 일꾼 수’를 정확하게 구하는 수학 공식을 찾아냈습니다.
일꾼들의 한계 증명: 아무리 일꾼들에게 힌트(위치 정보)를 많이 주더라도, 퀴즈의 난이도가 일정 수준 이상으로 올라가면 일꾼의 수를 무조건 늘려야만 문제를 풀 수 있다는 사실을 수학적으로 증명해 보였습니다.

🤖 3. 가장 놀라운 점: “AI가 스스로 연구하고 증명했다!”

사실 이 논문에서 가장 흥미롭고 혁신적인 부분은 연구를 진행한 ‘방식’에 있습니다.

기존에는 대학의 교수님들과 천재 수학자들이 칠판에 수식을 적어가며 몇 달 동안 머리를 싸매고 증명했을 법한 수학 공식들을, 이번에는 AI 에이전트(인공지능 연구원)가 스스로 알아냈습니다.

인간의 역할: “이 문제에 대해 한번 탐구해봐”라고 가이드를 줌 🗺️
AI의 역할: 스스로 가설을 세우고 ➡️ 수학적으로 증명한 뒤 ➡️ 이 증명이 정말 컴퓨터 과학적으로 한 치의 오차도 없는지 검증하는 프로그램 코드(Lean 4)까지 완벽하게 짜서 제출함 💻

즉, “AI가 자기 자신의 뇌 구조(트랜스포머)가 작동하는 원리를 스스로 탐구하고, 그 비밀을 인간보다 더 정밀하게 수학적으로 증명해낸 사건”이라고 볼 수 있습니다.

📌 한 줄 요약

“인공지능(AI)이 자기 자신의 뇌 속 일꾼들이 몇 명이나 필요한지 분석하는 수학 공식을 스스로 연구하고 완벽하게 증명해낸 연구”입니다.

이 논문은 어떻게 AI를 수학적으로 활용하였는가?

이 논문은 AI를 단순한 코딩 보조나 텍스트 요약 도구로 쓴 것이 아닙니다. 가설 수립부터 수학적 증명, 그리고 기계 검증을 위한 코드 작성까지의 전 과정을 AI가 주도하도록 설계된 ‘자동화 연구(Autoresearch)’ 파이프라인을 구축해 활용했습니다.

🤖 AI 에이전트 기반 자동화 연구(Autoresearch) 프로세스

연구진은 AI 에이전트가 샌드박스 환경(Codex sandbox) 내에서 도구들을 자유롭게 다루며 자율적으로 수학적 탐구를 수행할 수 있도록 시스템을 디자인했습니다. 구체적인 작동 프로세스는 다음과 같은 5단계로 이루어집니다.

[인간 연구자] ➡️ /goal 프롬프트 던지기 (상위 문제 정의)
      ⬇️
[GPT-5.6 Sol] ➡️ 1단계: 가설(Conjecture) 생성 & 브레인스토밍
      ⬇️
[GPT-5.6 Sol] ➡️ 2단계: 자연어(수학 논문 스타일) 증명 작성 (약 9.5시간 소요)
      ⬇️
[GPT-5.6 Sol] ➡️ 3단계: Lean 4 형식 기계 정형 검증 코드 자동 작성
      ⬇️
[인간 연구자] ➡️ 4단계: Lean 컴파일러 검증 결과 최종 검토 및 리팩토링

1️⃣ 1단계: 상위 목표 제시 (/goal Prompt)

인간 연구자는 연구의 세부적인 수학적 단계를 지시하지 않았습니다. 대신 AI 에이전트에게 “멀티헤드 어텐션(MHA) 레이어가 Boolean 함수를 표현할 때 필요한 헤드 수의 하한선과 물리적 한계를 탐구하라”는 상위 수준의 목표(/goal) 프롬프트만을 제공했습니다.

2️⃣ 2단계: 자율적 가설 설정 및 자연어 증명 (약 9.5시간 수행)

에이전트인 GPT-5.6 Sol은 인간 연구자가 던진 질문을 바탕으로 스스로 생각하기 시작했습니다.

브레인스토밍 및 가설 수립: ‘어텐션 헤드 수’와 ‘표현 능력’ 간의 상관관계를 설명할 수 있는 수학적 가설(Conjecture)들을 스스로 정의했습니다.
자연어 증명 작성: 논문 작성용 라텍(LaTeX) 수학식 스타일의 자연어 논증 및 수학적 증명 과정을 스스로 적어 내려갔습니다. 이 과정은 샌드박스 환경 내에서 약 9.5시간 동안 자율적으로 반복 수행되었습니다.

3️⃣ 3단계: 공식 정형 검증 (Lean 4 Formalization)

AI가 수식이나 논리에 치명적인 오류를 범하는 ‘환각(Hallucination)’ 현상을 막기 위해, 연구진은 정형 수학 검증 도구인 Lean 4와 대학 수준 이상의 공인된 수학 라이브러리인 Mathlib 환경을 제공했습니다.

에이전트는 앞서 작성한 자연어 증명을 컴퓨터가 논리적으로 한 치의 오차도 없이 검증할 수 있는 Lean 4 코드로 자동 변환(Formalization)했습니다.
Lean 4 컴파일러가 “수학적 논리에 오류가 있음”을 피드백하면, 에이전트는 스스로 코드를 디버깅하고 증명을 수정하여 기계 검증을 완벽히 통과할 때까지 증명을 다듬었습니다.

4️⃣ 4단계: 반례 검색 (Counterexample Search)

AI가 제시한 복잡한 수학 공식들 중 일부 일반화된 수학 법칙이 완벽한지 확인하기 위해 별도의 시스템을 가동했습니다.

AI 에이전트는 일반 이론을 정형화하는 동안, 한편으로는 이론을 깨뜨릴 수 있는 구체적인 반례가 존재하는지 찾는 독립적인 반례 탐색 프로세스(Counterexample Search)를 가동했습니다.
이 과정을 통해 일반적인 이론의 한계를 정확히 짚어주는 “10비트짜리 특수 함수(반례)”를 직접 찾아내 정리의 타당성을 입증해 냈습니다.

5️⃣ 5단계: 인간 연구자의 검토 및 최종 리팩토링 (Human-in-the-loop)

AI가 완벽하게 수학적 검증을 통과한 코드를 작성해 주면, 인간 연구자는 최종 단계에서 감독관 역할을 수행했습니다.

의도 확인: AI가 논리적 구멍을 피하기 위해 다르게 해석한 수학적 명제가 없는지, 원래 사람이 의도한 질문과 논리적으로 일치하는지 최종 확인했습니다.
코드 리팩토링: AI가 도출한 Lean 4 코드가 학술적으로 읽기 편하고 다른 연구자들이 재사용하기 좋도록 가독성을 높이고 문서를 다듬는(Refactoring) 작업을 진행했습니다.

🌟 이 AI 기반 방법론의 가치

이 연구는 AI가 이제 단순히 ‘글을 대신 써주는 비서’를 넘어, 수학적 가설을 홀로 발견(Discovery)하고 컴퓨터 코드를 통해 완벽하게 검증(Verification)까지 할 수 있는 자율 연구자로 활약할 수 있다는 점을 실증한 중요한 사례입니다.

이를 통해 인간 연구자는 노가다성 수학 수식 전개나 자잘한 논리 오류 검증에 시간을 뺏기지 않고, 더 고차원적인 방향성 설정에만 집중할 수 있게 되었습니다.

관련 개념

Transformer 표현력(Expressivity)과 head complexity

표현력(expressivity)은 “이 아키텍처가 어떤 함수를 정확히 계산할 수 있는가”를 묻는 질문입니다. 학습 동역학(어떤 해를 실제로 찾는가)과는 분리된, 순수하게 구조적인 질문입니다. 이 논문은 표현력을 head 수라는 아키텍처 자원의 함수로 보고, Boolean 함수 $f:{0,1}^n\to{0,1}$를 대상으로 “최소 몇 개의 attention head가 필요한가”를 묻습니다.

📚 1. 기존 접근들

접근	대표 연구	핵심 질문
논리적 특성화	Weiss et al. (2021), Yang and Chiang (2024)	Transformer가 어떤 논리·프로그래밍 언어와 동등한가
근사 이론	Kajitsuka and Sato (2024), Yu et al. (2026)	$\epsilon$-근사에 필요한 파라미터 복잡도, head 수에 따른 상·하한
형식 언어 / Boolean 함수	Hahn (2020), Hsu (2026), Kozachinskiy et al. (2026)	parity 같은 특정 함수를 1-layer로 계산하는 데 필요한 자원의 하한
동시 연구 (head complexity)	Hsu and Xu (2026), Rajaraman et al. (2026)	대칭 함수의 정확한 head 수, parity는 정확히 $n$ head 필요

이런 진전에도 불구하고, 1-layer라도 여러 head의 업데이트와 그 상호작용을 동시에 추적해야 하기 때문에 일반적인 보장을 유도하는 것은 기술적으로 까다롭습니다. 논문은 바로 이 지점에 agent-assisted 수학 추론과 형식 검증을 투입합니다.

🎯 2. 이 논문의 질문

Boolean 함수 $f$에 대해, 단일 attention layer에서 $f$를 표현하는 데 필요한 최소 attention head 수는 얼마인가?

문제의 동기가 된 2비트 예시가 직관을 줍니다. AND와 OR은 head 하나로 선형 실현이 되지만 XOR은 head 하나로는 안 되고 두 개면 됩니다. 그래서 head 수가 Boolean 함수의 의미 있는 복잡도 척도가 될 수 있다는 가설이 나옵니다.

💡 Key Takeaway 이 논문의 표현력은 “근사”가 아니라 “정확한 표현“이며, 자원은 width나 depth가 아니라 head 수입니다. 학습이 아니라 아키텍처가 무엇을 강제하는지를 묻는 설정입니다.

모델 설정: 1-layer attention-only transformer

논문의 모든 정리는 다음의 의도적으로 단순화된 모델 위에서 성립합니다. 결과의 범위를 정확히 이해하려면 이 설정을 알아야 합니다.

🧱 1. 구조

구성 요소	정의
입력	$n$비트 $\mathbf{x}\in{0,1}^n$ 뒤에 전용 query 토큰 $q$를 붙인 시퀀스 $(x_1,\dots,x_n,q)$. 위치 집합 $\mathcal{I}=[n]\cup{q}$
임베딩	토큰 임베딩 + positional 임베딩: $\mathbf{u}j(\mathbf{x})=\mathbf{e}{x_j}+\mathbf{p}_j$ ($j\in[n]$), $\mathbf{u}_q=\mathbf{e}_q+\mathbf{p}_q$ (입력과 무관)
head	$H$개 head가 같은 임베딩 시퀀스를 공유. 각 head는 $W_Q^{(h)},W_K^{(h)},W_V^{(h)}\in\mathbb{R}^{d_{head}\times d_{model}}$, $W_O^{(h)}\in\mathbb{R}^{d_{model}\times d_{head}}$
readout	query 위치의 residual $\mathbf{h}_q(\mathbf{x})$에 선형 threshold $(\mathbf{w},\tau)$ 적용
없는 것	MLP, LayerNorm, dropout, 추가 layer. 비선형성은 softmax와 마지막 threshold뿐

query 위치의 최종 출력은 다음과 같습니다.

$$\mathbf{h}q(\mathbf{x})=\mathbf{u}_q+\sum{h=1}^{H}W_O^{(h)}\frac{\sum_{j\in\mathcal{I}}\exp\big(\langle W_K^{(h)}\mathbf{u}j(\mathbf{x}),W_Q^{(h)}\mathbf{u}_q\rangle\big)W_V^{(h)}\mathbf{u}_j(\mathbf{x})}{\sum{j\in\mathcal{I}}\exp\big(\langle W_K^{(h)}\mathbf{u}_j(\mathbf{x}),W_Q^{(h)}\mathbf{u}_q\rangle\big)}$$

📐 2. 정확한 표현과 head complexity

$f$가 $H$개 head로 정확히 표현된다(exactly representable)는 것은 모델 파라미터와 readout $(\mathbf{w},\tau)$가 존재하여

$$\forall\mathbf{x}\in{0,1}^n,\quad \big[f(\mathbf{x})=1\iff\langle\mathbf{w},\mathbf{h}_q(\mathbf{x})\rangle>\tau\big]$$

가 성립하는 것입니다. 즉 라벨 0과 1의 입력이 readout 위치에서 선형 분리 가능해야 합니다. 그리고

$$H^{\ast}(f)=\min{H: f\text{ is exactly representable by an }H\text{-head model}}$$

입니다. $d_{model}$과 $d_{head}$는 제한이 없습니다(unrestricted width).

🧭 3. 설정에 관한 관례

$1/\sqrt{d_{head}}$ 스케일링은 $W_Q$나 $W_K$에 흡수되므로 생략합니다.
$\mathbf{u}_q$는 입력에 독립이므로 readout threshold에 흡수할 수 있습니다.
query 토큰이 마지막에 있으므로 full attention과 causal mask는 동일한 위치 집합을 봅니다.
positional embedding을 허용한 것이 Hsu and Xu (2026)와의 결정적 차이입니다. 순열 불변성을 깨뜨려 표현 가능한 함수 클래스를 넓히고, 비대칭 Boolean 함수를 다룰 수 있게 합니다.

💡 Key Takeaway 이 모델은 “attention head가 혼자서 무엇을 할 수 있는가”를 가장 깨끗하게 분리한 설정입니다. MLP가 없으므로 head 수가 곧 비선형 자원의 전부입니다.

Linear-fractional normal form (Theorem 1)

논문의 기술적 핵심은 각 head의 readout 기여가 Boolean cube 위에서 정확히 하나의 “아핀/아핀” 비율이 된다는 관찰입니다. 이 덕분에 임베딩과 가중치 행렬을 추적하지 않고도 $H^{\ast}(f)$를 다룰 수 있습니다.

🧮 1. Linear-fractional atom (Definition 1)

함수 $\phi:{0,1}^n\to\mathbb{R}$이 다음 형태의 표현을 가지면 linear-fractional atom이라 부릅니다.

$$\phi(\mathbf{x})=\frac{\mathbf{A}^\top\mathbf{x}+b}{\mathbf{C}^\top\mathbf{x}+d}$$

단, 계수 $(\mathbf{A},b,\mathbf{C},d)$는 다음 세 조건을 모두 만족해야 하며 이를 admissible하다고 합니다.

조건	내용	의미
(i)	모든 $\mathbf{x}\in{0,1}^n$에서 $\mathbf{C}^\top\mathbf{x}+d>0$	분모 = 총 attention weight 이므로 항상 양수
(ii)	$\mathbf{C}$의 성분이 모두 양수, 모두 음수, 또는 모두 0	비트가 1로 바뀔 때 attention weight 배율 $\alpha$가 모든 위치에서 같음
(iii)	$\mathbf{C}=\mathbf{0}$이면 $\mathbf{A}$의 성분도 모두 양수/모두 음수/모두 0	$\alpha=1$이면 numerator 기울기는 $\rho_i\beta$ 형태라 부호가 같음

Linear-fractional complexity $L_{\mathrm{frac}}(f)$ 는 상수 $c$와 atom $\phi_1,\dots,\phi_H$가 존재하여 $c+\sum_h\phi_h(\mathbf{x})>0\iff f(\mathbf{x})=1$이 되는 최소 $H$입니다.

🔍 2. 왜 head 하나가 atom 하나인가

head 하나를 고정하고 $\Delta\mathbf{e}=\mathbf{e}_1-\mathbf{e}_0$라 두면, 위치 $i$의 입력 벡터는 $\mathbf{u}_i(\mathbf{x})=\mathbf{e}_0+\mathbf{p}_i+x_i\Delta\mathbf{e}$ 로 $x_i$에 대해 아핀입니다. logit과 scalar value도 선형 맵의 합성이므로

$$\ell_i(\mathbf{x})=\kappa_i+a\,x_i,\qquad s_i(\mathbf{x})=m_i+\beta\,x_i$$

가 됩니다. 핵심은 $a$와 $\beta$가 위치에 무관하다는 점입니다. 어느 비트를 켜든 같은 벡터 $\Delta\mathbf{e}$가 더해지기 때문입니다. 이제 Boolean 입력의 두 가지 항등식

$$\alpha^{x_i}=1+(\alpha-1)x_i,\qquad x_i^2=x_i$$

을 쓰면 numerator(가중 value 합)와 denominator(unnormalized attention weight 합)가 모두 아핀이 됩니다.

$$N(\mathbf{x})=\exp(\ell_q)s_q+\sum_{i=1}^n\rho_i\alpha^{x_i}(m_i+\beta x_i)=\mathbf{A}^\top\mathbf{x}+b,\qquad D(\mathbf{x})=\exp(\ell_q)+\sum_{i=1}^n\rho_i\alpha^{x_i}=\mathbf{C}^\top\mathbf{x}+d$$

여기서 $\rho_i=\exp(\kappa_i)>0$, $\alpha=\exp(a)>0$ 입니다. 따라서 head의 scalar 기여는 $\phi=N/D$, 즉 atom입니다. 계수 공식은 명시적으로

$$A_i=\rho_i\big((\alpha-1)m_i+\alpha\beta\big),\quad b=\eta+\sum_i\rho_i m_i,\quad C_i=\rho_i(\alpha-1),\quad d=\gamma+\sum_i\rho_i$$

이고, 역으로 모든 admissible 튜플은 어떤 파라미터로부터 나온다는 것을 Appendix E.1이 양방향으로 증명합니다.

🏗️ 3. Theorem 1 (정규형)

$H$-head 모델의 scalar score $S(\mathbf{x})=\langle\mathbf{w},\mathbf{h}_q(\mathbf{x})\rangle-\tau$는 다음 형태와 동치입니다.

$$S(\mathbf{x})=c+\sum_{h=1}^{H}\frac{\mathbf{A}_h^\top\mathbf{x}+b_h}{\mathbf{C}_h^\top\mathbf{x}+d_h}$$

각 튜플은 admissible하고, 임의의 $H$개 atom은 공유 임베딩을 쓰는 $H$개 head로 동시에 실현됩니다(width가 무제한이므로 head마다 직교 좌표 블록을 할당). 결과적으로

$$H^{\ast}(f)=L_{\mathrm{frac}}(f).$$

atoms → heads 방향의 구성은 $d_{model}\ge 4H$를 잡고 head마다 정규직교 벡터 $\mathbf{q}^{(h)},\mathbf{k}^{(h)},\mathbf{v}^{(h)},\mathbf{o}^{(h)}$를 할당한 뒤, 토큰·positional 임베딩을 $\log\alpha^{(h)},\log\rho_i^{(h)},m_i^{(h)}$ 등의 합으로 명시적으로 짓는 방식입니다.

💡 Key Takeaway softmax attention은 Boolean 입력 위에서 “아핀 나누기 아핀”으로 완전히 붕괴합니다. 그래서 head 수 문제는 “Boolean 함수를 몇 개의 admissible 유리 함수의 합으로 sign-represent 할 수 있는가”라는 순수 대수 문제가 됩니다.

단일 head의 한계와 threshold degree 하한

정규형이 생기면 하한을 얻는 길이 바로 열립니다. 분모를 모두 곱해 다항식으로 바꾸면, 고전적인 Boolean 함수 복잡도 척도인 threshold degree와 연결됩니다.

1️⃣ 1. Corollary 1 (One head)

$H^{\ast}(f)=0\iff f$가 상수 함수
$H^{\ast}(f)\le 1\iff f$가 linear threshold function: $f(\mathbf{x})=1\iff\theta_0+\sum_i\theta_i x_i>0$

증명 방향 (⇒): atom 하나 $\phi=N/D$에 대해 $c+\phi=(cD+N)/D$이고 $D>0$이므로 부호는 아핀 함수 $cD+N$과 같습니다. (⇐): $\phi(\mathbf{x})=\dfrac{\theta_0+\sum_i\theta_ix_i}{1+\sum_i x_i}$ 는 분모 기울기가 모두 1이라 admissible한 atom입니다.

parity는 linear threshold function이 아니므로, 서론의 modular-addition 모델에서 parity가 단일 head에서 선형 디코딩되지 않았던 현상에 구조적 설명이 생깁니다.

📉 2. Theorem 2 (Threshold-degree lower bound)

실수 다항식 $P$가 $f$를 sign-represent한다는 것은 모든 $\mathbf{x}$에서 $P(\mathbf{x})>0\iff f(\mathbf{x})=1$인 것이며, 그런 다항식의 최소 차수가 $\deg_\pm(f)$ 입니다(Minsky and Papert, 1969). 모든 Boolean 함수에 대해

$$\deg_\pm(f)\le H^{\ast}(f).$$

증명은 한 줄입니다. $H$-head score $S=c+\sum_h N_h/D_h$에 양의 공통분모 $\prod_h D_h$를 곱하면 부호 패턴이 보존되고,

$$P(\mathbf{x})=c\prod_{h=1}^{H}D_h(\mathbf{x})+\sum_{h=1}^{H}N_h(\mathbf{x})\prod_{g\ne h}D_g(\mathbf{x})$$

의 각 항은 차수가 최대 $H$이므로 $P$는 차수 $\le H$인 sign representation입니다.

척도	정의	관계
$\deg_\pm(f)$	sign-representing 다항식의 최소 차수	하한
$H^{\ast}(f)$	정확 표현에 필요한 최소 head 수	$\ge\deg_\pm(f)$
$L_{\mathrm{frac}}(f)$	admissible atom의 최소 개수	$=H^{\ast}(f)$

💡 Key Takeaway “head 하나 = 차수 하나”입니다. head를 하나 더 붙일 때마다 sign-representing 다항식의 차수가 최대 1 늘어날 수 있을 뿐이므로, 차수가 높은 함수는 head를 많이 요구합니다.

하한의 strictness: 10비트 separation (Theorem 3)

Theorem 2의 하한이 항상 tight한 것은 아닙니다. 저자들은 threshold degree와 head complexity가 갈라지는 명시적 함수를 찾았고, 이 부분은 autoresearch가 특히 유용했던 대목이라고 밝힙니다.

🔢 1. 함수 $f_{10}$

10비트 입력 $\mathbf{x}=(\mathbf{a},\mathbf{b})$, $\mathbf{a},\mathbf{b}\in{0,1}^5$에 대해

$$Q(\mathbf{a},\mathbf{b})=\Big(\sum_{i=1}^5(1-2a_i)\Big)\Big(\sum_{j=1}^5(1-2b_j)\Big)-3\sum_{i=1}^5(1-2a_i)(1-2b_i),\qquad f_{10}(\mathbf{x})=1\iff Q(\mathbf{a},\mathbf{b})>0$$

Theorem 3. $\deg_\pm(f_{10})=2<3\le H^{\ast}(f_{10})$.

🧩 2. 증명 스케치

sign 좌표 $s_i=1-2a_i$, $t_i=1-2b_i\in{-1,+1}$로 바꾸면 $\widetilde Q(\mathbf{s},\mathbf{t})=(\sum_i s_i)(\sum_j t_j)-3\sum_i s_it_i$ 입니다.

단계	내용
$\deg_\pm=2$	$\widetilde Q\equiv 2\pmod 4$ 라 절대 0이 되지 않으므로 $Q$ 자체가 strict한 2차 sign representation. 한편 특정 2차원 face에서 $\widetilde Q=-2rw$ (XOR 패턴)이므로 아핀으로는 불가능 → 정확히 2
2 head 불가	2 head라면 $P=(cD_1+N_1)D_2+N_2D_1$ 즉 아핀 곱 두 개의 합 $L_1R_1+L_2R_2$ 형태. mixed antipodal difference $\Delta g(\mathbf{s},\mathbf{t})=g(\mathbf{s},\mathbf{t})-g(\mathbf{s},-\mathbf{t})-g(-\mathbf{s},\mathbf{t})+g(-\mathbf{s},-\mathbf{t})$를 취하면 $\Delta P^\pm=\mathbf{s}^\top K\mathbf{t}$ 에서 $\operatorname{rank}(K)\le 4$
모순	$\widetilde Q(\mathbf{s},\mathbf{z}^{(j)})=6s_j$ 라는 slice의 부호 조건이 행렬 $M=KZ$를 strictly column diagonally dominant하게 만들어 rank 5 → $\operatorname{rank}\le4$와 모순

🤖 3. 발견 과정

이 separation은 정리 생성 run에서는 나오지 않았습니다. 저자들이 “$\deg_\pm(f)\ne H^{\ast}(f)$인 명시적 예를 찾아라”는 한 줄 목표로 별도 세션(GPT-5.6 Sol, ultra reasoning effort)을 열었고, 첫 턴(32회 tool call, 7분 이내)에 128비트 예시가 나왔습니다. 이후 사람이 “설명해 달라”, “더 작고 Lean 친화적인 증명이 있는 예를 찾아 달라”고 요청하는 턴을 거쳐 10비트 예시로 줄었습니다.

💡 Key Takeaway threshold degree는 head complexity를 특성화하지는 못합니다. 두 head의 합은 “rank 4 이하”라는 대수적 지문을 남기고, $f_{10}$은 그 지문으로 잡히지 않도록 설계된 함수입니다.

상한: weighted-sum interpolation (Theorem 4)

하한만 있으면 반쪽입니다. 저자들은 입력이 가중합 하나를 통해서만 함수에 영향을 줄 때의 constructive 상한을 제시합니다.

🧮 1. 정리

$\lambda_1,\dots,\lambda_n>0$에 대해 $t_\lambda(\mathbf{x})=\sum_i\lambda_ix_i$라 하고, $f(\mathbf{x})=F(t_\lambda(\mathbf{x}))$ 꼴이면

$$H^{\ast}(f)\le

\operatorname{Im}(t_\lambda)

-1.$$

$\lambda_i=2^{i-1}$을 잡으면 $t_\lambda$는 Boolean cube 위에서 단사이므로 $

\operatorname{Im}(t_\lambda)

=2^n$, 따라서 모든 Boolean 함수는 $2^n-1$개 head로 표현 가능합니다.

🔧 2. 구성

$M=

\operatorname{Im}(t_\lambda)

$, $\Lambda=\sum_i\lambda_i$, 서로 다른 $\alpha_1,\dots,\alpha_{M-1}>1$을 잡고

$$\phi_j(\mathbf{x})=\frac{\alpha_j\,t_\lambda(\mathbf{x})}{1+\Lambda+(\alpha_j-1)t_\lambda(\mathbf{x})}=g_j(t_\lambda(\mathbf{x}))$$

로 둡니다. 분모의 기울기 $(\alpha_j-1)\lambda_i$가 모두 양수이므로 atom입니다. $1,g_1,\dots,g_{M-1}$이 $\operatorname{Im}(t_\lambda)$ 위의 함수 공간의 기저를 이룬다는 것을(유리 함수의 분자가 $M-1$개 근을 갖는 차수 $\le M-2$ 다항식이라 항등적으로 0) 보이면, 목표 부호를 interpolation하여 $(M-1)$-head 표현을 얻습니다.

선택	$	\operatorname{Im}(t_\lambda)	$	상한
$\lambda_i=1$ (대칭 함수)	$n+1$	$H^{\ast}(f)\le n$
$\lambda_i=2^{i-1}$ (임의 함수)	$2^n$	$H^{\ast}(f)\le 2^n-1$

💡 Key Takeaway 각 head는 “$t_\lambda$ 의 한 값을 골라내는 유리 기저 함수”로 쓰일 수 있습니다. 값의 개수만큼 head가 있으면 어떤 라벨 패턴이든 interpolation할 수 있습니다.

대칭 함수의 정확한 특성화 (Theorem 5)

대칭 Boolean 함수에 대해서는 하한과 상한이 정확히 만납니다. 이것이 논문의 대표 결과이며, 동시 연구 Hsu and Xu (2026)와 독립적으로 얻어졌습니다.

📏 1. Hamming-weight profile과 변화 횟수

$f$가 대칭이면 유일한 $F:{0,\dots,n}\to{0,1}$이 있어 $f(\mathbf{x})=F(

\mathbf{x}

)$입니다($

\mathbf{x}

=\sum_ix_i$). 연속한 weight 수준 사이에서 $F$가 값을 바꾸는 횟수를

$$C(F)=\big

{k\in[n]:F(k-1)\ne F(k)}\big

로 정의합니다.

Theorem 5. 모든 대칭 Boolean 함수에 대해

$$H^{\ast}(f)=\deg_\pm(f)=C(F).$$

Corollary 2 (Parity). parity는 weight가 1 늘 때마다 값이 바뀌므로 $C(F)=n$, 따라서 $H^{\ast}(\mathrm{PARITY}_n)=n$ 입니다.

⚖️ 2. 하한과 상한

방향	논증
하한 $H^{\ast}\ge C(F)$	Aspnes et al. (1994) Lemma 2.6: 대칭 함수의 threshold degree는 univariate 표현의 변화 횟수와 같음, 즉 $\deg_\pm(f)=C(F)$. 여기에 Theorem 2를 결합. Appendix E.6은 대칭화(symmetrization) 논증으로 직접 재증명: 차수 $d$ sign-representing 다항식을 multilinearize하고 좌표 순열로 평균하면 $	\mathbf{x}	=k$에서 차수 $\le d$인 univariate $R(k)$가 되고, $F$가 바뀌는 구간마다 근이 하나씩 있어야 하므로 $d\ge C(F)$
상한 $H^{\ast}\le C(F)$	$F$가 바뀌는 각 지점 $k\in T$ 사이에 근을 하나씩 두는 다항식 $P(z)=\sigma_0\prod_{k\in T}(k-\tfrac12-z)$ 를 만들고, 양의 다항식 $B(z)=\prod_{h=1}^{C}(z+r_h)$ 로 나눈 뒤 부분분수 분해

$$\frac{P(z)}{B(z)}=c+\sum_{h=1}^{C}\frac{d_h}{z+r_h}$$

각 항 $d_h/(

\mathbf{x}

+r_h)$는 분모 기울기가 모두 1이고 분자가 상수인 atom이므로, Theorem 1에 의해 $C(F)$개 head로 실현됩니다.

🆚 3. 동시 연구와의 관계 (Appendix C)

연구	모델	결과	본 논문과의 관계
Hsu and Xu (2026)	positional embedding 없음, 차수 $D$ polynomial-threshold readout	$DH\ge\deg_\pm(f)$, 대칭 함수에서 exact	$D=1$에서 Theorem 5와 일치. 본 논문은 positional embedding을 허용해도 대칭 함수의 head 수는 줄지 않음을 추가로 보임
Rajaraman et al. (2026)	임의의 token-position 임베딩	parity는 정확히 $n$ head, $2^n$ 보편 상한, 거의 모든 함수에 $\Omega(2^n/n^2)$ 하한	Corollary 2와 일치. 그들의 Lemma 8은 Theorem 2와 같은 “분모 소거” 아이디어

본 논문만의 추가 기여는 (a) 정확한 linear-fractional 정규형, (b) 비대칭 separation $f_{10}$, (c) Lean 4 형식화입니다.

💡 Key Takeaway 대칭 함수에서는 “Hamming weight 축에서 몇 번 뒤집히는가“가 곧 head 수입니다. parity는 매번 뒤집히므로 가장 비싼 대칭 함수이고, 서론의 분산 계산 관찰은 이 결과의 직접적인 귀결입니다.

Autoresearch 파이프라인: 에이전트, 하니스, 연구 루프

이 논문의 또 다른 축은 “이 정리들을 누가, 어떻게 찾았는가” 입니다. 저자들은 익명화된 run 기록(theorems-rollout.jsonl)을 공개하고 Section 3에서 메타 분석합니다.

🤖 1. 에이전트와 환경

항목	내용
모델	GPT-5.6 Sol 단일 에이전트, xhigh reasoning effort
하니스	Codex Desktop, `/goal` 명령(지속적 목표·완료 조건 유지), Codex CLI 0.148.0-alpha.21, 258,400-token context, 4회 context compaction
샌드박스	로컬 Linux VM. 전체 파일시스템 읽기, 프로젝트·임시 디렉토리만 쓰기, 네트워크 없음. 경계 밖 행동은 승인 필요(기록상 요청 없음)
도구	Python 3, NumPy, SciPy, SymPy, shell, Git. 공개 웹 검색 비활성화(기존 해법 검색 차단)
subagent	multi-agent runtime이 가능했지만 사용하지 않음
Lean	초기 run에서는 호출하지 않음. 자연어 이론 개발 후 사용자 요청으로 도입
시작 상태	저장소에 `README.md`, `problem_statement.md`, `model.md`만 존재. 선행 결과·증명·서베이 없음

📝 2. 프롬프트 설계

프롬프트는 OpenAI (2026)의 “cycle double cover conjecture 증명” 프롬프트를 각색한 것으로, 다음을 요구합니다.

다양한 approach 포트폴리오를 시작하고, 수학적 아이디어 기준으로 approach family 레지스트리를 유지할 것
우아한 reduction이 하나의 approach를 지배하게 두지 말 것. 원래 추측과 동등한 강도의 lemma에서 멈춘 경로는 blocked로 표시
결과는 구체적 정리·구성·방정식·counterexample이어야 하며 “routine”이라는 주장은 거부
최소 8시간은 쓰고 나서야 반환을 고려할 것. 완전한 증명이 adversarial audit을 통과할 때까지 반환 금지

저자들은 예비 run에서 /goal만 주면 에이전트가 짧게 멈추고, 점진적 진전만 내고, 목표를 조기에 완료로 표시했다고 보고합니다. 지속성·탐색 지시를 넣는 것이 긴 run을 유지하는 데 중요했습니다.

🔄 3. 연구 루프와 통계

run은 두 단계로 진행되었습니다. 약 9시간 38분 동안 증명을 개발해 answer.md를 만들고, 이후 22분 만에 Lean 형식화를 완료하고 commit했습니다.

측정	값
tool call	949회 (그 안의 operation 960회: shell 387, 파일 편집 307, shell 세션 계속 205, goal 확인 55, goal/plan 갱신 6)
shell 분류	Python 153, sed 70, rg 40, 경험적 검사 실행 24, 파일 inspection 17, Git 14, 기타 55, 미분류 14
token	누적 input 약 142.4M (그중 140.2M, 98.5%가 cache), output 0.64M (reasoning 0.32M 포함)
approach family	13개 등록
외부 자원	공개 검색·외부 connector·위임 모델 호출 모두 0
비용	ChatGPT Pro 플랜으로 수행

에이전트는 approach_registry.md에 approach를 추적했고, 유한 인스턴스에서 정확 산술·전수 평가로 검사했습니다. 작은 경우의 패턴은 나머지 증명 단계를 완료할 수 있을 때만 일반 결과로 인정했고, counterexample이 나오면 blocked로 표시했습니다. 이 과정이 “그럴듯하지만 뒷받침되지 않은 일반화” 여러 개가 최종 답에 들어가는 것을 막았습니다.

목표	approach	결과
head complexity 재정식화	행렬 파라미터화를 head별 scalar 기여로 치환	Theorem 1
상한	가중합·대칭 함수에 대한 구성	Theorem 4, 5 + 미수록 bound
하한	threshold degree 비교, 더 많은 head가 필요한 함수 연구	Theorem 2 + 추가 하한 논증
후보 평가	유한 인스턴스에서 항등식·구성 검사	실패한 approach 기각, 미증명 lemma 필요 시 보류

💡 Key Takeaway 핵심 정리 세 개는 프롬프트 한 번, 사람 개입 0회, 약 9.5시간의 one-shot run에서 나왔습니다. 성공의 열쇠는 모델 자체보다 “여러 경로를 살려 두고, 유한 검사로 걸러내고, 조기 반환을 금지하는” 프롬프트 구조였습니다.

사람의 역할과 형식 검증(Lean 4)

“자율 연구”라고 해서 사람이 없었던 것은 아닙니다. 논문은 사람이 개입한 지점을 명시하고, 형식 검증을 환각 방지 장치로 사용합니다.

👤 1. 사람 개입 지점

단계	사람의 역할
문제 정의	연구 질문을 정밀하게 명세하고, 결과를 감사할 수 있는 모델을 고정(Appendix F.3, F.4). 닫힌 형태의 특성화를 가정할 수 없으므로 상·하한, 고전 척도와의 비교, 자연 함수족의 exact 결과 등 “넓은 의미의 진전”을 명시
정리 생성	초기 프롬프트 제출 후 `answer.md` 전달까지 추가 입력·lemma·정정 없음
Lean 형식화	에이전트에게 commit과 형식화를 요청. 생성된 코드는 의도한 결과를 담았지만 가독성·재사용성이 부족 → 사람이 최종 정리 집합 선택, Lean 명제가 의도한 주장과 일치하는지 확인, 명명·문서화·라이브러리 사용을 재구성
counterexample 탐색	명시적 반례를 찾기로 한 결정 자체가 사람의 것. 이후 설명 요청, 더 작은 예시 요청, 형식화 요청

✅ 2. 검증 체계

$$\text{Lean kernel이 각 증명을 검사} \;+\; \text{Lean 전문가가 형식 명제가 자연어 주장의 의미·가정·범위를 충실히 담는지 검사}$$

두 층이 함께 환각된 증명(hallucinated proof)을 막습니다. 기계 검증은 “증명이 맞는가”를, 사람은 “맞는 것을 증명했는가”를 봅니다. 향후에는 Lean의 comparator 도구(Lean FRO, 2026)로 신뢰할 수 없는 에이전트 증명을 사람이 검토한 정리 명제와 샌드박스에서 대조하는 방안을 제안합니다.

항목	내용
Lean / Mathlib	4.31.0 / 4.31.0
무거운 build	기관 SLURM 클러스터
공개 저장소	`github.com/VerifiedMechanisms/automlr` — `theorems/`(자연어), `formalization/`(Lean), `system-design/rollouts/`(run 기록)
초안 작성	Codex가 기술 논문 초안과 문장 수준 수정을 보조. 사람이 결과 절을 다듬고 system-design 절을 집필, 모든 주장·그림·참고문헌을 검증

💡 Key Takeaway 이 논문에서 사람은 “질문을 던지는 사람“과 “명제가 의도와 맞는지 판단하는 사람“입니다. 증명의 정확성은 Lean에게, 질문의 의미는 사람에게 맡기는 분업입니다.

Mechanistic interpretability에 대한 함의

저자들은 이 결과를 “head 수를 아키텍처 자원으로 보는” 이론적 기준점으로 자리매김합니다.

🔬 1. 학습된 해 vs 아키텍처의 요구

toy 모델에서 어떤 계산이 여러 head에 걸쳐 관찰될 때, 그것이 아키텍처가 요구한 것인지, 학습이 우연히 찾은 특정 해인지 구분할 수학적 기준이 생깁니다. parity의 경우 $H^{\ast}=n$이므로, 분산 구현은 선택이 아니라 필연입니다.

🧰 2. 아키텍처 인식 probe를 향해

현재의 feature 분해 방법(SAE 등, Cunningham et al. 2023; Shafran et al. 2026)은 활성화에서 feature를 학습하되 아키텍처가 실제로 구현할 수 있는 계산으로 feature를 제약하지 않습니다. Theorem 1의 정규형은 “head 하나가 실현할 수 있는 기여”를 정확히 특성화하므로, “주어진 feature를 한 attention layer 업데이트로 만들려면 head가 몇 개 필요한가”를 묻는 architecture-aware probe의 이론적 출발점이 될 수 있습니다.

🪜 3. 더 넓은 프로그램

현재	향후
1-layer, attention-only, Boolean, 정확 표현	attention → feed-forward → multi-layer로 feature를 추적하는 수학적 추상화
toy 설정의 exact 정리	대규모 학습 모델로의 transfer (아직 미입증)
Lean 환경의 초기 버전	transformer 부품에 관한 질문을 서술·검증하는 재사용 가능한 형식 환경

💡 Key Takeaway 결과 자체는 작은 모델에 대한 것이지만, 저자들이 노리는 것은 “feature 분해 도구를 아키텍처 이론으로 근거 짓는” 장기 프로그램의 첫 단추입니다.

한계와 autoresearch의 실패 모드

논문은 수학적 범위의 한계와 함께, autoresearch 과정 자체의 문제를 솔직하게 기록합니다.

⚠️ 1. 결과의 범위

정리는 1-layer attention-only 모델에서의 정확 표현에 관한 것이며, 배포된 시스템에 대한 안전성 보장이 아닙니다.
학습 동역학은 다루지 않습니다. “표현 가능”과 “학습으로 도달 가능”은 다른 문제입니다.
대규모 학습 모델로의 transfer는 시연되지 않았습니다.

🔍 2. 자율 연구의 감사 가능성(auditability)

긴 run이 만드는 추론·결과의 양이 너무 많아 진행을 검사하고 조종하기 어렵습니다. 어떤 approach가 진전했고 실패했고 버려졌는지 파악하려면 상당한 검토가 필요합니다. 연구 branch를 요약하고 주장의 상태를 추적하는 도구가 필요하다고 제안합니다.

🔁 3. 반복과 조기 진전 주장

공개된 rollout에는 다음이 실제로 들어 있습니다.

현상	설명
정체된 탐색의 장기 모니터링	진전 없는 탐색을 오래 지켜봄
틀린 설명의 반복	정정 전까지 같은 잘못된 설명을 되풀이
불필요한 새 bound	기존 bound가 더 강해서 나중에 제거된 bound를 제안

이 에피소드들은 최종 결과를 개선하지 못한 채 작업량만 늘렸습니다. 새 증거를 추적하고 반복적·근거 없는 주장을 표시하며 방향 전환이나 중단을 권고하는 모니터가 도움이 될 수 있지만, 그것이 실제로 연구 결과를 개선하는지는 아직 검증되지 않았습니다. 저자들은 UK AISI의 Inspect와 Inspect Scout를 각색해 로그 기반으로 run을 감사하는 방안을 제안합니다.

🧑‍🔬 4. 과학적 판단은 여전히 사람의 몫

최신 에이전트는 잘 정의된 문제를 푸는 데 능하지만, 고수준 질문을 던지고 autoresearch run을 안내하는 것은 여전히 연구자의 일이다.

넓은 질문에는 완전한 답으로 가는 명확한 경로가 없으므로, 연구자가 “경험적 해석 연구에 정보를 줄 수 있는 의미 있는 측면”을 분리하는 tractable한 이상화를 골라야 합니다. 저자들은 autoresearch 자체를 과학적 연구 대상으로 삼아, 프롬프트·도구·모니터링·사람의 조종·중단 규칙을 통제 비교해야 한다고 결론짓습니다.

💡 Key Takeaway 이 논문의 가장 정직한 부분은 “에이전트가 정리를 찾았다”가 아니라 “찾는 과정에서 무엇이 낭비였는지“를 기록으로 남겼다는 점입니다. 형식 검증은 결과의 정확성을 보증하지만, 과정의 효율과 질문의 가치는 아직 사람이 보증해야 합니다.