기술 요약: 방정식 발견을 위한 포화 스케일링 법칙

문제 제기

본 논문은 방정식 재작성 규칙을 추가하며 성장하는 결정론적 기호 발견 시스템이 대규모 언어 모델 (LLM) 에서 발견된 것과 유사한 경험적 스케일링 법칙을 따르는지 조사한다. 신경망 모델에 대한 스케일링 법칙 (Kaplan et al., 2020; Hoffmann et al., 2022) 은 잘 정립되어 있지만, 귀납적 논리 프로그래밍, 등식 포화 (equality saturation), 프로그램 합성 등에 사용되는 결정론적 기질이 유사한 성장 역학을 따르는지는 여전히 열린 질문으로 남아 있다. 저자들은 이러한 시스템에서의 성장 현상학을 규명하고, 단순한 멱법칙 (power-law) 이 발견된 규칙의 누적을 더 잘 설명하는지 아니면 더 복잡한 포화 함수가 더 적합한지 검증하고자 한다.

방법론

본 연구는 점증적인 타입 복잡성을 가진 세 가지 "토이 (toy)" 결정론적 기질을 포함하는 통제된 실험 프레임워크를 사용한다:

1. 산술 (arith): 덧셈, 곱셈 및 자유 변수를 갖는 타입 지정 문법 위의 방정식 항등식.
2. 부울 (bool): 논리 연산자 (and, or, not) 에 대한 항등식.
3. 고차원 리스트 (list): map, fold, cons 와 같은 원시 연산을 갖춘 DreamCoder 에서 영감을 받은 도메인.

발견 루프:
시스템은 이산적인 단계 $t$를 거쳐 기질 $S$(재작성 규칙 집합) 를 성장시킨다. 각 단계에서:

• 생성기는 $S$의 현재 상태를 기반으로 후보 방정식을 제안한다 (무작위, 구성적, 빈도 가중, 또는 MDL-탐욕적 전략 등 사용).
• 후보들은 무작위 인스턴스화를 통해 의미적 건전성을 테스트받는다.
• 승인된 쌍은 일반화된다 (자유 변수를 패턴 변수로 대체).
• 구성 가능한 승인 필터 ("any" 또는 "novelty") 가 규칙이 $S$에 확정될지 여부를 결정한다.

데이터 수집:
저자들은 다섯 가지 아키텍처 특징 (생성기 유형, 필터 엄격도, 재귀 깊이, 배치 크기, 무작위 시드) 을 변화시켜 이러한 기질 전반에 걸쳐 592 개의 독립적인 발견 궤적을 생성했다. 그들은 시간에 따른 총 규칙 수 $|S(t)|$를 측정했다.

모델링 접근법:
저자들은 균일한 커버리지와 근사적 독립성에 대한 가정에서 유도된 휴리스틱 평균장 폐쇄 모델을 제안한다. 이는 성장에 대한 미분 방정식을 산출한다:
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
여기서 $N$은 기질 크기, $k$는 생성기의 재조합 깊이와 관련되며, $\mu$는 후보 공간의 커버리지 비율을 나타낸다.

• 단거리 ($\mu N \ll 1$): 이 방정식은 순수 멱법칙 $N(t) \propto t^b$로 근사되며, 여기서 $b = 1/(1-k)$이다.
• 장거리 ($\mu N \gtrsim 1$): 지수 항은 로지스틱 - 멱법칙 형태로 모델링된 포화를 유도한다.

본 연구는 모델 선택을 위해 AIC 를 사용하고 아키텍처 특징으로부터 지수 $b$를 예측하기 위해 그래디언트 부스팅 회귀를 사용하여 세 가지 후보 모델 (순수 멱법칙, 늘어난 지수, 포화 멱법칙) 을 데이터에 적합시켰다.

주요 기여 및 결과

1. 단거리 멱법칙 역학

592 개의 궤적 전반에 걸쳐, 단거리 (최대 30 에포크) 에서 기질 크기 $|S(t)|$의 성장은 일관되게 멱법칙 형태 $t^b$에 적합된다. 지수 $b$는 도메인과 아키텍처에 따라 0 에서 1.15 사이에서 연속적으로 변한다.

• 아키텍처 민감도: 단일 기질 내에서 지수 $b$는 아키텍처 선택에 매우 민감하다. 다섯 가지 아키텍처 특징을 사용하는 그래디언트 부스팅 회귀기는 산술/부울 및 리스트 도메인 모두에 대해 교차 검증된 $R^2 \approx 0.82$로 $b$를 예측한다.
• 기질 간 전이 실패: 산술 및 부울 데이터에서 $b$를 예측하도록 훈련된 모델은 리스트 도메인에 적용될 때 완전히 실패한다 ($R^2 \approx -0.84$). 평평한 타입 기질 (예: 신규성 필터) 에서 복합 성장을 위한 최적 아키텍처는 고차원 타입 기질에서는 성장을 억제한다. 이는 성장 역학이 보편적인 것이 아니라 기질 조건부임을 나타낸다.

