首页 文章 精选 留言 我的
优秀的个人博客,低调大师

微信关注我们

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

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

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

微软开源“原生 1-bit”模型:超过 20 亿参数、大幅减少内存占用

微软近日发布了20亿参数的1-bit模型——BitNet b1.58 LLM家族,称此新型模型比主流Transformer LLM更不占内存且更低能耗,适合在CPU或较小型硬件平台上执行。 Hugging Face 地址:https://huggingface.co/microsoft/bitnet-b1.58-2B-4T 微软研究院与中国科学院研究人员2023年发布名为《BitNet: Scaling 1-bit Transformers for Large Language Models》的论文,首度发布为大语言模型设计的1-bit Transformer架构,称为BitNet。 https://arxiv.org/pdf/2310.11453 微软表示,这是第一个参数20亿的开源原生1-bit LLM。它是以4兆字词的数据集训练而成,具备4096 token的context length。 研究团队说明,在BitNet b1.58模型中,单一参数或权重是三元( {-1, 0, 1})的。此类新模型架构引入BitLinear作为nn.Linear层的替代,能够训练1-bit的权重,...

Verus —— 用于验证 Rust 代码正确性的工具

Verus 是一款用于验证 Rust 代码正确性的工具。开发者编写代码功能规范,Verus 会静态检查可执行的 Rust 代码是否始终满足所有可能执行场景下的规范。 Verus 并非添加运行时检查,而是依靠强大的求解器来验证代码的正确性。Verus 目前支持 Rust 的一个子集(开发团队正在努力扩展),在某些情况下,它允许开发者超越标准 Rust 类型系统,静态检查代码的正确性,例如操作原始指针的代码。 Verus 的目标是: 提供纯数学语言来表达规范(如 Dafny、Creusot、F*、Coq、Isabelle/HOL) 提供一种基于经典逻辑(如 Dafny)的数学语言来表达证明(如 Dafny、F*、Coq、Isabelle/HOL) 提供一种基于 Rust(如 Prusti、Creusot 和 Aeneas)的低级、命令式语言来表达可执行代码(如 VCC) 根据以下原则, 生成小型、简单的验证条件,以便Z3等 SMT 求解器能够有效地解决这些条件: 使数学规范语言接近 SMT 求解器的数学语言(如 Boogie) 使用轻量级线性类型检查(而不是 SMT 求解)来推理内存和别名...

相关文章

发表评论

资源下载

更多资源
Mario

Mario

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

腾讯云软件源

腾讯云软件源

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

Nacos

Nacos

Nacos /nɑ:kəʊs/ 是 Dynamic Naming and Configuration Service 的首字母简称,一个易于构建 AI Agent 应用的动态服务发现、配置管理和AI智能体管理平台。Nacos 致力于帮助您发现、配置和管理微服务及AI智能体应用。Nacos 提供了一组简单易用的特性集,帮助您快速实现动态服务发现、服务配置、服务元数据、流量管理。Nacos 帮助您更敏捷和容易地构建、交付和管理微服务平台。

Rocky Linux

Rocky Linux

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