阶跃星辰发布 StepFun-Prover-Preview 系列模型，用于形式化定理证明-低调大师

阶跃星辰发布 StepFun-Prover-Preview 系列模型，用于形式化定理证明

2025-08-14 256

阶跃星辰（StepFun）发布了 StepFun-Prover-Preview 系列模型，包括 7B 和 32B 两个版本，专门用于形式化定理证明（formal theorem proving）。

据介绍，StepFun-Prover-Preview 专为数学推理设计，通过工具集成推理（tool-integrated reasoning）实现高效的形式化定理证明，支持 Lean 4 证明语言。

论文地址：https://arxiv.org/abs/2507.20199

性能方面，StepFun-Prover-Preview-7B 在 miniF2F-test (pass@1) 基准测试中，其表现与 DeepSeek-Prover-V2-671B 和 Kimina-Prover-72B 持平。更强大的 StepFun-Prover-Preview-32B 模型在 miniF2F-test (pass@1) 上超越了所有已知同类模型 4% 以上。该系列模型还具备类人证明细化能力，非常适合推动数学推理领域研究的科研人员。

模型地址：https://huggingface.co/stepfun-ai/StepFun-Prover-Preview-32B

微信关注我们

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

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

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

FileZilla Server 1.11.0-rc1 发布

FileZilla Server 是一个免费开源的 FTP 和 FTPS 服务器，能够提供与服务器的安全加密连接。 FileZilla Server 1.11.0-rc1 现已发布，更新内容如下：新功能：支持挂载点的“只写”模式。向服务器添加了--version 选项。 FTP：在 LIST、NLST、MLSD 和 STAT 命令中新增了对通配符模式（“*”和“?”）的支持，其匹配语义与 Windows 上的相同。此功能适用于所有平台，默认禁用。可以使用“OPTS filezilla.wildcards=1”为每个会话启用此功能；FEAT 命令已启用此功能。有关匹配行为的参考信息，参阅：https://learn.microsoft.com/en-us/archive/blogs/jeremykuhne/wildcards-in-windows MSW：添加了在挂载列表中指定 UNC 路径凭据的支持。凭据可通过管理界面的 Rights Management -> Windows Share Credentials 进行配置。错误修复和细微更改：修复了路径规范化中的edg...

2025-08-15

155

Editor Code Assistant(ECA) - 人工智能结对编程功能，不受编辑器限制。旨在轻松连接 LLM 和编辑器，并通过定义明确的协议为 AI 结对编程提供最佳的用户体验。服务器采用 Clojure 编写，并深受LSP 协议的启发，LSP 协议是此类集成的一个成功案例。该协议使其他编辑器更容易集成，并且在中间有一个服务器有助于快速添加更多功能，以下是一些示例：工具调用管理多LLM互动功能使用情况遥测为任何编辑器配置的单一方法相同的用户体验，易于人员和团队加入。与编辑器无关：适合任何编辑器集成的协议。单一配置：通过全局或本地配置配置 eca，使其在任何编辑器中都能正常工作。聊天界面：提出问题、审查代码、共同编写代码。 Agentic：让 LLM 使用其原生工具和你可以配置的 MCP 作为代理工作。背景：支持：向 LLM 提供有关你的代码的更多详细信息，包括 MCP 资源和提示。多模型：OpenAI、Anthropic、Ollama 本地模型和自定义用户配置模型。使用eca-emacs 的演示使用eca-vscode 的演示

2025-08-14

204

资源下载

更多资源

优质分享App

近一个月的开发和优化，本站点的第一个app全新上线。该app采用极致压缩，本体才4.36MB。系统里面做了大量数据访问、缓存优化。方便用户在手机上查看文章。后续会推出HarmonyOS的适配版本。

Mario

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

腾讯云软件源

为解决软件依赖安装时官方源访问速度慢的问题，腾讯云为一些软件搭建了缓存服务。您可以通过使用腾讯云软件源站来提升依赖包的安装速度。为了方便用户自由搭建服务架构，目前腾讯云软件源站支持公网访问和内网访问。

Rocky Linux

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