摘要
能够攻克形式化数学难题的自我进化科学智能体需要具备组合学习行为（CLBs），即在上下文中 grounding 并重组新颖符号结构的能力。本文提出 S2B-LM，通过移除数值处理干扰并引入思维链支架来激发潜在的 CLB 能力。对十个 Lean 4 定理证明器的交叉评估表明，搜索密集型模型虽能解决常规问题但缺乏 CLB，而所有突破奥林匹克级别性能的模型均具备高 CLB 得分。结果证实，CLB 能力是解决形式化数学验证长尾难题的必要非充分条件。
AI 推荐理由
论文核心研究形式化数学中的组合学习行为与思维链推理，直接关联推理能力。
研究机构
Work conducted as an Independent Researcher during the revision phase of a PhD at the University of York. Correspondence to: Kevin Yandoka DenanganaI
论文信息