형식 수학에서의 구성적 학습 행동에 대하여

형식 수학 (Formal Mathematics)의 어려운 난제들을 정복할 수 있는 자기 진화형 과학 에이전트 (Self-evolving scientific agents)에게는 구성적 학습 행동 (Compositional Learning Behaviours, CLBs)이 필요합니다. 이는 단순히 미리 학습된 원자 (Atoms)들을 재조합하는 것을 넘어, 문맥 속에서 새로운 상징적 구조 (Symbolic structures)를 근거화하고 재결합할 수 있는 능력을 의미합니다. 본 연구에서는 수치 처리 (Numerical processing)를 혼란 변수 (Confound)에서 제거하고, 잠재적인 CLB 역량을 단순히 탐색하는 것을 넘어 이끌어내기 위해 사고의 사슬 (Chain-of-thought) 스캐폴딩 (Scaffolding)을 추가한 Symbolic Behaviour Benchmark의 변형 모델인 \textbf{S2B-LM}을 제안합니다. 10개의 Lean~4 정리 증명기 (Theorem provers)를 대상으로 CLB 역량 (adj-ZSCT)과 miniF2F 전체 증명 성능을 교차 평가한 결과, 정확한 순열 검정 (Exact permutation tests)을 통해 계층적 필요 구조를 확립했습니다. 즉, 탐색 중심적인 (Search-heavy) 모델들은 감지 가능한 CLB 없이도 다루기 쉬운 대부분의 문제를 해결하지만, 올림피아드 수준의 계층 (miniF2F $>75%$)에 진입하는 모든 모델은 CLB 점수가 가장 높은 상위 5개 모델에 포함되었습니다 ($p=0.004$). 모델 규모를 혼란 변수에서 배제한 후, 우리의 결과는 CLB 역량이 형식 수학 검증의 어려운 난제들을 해결하기 위해 \emph{필요조건이지만 충분조건은 아님}을 보여줍니다.