论形式数学中的作文学习行为

能够克服形式数学硬尾的自我进化科学主体需要组合学习行为（CLB）——在上下文中基础和重新组合新颖符号结构的能力，而不仅仅是预先学习的原子的重组。我们提出了 S2B-LM，它是 CLB 评估符号行为基准的改编版，它消除了作为混淆的数字处理，并添加了思想链支架以引出而不是仅仅探测潜在的 CLB 能力。对 S2B-LM 和 miniF2F 整体证明性能中的 CLB 能力进行交叉评估 10 个 Lean~4 定理证明者，我们发现了我们的主张的相关和因果证据：首先，通过象限测试进行必要条件分析，得出 $p=0.004$，模型规模被排除为混杂因素。其次，通过对比激活加法使用 S2B-LM 轨迹从 DeepSeek-Prover-V2-7B 中提取 CLB 编码激活方向，并将其应用于 AIME 子集上的 miniF2F 整体证明生成过程中，CLB 抑制将求解率从 $32.3\%$ 降低到 $2.9\%$，而不会损失一致性，同时抑制同等幅度的随机激活方向使其保持在 $31.9\%$。总之，这些结果表明 CLB 能力对于形式数学验证的硬尾来说是必要的，但还不够。