论形式数学中的组合学习行为
On Compositional Learning Behaviours in Formal Mathematics
AI总结：
本文提出 S2B-LM 基准，通过去除数值处理混淆并添加思维链框架来评估组合学习行为（CLB），发现 CLB 能力对于形式数学验证的困难部分必要但不充分。
摘要：
能够征服形式数学困难尾部的自我进化科学智能体需要组合学习行为（CLBs）——在上下文中基础化和重组新颖符号结构的能力，而不仅仅是预学习原子的重组。我们提出了 extbf{S2B-LM}，这是符号行为基准的一个改编，它移除了数值处理作为混淆因素，并添加了思维链框架以引发而非仅仅探测潜在的 CLB 能力。在 CLB 能力（adj-ZSCT）和 miniF2F 整体证明性能上交叉评估十个 Lean~4 定理证明器，精确置换检验建立了一个层次必要性结构：搜索密集型模型覆盖了可处理的绝大部分而没有可检测的 CLB，然而每个进入奥林匹克级别（miniF2F $>75\%$）的模型都是五个最高 CLB 得分者之一（$p=0.004$）。在排除模型规模作为混淆因素后，我们的结果表明 CLB 能力对于形式数学验证的困难尾部是 \emph{必要但不充分的}。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
