On Compositional Learning Behaviours in Formal Mathematics

📄 arXiv: 2605.28512v1 📥 PDF

作者: Kevin Yandoka Denamganaï

分类: cs.CL

发布日期: 2026-05-27

备注: work in progress, under review

💡 一句话要点

提出S2B-LM基准，研究形式化数学中组合学习行为对定理证明的影响。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化数学 定理证明 组合学习 思维链 基准测试

📋 核心要点

  1. 现有定理证明模型在处理复杂形式化数学问题时，缺乏组合学习能力，难以泛化到新的符号结构。
  2. 论文提出S2B-LM基准，通过移除数值混淆和引入思维链，更有效地评估模型的组合学习行为。
  3. 实验表明，组合学习能力是模型在形式化数学难题上取得高性能的必要条件，但并非充分条件。

📝 摘要（中文）

为了使能够征服形式化数学难题的自进化科学智能体成为可能，需要组合学习行为(CLBs)——即在上下文中扎根并重组新的符号结构的能力，而不仅仅是预先学习的原子符号的重组。我们提出了S2B-LM，它是符号行为基准的一个改进版本，消除了数值处理的混淆，并增加了思维链脚手架，以引出而非仅仅探测潜在的CLB能力。通过在CLB能力(adj-ZSCT)和miniF2F整体证明性能上交叉评估十个Lean 4定理证明器，精确的排列测试建立了一个分层必要结构：重搜索模型覆盖了易于处理的大部分，而没有可检测的CLB，但每个突破奥林匹克级别(miniF2F >75%)的模型都在五个最高的CLB得分者之列(p=0.004)。在排除模型规模作为混淆因素后，我们的结果表明，CLB能力对于形式化数学验证的难题是必要但不充分的。

🔬 方法详解

问题定义：论文旨在解决形式化数学定理证明中，现有模型缺乏有效组合学习能力的问题。现有方法往往侧重于对预定义符号的简单重组，难以处理需要创造性组合新符号结构的复杂问题，导致在形式化数学难题上表现不佳。

核心思路：论文的核心思路是通过设计新的基准测试（S2B-LM），更准确地评估模型在形式化数学领域的组合学习行为（CLBs）。通过引入思维链（Chain-of-Thought）提示，引导模型展示其推理过程，从而更有效地激发和评估其潜在的组合学习能力。

技术框架：S2B-LM基准是基于Symbolic Behaviour Benchmark的改进版本。主要改进包括：1) 移除数值处理，避免数值计算对组合学习能力的干扰；2) 引入思维链脚手架，鼓励模型逐步推理，从而更清晰地展现其组合学习过程。论文使用该基准评估了十个Lean 4定理证明器，并结合miniF2F基准评估了模型的整体证明性能。

关键创新：论文的关键创新在于提出了S2B-LM基准，该基准能够更有效地评估模型在形式化数学领域的组合学习行为。与传统基准相比，S2B-LM通过移除数值混淆和引入思维链，能够更准确地衡量模型在符号结构上的组合和泛化能力。

关键设计：S2B-LM基准的设计关键在于：1) 题目设计：题目需要能够考察模型对新符号结构的创造性组合能力；2) 思维链提示：思维链提示需要能够引导模型逐步推理，并清晰地展现其组合学习过程；3) 评估指标：评估指标需要能够准确地衡量模型的组合学习能力，例如adj-ZSCT指标。

📊 实验亮点

实验结果表明，在miniF2F基准上取得超过75%性能的模型，均在S2B-LM基准上获得了较高的组合学习能力得分(p=0.004)，表明组合学习能力是解决形式化数学难题的必要条件。同时，实验也发现，仅具备高组合学习能力并不足以保证在miniF2F上取得优异成绩，说明还需要其他因素的配合。

🎯 应用场景

该研究成果可应用于开发更强大的自动化定理证明器，提升数学研究效率。此外，组合学习能力的研究对于通用人工智能的发展具有重要意义，有助于构建具备更强推理和泛化能力的智能系统，应用于科学发现、软件验证等领域。

📄 摘要（原文）

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 \textbf{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 \emph{necessary but not sufficient} for the hard tail of formal mathematical verification.