今天(7 月 21 日),以太坊联合创始人维塔利克·布特林提出创建一种新的高层编程语言。该语言可编译到诸如 Lean 和 HOL 之类的形式化证明系统,从而优化定义与定理的可读性,而非证明过程本身。根据 PANews,布特林表示,该语言旨在帮助人类清楚理解 AI 生成的大规模形式化证明在数学与逻辑层面所展示的内容,使读者能够更容易地审计并核实 AI 所提出的具体主张。
据格隆汇,中国首个合规具身 AI 数据平台由上海技术交易所、科兴时空技术以及优必选机器人联合开发,于 7 月 21 日正式开始运营。该平台定位为面向全球研究机构的国家首个具身 AI 数据基础设施,并从一开始就实施全流程合规管理。它借助优必选在机器人运动控制与场景适配方面的专长,提升数据采集的质量与用于模型训练的覆盖范围。该平台在上海网信主管部门指导下开展端到端的合规监测,并融合电子数据鉴证与权益登记机制,将具身 AI 数据确立为标准化、可交易的知识产权资产。