AI行业动态 - 上智院等联合发布星河启智科学智能开放平台，具备六大核心能力，支持多学科众研和干湿实验闭环[7] - 燧原科技AI算力部署规模达七万卡，推理卡"燧原 S60"支撑互联网客户及智算中心需求[30] AI应用资讯 - 商汤发布悟能具身智能平台，日日新V6.5多模态推理大模型跨模态推理精度超Gemini 2.5 Pro，性价比提升5倍[8] - 华为发布异腾智算平台AI-Box，搭载异腾400I Pro芯片，支持多模态大模型本地运行，适配工业质检等场景[9] - 腾讯发布具身智能开放平台Tairos，提供多模态感知、规划等模型及云服务工具，与硬件厂商合作推动行业落地[10] AI大模型资讯 - 阶跃Step 3模型总参数321B，激活参数38B，推理效率达DeepSeek-R1的300%，2025年预计收入近10亿[11] - 字节开源AI Agent Coze，GitHub星标超6000，支持可视化开发和一键分享至主流平台[14] - 智谱发布GLM-4.5融合大模型，总参355B，激活参32B，API价格低且生成速度快，获全球开源模型第一[17][22] - 京东云开源企业级全栈智能体JoyAgent，支持多智能体协同与并行处理，已应用于零售采销等场景[18] 科技前沿 - 后摩智能发布存算一体端边AI芯片M50，物理算力160TOPS，典型功耗仅10W，支持多模态大模型本地推理[32] - 钛动科技发布全球营销Agent Navos，将传统营销周期从数月缩至几天，提升人力资源效率数十倍[28]

CriticLean 团队 投稿 量子位 | 公众号 QbitAI 当人工智能已经能下围棋、写代码，如何让机器理解并证明数学定理，仍是横亘在科研界的重大难题。 字节跳动Seed团队与南京大学 联合发布 CriticLean 框架，一举将 数学自然语言到Lean 4代码的形式化准确率从38%提升至84%。 该框架创新性地将评估模型置于核心位置。通过强化学习训练的CriticLeanGPT模型，能像数学专家一样精准判断形式化代码是否贴合原始语 义，配合迭代优化机制，让生成的定理证明既符合语法规范，又忠实于数学逻辑。 ⽬前论⽂和数据代码仓库均已对外公开，欢迎开源使用。 数学形式化领域的核心挑战 将自然语言描述的数学命题转化为机器可验证的形式化代码（如Lean 4定理），是自动化定理证明领域的基础性难题，其核心挑战不仅在于 语法层面的准确转换，更在于对数学语义的深度理解与忠实还原。 尽管现有研究在生成模型与编译有效性上取得一定进展，但在复杂问题的语义对齐上仍存在显著瓶颈，具体体现在以下三方面： 语义鸿沟： 引入Critic角色以实现可靠形式化 上述挑战的核心在于：形式化流程中"评价"与"生成"的割裂。 CriticL ...