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

微信关注我们

原文链接: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

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

Spring

Spring

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

Sublime Text

Sublime Text

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

WebStorm

WebStorm

WebStorm 是jetbrains公司旗下一款JavaScript 开发工具。目前已经被广大中国JS开发者誉为“Web前端开发神器”、“最强大的HTML5编辑器”、“最智能的JavaScript IDE”等。与IntelliJ IDEA同源,继承了IntelliJ IDEA强大的JS部分的功能。

用户登录
用户注册