On Compositional Learning Behaviours in Formal Mathematics

arXiv:2605.28512v1 Announce Type: new Abstract: Self-evolving scientific agents capable of conquering the hard tail of formal mathematics require Compositional Learning Behaviours (CLBs) -- the capacity to ground and recombine novel symbolic structures in context, beyond mere recombination of prelearned atoms. We propose extbf{S2B-LM}, an adaptation of the Symbolic Behaviour Benchmark that removes numerical processing as a confound and adds chain-of-thought scaffolding to elicit rather than merely probe latent CLB competency. Cross-evaluating ten Lean~4 theorem provers on CLB competency (adj-ZSCT) and miniF2F whole-proof performance, exact permutation tests establish a hierarchical necessity structure: search-heavy models cover the tractable bulk without detectable CLBs, yet every model breaking into the Olympiad-level tier (miniF2F >75%) is among the five highest CLB scorers (p=0.004). After ruling out model scale as a confound, our results show that CLB competency is necessary but not sufficient for the hard tail of formal mathematical verification.

Source: arXiv cs.CL | 2026-05-28