On Compositional Learning Behaviours in Formal Mathematics

Kevin Yandoka Denamganai

AI4Math Workshop, ICML 2026 · OpenReview

---

Abstract

This work examines how language models develop the capacity to ground and recombine novel symbolic structures in context. We introduce S2B-LM, a modified benchmark for evaluating Compositional Learning Behaviours (CLBs), and evaluate it across ten Lean 4 theorem provers on miniF2F. Our findings indicate that CLB competency is necessary but not sufficient for solving difficult formal mathematics problems: statistical tests reveal a significant correlation (p = 0.004), while causal manipulation experiments via activation direction extraction demonstrate significant performance degradation when Compositional Learning Behaviour signals are suppressed.

---

Repository Structure

meta-rg-s2b/
├── run_eval.py                  ← zero-shot S2B-LM listener evaluation
├── run_grpo.py                  ← GRPO/RLVR fine-tuning
├── configs/
│   ├── base.yaml                ← shared S2B defaults
│   └── eval/                    ← one YAML per model / backend
├── meta_rg/                     ← core library (backends, env utils, metrics)
├── scripts/
│   └── steering/                ← CLB direction extraction, activation steering,
│                                   miniF2F pipeline, monitoring and analysis
└── third_party/
    └── Goedel-Prover-V2/        ← Lean 4 compiler utilities (git submodule)

---

Dependencies

S2B-LM (required)

The S2B-LM extension of the Symbolic Behaviour Benchmark is a prerequisite for replicating all results in this paper. It is maintained in a dedicated branch of the original repository:

https://github.com/Near32/SymbolicBehaviourBenchmark/tree/S2B-LM

Install it before anything else:

git clone --branch S2B-LM https://github.com/Near32/SymbolicBehaviourBenchmark.git
pip install -e SymbolicBehaviourBenchmark

Then install this package and its dependencies:

pip install -e .

Optional backends:

pip install -e ".[openai]"        # OpenAI API (GPT-4o-mini, etc.)
pip install -e ".[vllm]"          # vLLM local inference
pip install -e ".[llamacpp]"      # llama.cpp CPU inference
pip install -e ".[bitsandbytes]"  # 4-bit quantisation (HF models)
pip install -e ".[cot]"           # DSPy chain-of-thought

Lean 4 / Goedel-Prover-V2

Initialise the submodule for Lean compilation utilities:

git submodule update --init --recursive

---

Correlational Experiment

The correlational evidence rests on cross-evaluating ten state-of-the-art Lean 4 theorem provers on two axes: Compositional Learning Behaviour competency (adj-ZSCT on S2B-LM) and miniF2F whole-proof test-split Pass@32 (collected from the respective published papers).

S2B-LM evaluation (adj-ZSCT) is run per model via:

python run_eval.py --config configs/eval/<model>.yaml \
    --domain categorical --o 1 --shots 1 \
    --n_dim 3 --v_min 3 --v_max 5 \
    --prompt_strategy few_shot_discussion_cot --n_few_shot_games 10 \
    --n_seeds 8 --n_episodes 1

The adjusted ZSCT (adj-ZSCT) maps raw ZSCT onto ability above the 50% guessing floor: adj-ZSCT = max(0, (ZSCT − 50) / 50) × 100.

S2B-LM settings used in the paper: N_dim=3, V_min=3, V_max=5, O=1 (the categorical domain does not support object-centric sampling), S=1 (every atomic element appears in at least one target stimulus before the querying phase begins), 10-shot chain-of-thought verbalizer, 8 random seeds per model.

Statistical test. A necessary-condition analysis is performed via a quadrant test: each axis is dichotomised at its empirical median (adj-ZSCT median = 23.3; miniF2F median = 67.95%), and the forbidden cell (high miniF2F, low adj-ZSCT) is tested for depletion via a one-sided Fisher's exact test by exact enumeration of all $\binom{10}{5} = 252$ high-performance label placements. The forbidden cell is empty in the observed data, yielding $p = 0.004$. The test is implemented in:

python scripts/analysis/quadrant-test-analysis.py

---

Causal Experiment - Activation Steering Pipeline

The causal experiments in the paper proceed in five stages.

1. Extract the CLB direction (CAA vector)

Derive the Compositional Learning Behaviour direction from correct-vs-corrupted teacher-forced activations on S2B-LM:

bash scripts/steering/collect_clb_activations.sh

2. Validate on S2B-LM (causal suppression)

Run the α-sweep on S2B-LM to confirm that suppressing the CLB direction drives performance to chance while matched-norm controls remain at baseline:

bash scripts/steering/steer_s2b_sweep.sh

3. Evaluate on the AIME subset with CLB suppression

Generate proof attempts on the 15 AIME problems under baseline (α=0), CLB suppression (α=−3), CLB amplification (α=+1), and random controls at matching magnitudes; compile each proof via the Goedel REPL; then collate solve rates and coherence figures:

bash scripts/steering/run_aime_caa_steering_dsp7b.sh

This runs the full generate → compile → collate pipeline sequentially (single GPU). Each generation cell is resumable: re-running the script skips already-completed problems.

---

Citation

@inproceedings{denamganai2026clb,
  title     = {On Compositional Learning Behaviours in Formal Mathematics},
  author    = {Denamgana{\"i}, Kevin Yandoka},
  booktitle = {ICML 2026 Workshop on AI for Mathematics (AI4Math)},
  year      = {2026},
  url       = {https://openreview.net/forum?id=M3kKajgMpY}
}

---

License

This code is released under the MIT License.