超越DeepSeek-ProverV1.5！豆包首个形式化数学推理模型BFS-Prover来了，直接开源

主要观点总结

本文介绍了机器之心AIxiv专栏及其报道内容，重点介绍了字节跳动豆包大模型团队推出的自动定理证明系统BFS-Prover。BFS-Prover作为一种简单但极具竞争力的自动定理证明系统，在形式化数学测试集MiniF2F上创造了新的记录。文章还详细阐述了BFS-Prover的技术特征，包括采用专家迭代框架、直接偏好优化和BFS中的长度归一化等技术。最后，作者对BFS-Prover的成功进行了总结，并展望了未来自动定理证明领域的发展。

关键观点总结

关键观点1: 机器之心AIxiv专栏介绍及其报道内容

机器之心是发布学术、技术内容的平台，其AIxiv专栏接收报道了2000多篇内容，涉及全球各大高校与企业的顶级实验室。该专栏促进了学术交流与传播，欢迎优秀的工作投稿或联系报道。

关键观点2: 介绍BFS-Prover

BFS-Prover是字节跳动豆包大模型团队推出的自动定理证明系统，采用了简单的BFS方法，但在形式化数学测试集上取得了很好的成绩。

关键观点3: BFS-Prover的技术特征

BFS-Prover采用了专家迭代框架、直接偏好优化和BFS中的长度归一化等技术，能够处理大规模定理证明任务。该系统通过不断优化，实现了简洁高效的自动定理证明。

关键观点4: BFS-Prover取得的成果

BFS-Prover在形式化数学测试集MiniF2F上取得了新的纪录，成为该领域的最新先进技术。该系统成功证明了多个复杂的数学问题，包括国际数学奥林匹克竞赛的题目。

关键观点5: 未来展望

作者认为，随着大语言模型能力的提升，BFS-Prover开创的简洁高效路线有望进一步推动自动形式化定理证明领域发展。团队计划进一步提升BFS方法在处理更复杂数学问题上的能力，并基于推理模型和其他前沿路线持续挖掘模型潜力。

文章预览

AIxiv专栏是机器之心发布学术、技术内容的栏目。过去数年，机器之心AIxiv专栏接收报道了2000多篇内容，覆盖全球各大高校与企业的顶级实验室，有效促进了学术交流与传播。如果您有优秀的工作想要分享，欢迎投稿或者联系报道。 投稿邮箱：liyazhou@jiqizhixin.com；zhaoyunfeng@jiqizhixin.com 自动形式化数学定理证明，是人工智能在数学推理领域的重要应用方向。此类任务需要将数学命题和证明步骤转化为计算机可验证的代码，这不仅能确保推理过程的绝对严谨性，还能构建可复用的数学知识库，为科学研究提供坚实基础。 早在上世纪中叶，戴维斯、明斯基等不少逻辑学家、数学家、人工智能先驱便已在探索相关问题，其中，也不乏王浩、吴文俊等华人身影。 近些年在 LLM 能力加持下，自动定理证明系统更多依赖于复杂的蒙特卡洛树搜索 (MCTS) 或价值函数 ( ………………………………