# On Compositional Learning Behaviours in Formal Mathematics

arXiv: https://arxiv.org/abs/2605.28512 · HTML: https://mlsanity.com/paper/2605.28512/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 23 of its 38 references that are in the map.
- First posted on arXiv 27 May 2026.

## Builds on (most cited first, 23 of 23)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Emergent Abilities of Large Language Models](https://mlsanity.com/paper/2206.07682/) (2022)
- [HuggingFace's Transformers: State-of-the-art Natural Language Processing](https://mlsanity.com/paper/1910.03771/) (2019)
- [Steering Llama 2 via Contrastive Activation Addition](https://mlsanity.com/paper/2312.06681/) (2023)
- [Steering Language Models With Activation Engineering](https://mlsanity.com/paper/2308.10248/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [COGS: A Compositional Generalization Challenge Based on Semantic Interpretation](https://mlsanity.com/paper/2010.05465/) (2020)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Compositionality and Generalization in Emergent Languages](https://mlsanity.com/paper/2004.09124/) (2020)
- [Number Cookbook: Number Understanding of Language Models and How to Improve It](https://mlsanity.com/paper/2411.03766/) (2024)
- [Can language models handle recursively nested grammatical structures? A case study on comparing models and humans](https://mlsanity.com/paper/2210.15303/) (2022)
- [Symbolic Behaviour in Artificial Intelligence](https://mlsanity.com/paper/2102.03406/) (2021)
- [Meta-Referential Games to Learn Compositional Learning Behaviours](https://mlsanity.com/paper/2207.08012/) (2022)

## Abstract (arXiv)

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 S2B-LM, an adaptation of the CLB-evaluating 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 in S2B-LM and miniF2F whole-proof performance, we find correlational and causal evidence of our claim: First, a necessary-condition analysis via quadrant test yields p=0.004, with model scale being ruled out as a confound. Second, extracting a CLB-encoding activation direction from DeepSeek-Prover-V2-7B using S2B-LM traces via Contrastive Activation Addition and applying it during miniF2F whole-proof generation on the AIME subset, CLB suppression collapses solve rate from 32.3% to 2.9%, without loss of coherence, while suppressing a random activation direction of equal magnitude leaves it at 31.9%. Together, these results show that CLB competency is necessary but not sufficient for the hard tail of formal mathematical verification.