On Compositional Learning Behaviours in Formal Mathematics

Motivation

• Known: Symbolic Behaviour Benchmark(S2B)은 Compositional Behaviours(CB)와 이를 온라인 문맥에서 확장한 Compositional Learning Behaviours(CLB)를 구분하여 평가할 수 있는 진단 도구로 알려져 있으며, Lean 4 기반 whole-proof generation 모델들은 SFT와 Monte Carlo tree search를 결합해 miniF2F pass@32 성능을 크게 향상시켜 왔다.
• Gap: 기존 S2B는 numerical value에 크게 의존해 LM의 numerical understanding and processing abilities(NUPA) 부족이 혼입 변수로 작용하며, competence-performance distinction을 고려하지 않아 zero-shot 평가(ZSCT)가 CLB 능력의 부재와 단순 수행 실패를 혼동할 위험이 있어, 정형 정리 증명기에서 CLB 능력과 실제 hard-tail 성능 간의 관계를 명확히 검증한 연구가 부재했다.
• Why: self-evolving scientific agent가 형식 수학의 어려운 영역을 자율적으로 정복하기 위한 근본적 능력이 무엇인지 규명하는 것은, 향후 모델 아키텍처 설계와 훈련 패러다임 개선의 방향을 제시하는 데 핵심적이며, 단순 계산 자원 확장이 아닌 진정한 상징 처리 능력 함양이 필요함을 실증적으로 보여준다.
• Approach: numerical stimulus를 categorical stimulus로 대체하고 rule-based verbalizer로 chain-of-thought scaffolding을 추가한 S2B-LM을 제안하여 CLB 잠재 역량을 이끌어내고, 이를 miniF2F whole-proof 성능과 교차 평가하여 quadrant test와 CAA 기반 인과적 개입으로 CLB의 필요성을 검증한다.

Achievement

1. CLB의 필요조건 입증: quadrant test 분석 결과 forbidden cell(높은 miniF2F, 낮은 adj-ZSCT)이 비어 있음을 p=0.004로 확인하여, Olympiad급 성능 달성에는 측정 가능한 CLB 역량이 필수적임을 보였다.
2. 모델 규모 교란요인 배제: DeepSeek-Prover-V2-7B가 단 7B 파라미터로도 miniF2F 75.6%를 달성해 Olympiad 문턱을 넘어서면서, 모델 규모가 hard tail 성능의 필요조건이 아님을 입증했다.
3. CAA를 통한 인과적 증거 확보: DSP-V2-7B에서 S2B-LM trace를 이용해 Contrastive Activation Addition으로 CLB 인코딩 활성화 방향을 추출하고 AIME 부분집합에서 억제 실험을 수행한 결과, solve rate가 32.3%에서 2.9%로 붕괴한 반면 동일 크기의 무작위 방향 억제는 31.9%로 거의 영향이 없어 CLB 방향의 인과적 필요성을 입증했다.
4. S2B-LM 벤치마크 제안: numerical 혼입 요인을 제거하는 categorical stimulus domain과 competence-performance distinction 문제를 완화하는 rule-based CoT verbalizer를 도입하여 LM의 CLB 역량을 더 정밀하게 평가할 수 있는 개선된 벤치마크를 제시했다.

How

• S2B의 continuous(수치) stimulus domain을 categorical domain으로 교체해 NUPA 관련 혼입 요인을 제거
• episode의 sync round로부터 chain-of-thought 예시를 생성하는 rule-based verbalizer를 도입해 잠재적 CLB 역량을 유도(elicit)
• adj-ZSCT(Zero-Shot Compositional Test score를 무작위 추측 기저선 50%를 제거해 [0,100] 척도로 조정한 지표)를 산출하여 10개의 최신 Lean 4 정리 증명 모델을 평가
• miniF2F whole-proof test-split pass@32 성능과 adj-ZSCT를 교차 평가
• 각 축을 경험적 중앙값으로 이분화한 quadrant test를 수행하여 (10 choose 5)=252 가지 라벨 배치에 대해 forbidden cell(높은 miniF2F, 낮은 adj-ZSCT)의 결핍 여부를 검정
• Contrastive Activation Addition을 이용해 S2B-LM trace로부터 CLB 인코딩 활성화 방향을 추출하고, miniF2F AIME 부분집합 whole-proof generation에 적용해 CLB 억제 및 동일 크기 무작위 방향 억제를 비교하는 대조 실험 수행

Originality

• CLB(Compositional Learning Behaviours) 개념을 형식 수학 정리 증명이라는 실세계 고난도 과제에 최초로 적용하고 검증한 점
• 기존 S2B 벤치마크의 numerical 혼입 요인과 competence-performance distinction 문제를 명시적으로 통제한 S2B-LM이라는 개선된 진단 도구를 제안한 점
• 단순 상관관계 분석을 넘어 quadrant test라는 필요조건 검정 방법론과 Contrastive Activation Addition을 이용한 인과적 개입 실험을 결합하여, CLB 역량이 hard-tail 성능에 필요하지만 충분하지 않다는 이중적 결론을 실증적으로 도출한 점
• 모델 규모라는 대표적 교란변수를 DeepSeek-Prover-V2-7B 사례를 통해 직접 배제한 점

Limitation & Further Study

• 인과 개입 실험이 단일 모델(DeepSeek-Prover-V2-7B)과 AIME 부분집합에 국한되어 있어 일반화 가능성 검증이 제한적임
• receptivity 측면만 다루고 constructivity 측면은 이론적 논증(receptive bottleneck이 constructivity를 붕괴시킨다는 주장)에 의존하며 직접 실증하지 않음
• CAA로 추출된 단일 활성화 방향이 CLB 개념 전체를 얼마나 온전히 포착하는지에 대한 추가 검증(예: 다양한 방향 추출 기법 비교, 여러 레이어에서의 강건성 분석)이 필요함
• miniF2F 외 LeanDojo, PutnamBench 등 다른 형식 검증 벤치마크에서의 재현 실험이 후속 연구로 요구됨

Evaluation

총평: 형식 수학 정리 증명이라는 고난도 실제 과제에서 compositional learning behaviour의 필요성을 상관관계와 인과관계 양면에서 정교하게 입증한 흥미로운 연구로, 벤치마크 설계와 해석 가능성(interpretability) 개입 기법을 결합한 방법론적 기여가 돋보이나 단일 모델 기반 인과 실험의 일반화 검증이 추가로 필요하다.