字节发布 Seed Prover 1.5：全新 Agentic 架构，更强数学推理表现-低调大师

字节发布 Seed Prover 1.5：全新 Agentic 架构，更强数学推理表现

2025-12-24 6

字节跳动 Seed 团队推出新一代形式化数学推理专用模型 Seed Prover 1.5，通过大规模的 Agentic RL 训练，其推理能力和推理效率取得显著进步。相比上一代模型，Seed Prover 1.5 在 16.5 小时内，针对 IMO 2025 的前 5 道题目生成了完整可编译验证的 Lean 证明代码，换算成绩为 35/42，达到此前 IMO 评分标准的金牌分数线。

更系统的评估中，Seed Prover 1.5 在完整的 Putnam 历史评估集上解决了 88% 的问题，在代表硕士数学难度的 Fate-H 和代表博士生数学难度的 Fate-X 评估集上，分别解决了 80% 和 33% 的问题，刷新了形式化数学推理模型在这几个评测集上的 SOTA 表现。

Seed Prover 1.5 针对 FATE-H 问题调用工具示例：

技术报告：https://arxiv.org/abs/2512.17260Lean
证明代码：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip

微信关注我们

原文链接：https://www.oschina.net/news/391801

转载内容版权归作者及来源网站所有！

低调大师中文资讯倾力打造互联网数据资讯、行业资源、电子商务、移动互联网、网络营销平台。持续更新报道IT业界、互联网、市场资讯、驱动更新,是最及时权威的产业资讯及硬件资讯报道平台。

LibreOffice 26.2 不再使用 “Community Edition（社区版）” 品牌名

在即将发布的 LibreOffice 26.2 中，官方决定不再使用“Community Edition”名称来称呼标准版本。之前 LibreOffice 曾试图用 “Personal Edition（个人版）” 命名，但因用户混淆而被否定，后来改为“Community Edition”。“Community Edition” 本意是和商业/企业版本做区分，但这个命名同样造成理解问题，因此董事会决定彻底去掉这类品牌标签。对应的相关代码变更已经合并进 LibreOffice 26.2 开发分支，包括启动画面、版本字符串中删除“Community”字样。该新版计划在 2026 年初（约 1 月底到 2 月初）正式发布。

2025-12-24

7

著名开源开发者 Fabrice Bellard（因 QEMU、TinyCC、FFmpeg 和 QuickJS 等项目而知名）开源了一个全新 JavaScript 引擎：MicroQuickJS，特点是极低的资源占用，专为嵌入式系统和受限内存环境设计。开源地址：https://github.com/bellard/mquickjs 根据介绍，MicroQuickJS（又名 MQuickJS）是一款面向嵌入式系统的 JavaScript 引擎。它仅需 10kB 的 RAM 即可编译和运行 JavaScript 程序。整个引擎（包括 C 库）大约需要 100kB 的 ROM（ARM Thumb-2 代码），其运行速度与 QuickJS 相当。 MQuickJS 支持简化版 JavaScript 语言子集，类似 ES5 范围，但比标准 ES5 更严格，也不包括 JavaScript 中所有现代大型特性，目的是减少运行时内存压力和复杂性。尽管 MQuickJS 与 QuickJS 共享许多代码，但为了减少内存消耗，其内部机制有所不同。具体而言，它依赖于追踪式垃圾回收器，虚拟机不使用 CPU ...

2025-12-24

6

资源下载

更多资源

Mario

马里奥是站在游戏界顶峰的超人气多面角色。马里奥靠吃蘑菇成长，特征是大鼻子、头戴帽子、身穿背带裤，还留着胡子。与他的双胞胎兄弟路易基一起，长年担任任天堂的招牌角色。

Spring

Spring框架（Spring Framework）是由Rod Johnson于2002年提出的开源Java企业级应用框架，旨在通过使用JavaBean替代传统EJB实现方式降低企业级编程开发的复杂性。该框架基于简单性、可测试性和松耦合性设计理念，提供核心容器、应用上下文、数据访问集成等模块，支持整合Hibernate、Struts等第三方框架，其适用范围不仅限于服务器端开发，绝大多数Java应用均可从中受益。

Rocky Linux

Rocky Linux（中文名：洛基）是由Gregory Kurtzer于2020年12月发起的企业级Linux发行版，作为CentOS稳定版停止维护后与RHEL（Red Hat Enterprise Linux）完全兼容的开源替代方案，由社区拥有并管理，支持x86_64、aarch64等架构。其通过重新编译RHEL源代码提供长期稳定性，采用模块化包装和SELinux安全架构，默认包含GNOME桌面环境及XFS文件系统，支持十年生命周期更新。

Sublime Text

Sublime Text具有漂亮的用户界面和强大的功能，例如代码缩略图，Python的插件，代码段等。还可自定义键绑定，菜单和工具栏。Sublime Text 的主要功能包括：拼写检查，书签，完整的 Python API ， Goto 功能，即时项目切换，多选择，多窗口等等。Sublime Text 是一个跨平台的编辑器，同时支持Windows、Linux、Mac OS X等操作系统。