2. 장거리 포화 가설

저자들은 폐쇄 모델이 예측한 대로 성장이 결국 포화되는지 테스트했다.

• 토이 데이터 (리스트 도메인): 다섯 개의 리스트 도메인 궤적을 500 에포크까지 확장했을 때, 200 에포크보다 긴 궤적에 대해 포화 멱법칙 모델이 인 - 샘플 AIC 비교에서 승리했다. 그러나 아웃 - 오브 - 샘플 예측 (첫 100 에포크에 적합하고 다음 400 에포크를 예측) 은 모든 5 가지 사례에서 순수 멱법칙이 승리했다. 저자들은 토이 궤적이 실제로 500 에포크 내에 포화 영역에 도달하지 않았다고 결론지었다. 인 - 샘플에서 포화 모델이 선호되는 것은 외삽이 잘되지 않는 피팅 아티팩트일 가능성이 높다.
• 실제 세계 데이터 (Mathlib4): Mathlib4 라이브러리의 월별 새로운 .lean 파일 추가 (60 개월, 9,701 개 파일) 에 대한 분석은 포화 형태를 지지한다. 포화 모델은 아웃 - 오브 - 샘플 예측에서 순수 멱법칙보다 약 $7\times$배 더 우수하게 수행되었다 (RMSE 3,279 대 23,896). 이는 Mathlib4 가 포화 영역에 도달했음을 시사한다.
• 실제 세계 데이터 (Coq Mathcomp): Coq Mathcomp 라이브러리의 월별 커밋 (129 개월) 에 대한 분석은 순수 멱법칙을 지지한다. 포화 매개변수 $\mu$는 0 으로 붕괴되며, 순수 멱법칙은 아웃 - 오브 - 샘플 예측에서 포화 모델보다 약 $67\times$배 더 우수하게 수행된다. 이는 Mathcomp 가 아직 포화 영역에 도달하지 않았음을 시사한다.

3. 현상학적 틀

본 논문은 다음과 같은 작업 틀을 제안한다: "기질이 포화 영역에 도달했을 때 관찰 가능한, 기질 조건부 $(k, \mu)$를 갖는 포화 멱법칙 성장." 역학은 두 수준에서 조건부이다:

1. 성장 지수를 예측하는 아키텍처 매개변수는 서로 다른 기질 유형 간에 전이되지 않는다.
2. 성장을 설명하는 함수 계열 (순수 대 포화 멱법칙) 은 기질의 특정 수명 주기 단계에 의존한다.

중요성 및 주장

본 논문은 결정론적 방정식 발견의 스케일링 법칙에 대한 첫 경험적 및 이론적 조사로 자신을 위치시키며, 확정적인 이론이 아닌 현상학을 제공한다.

• 겸손한 범위: 저자들은 증거가 세 가지 토이 기질과 두 가지 실제 세계 대리 변수 (커밋/파일 수에 의존하는 거친 데이터) 에만 국한되어 있음을 명시적으로 밝힌다. 토이 데이터에 대한 아웃 - 오브 - 샘플 예측 실패로 인해 장거리 토이 결과는 "확인된 것이 아니라 일관된 것"으로 인정한다.
• 주요 통찰: 주요 발견은 기호 발견 역학이 기질 조건부라는 것이다. 종종 아키텍처 전반의 보편성을 가정하는 신경 스케일링 법칙과 달리, 여기서의 성장 행동은 기질의 타입 시스템의 특정 "폐쇄 기하학"(커버리지 매개변수 $\mu$) 에 크게 의존한다.
• 향후 방향: 저자들은 이 작업을 "토이 현상학"에서 "진정한 현상"으로 격상시키기 위해 필요한 세 가지 구체적인 업그레이드를 식별한다:
  1. 커밋 수뿐만 아니라 궤적 수준의 세분성을 가진 비 - 토이 기질에서의 재현.
  2. 포화 모델에 대한 성공적인 아웃 - 오브 - 샘플 예측적 예측.
  3. 기질 조합론 (예: 타입 엔트로피) 에서 포화 매개변수 $\mu$의 이론적 유도 (기질 간 전이를 반증 가능하게 만들기 위해).

본 논문은 포화 멱법칙 프레임워크가 포화가 타당한 영역에서 관찰된 데이터와 일관되지만, 모든 기호 발견 시스템에 대한 보편적 법칙은 아니라고 결론지었다. 이 작업은 잠재적인 "기호 발견의 통계 역학"을 위한 출발점으로 기능한다.