★ 4
基于 Gemini 的智能体在忙碌海狸 BB(6) 自主发现并形式化验证加速规则
论文构建基于 Gemini 的智能体流水线,整合模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明,在不可计算的忙碌海狸 BB(6) 领域自主发现并形式化验证了 11 台图灵机的新型 Collatz 式加速规则。这些机器暂被归类为 Cryptids,展示了 AI 在开放式数学发现中的潜力。
arXiv cs.AI13 天前
共 2 篇相关资讯,按重要度与时间排序,每 3 小时更新。
论文构建基于 Gemini 的智能体流水线,整合模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明,在不可计算的忙碌海狸 BB(6) 领域自主发现并形式化验证了 11 台图灵机的新型 Collatz 式加速规则。这些机器暂被归类为 Cryptids,展示了 AI 在开放式数学发现中的潜力。
论文提出 PermuFormer,一个在 28 亿 token 多任务多编码语料上训练的自回归 Transformer,用于代数组合中置换相关任务的预训练。实验表明它是微调预训练未见基础任务与更复杂研究级任务的有效起点,常优于从零训练的同架构、基线 MLP 及同规模通用语言模型。作者还分析了其内部…