北京
分享至
一个悬了30多年的数学难题，被国产大模型啃下来了。上海人工智能实验室徐迪生团队依托国产"书生S2"科学大模型，通过人机协作，完成了三维Ghys猜想的严格证明。这个猜想此前困扰国际数学界超过30年。
这件事值得拆开看，至少有三个要点。
- 模型是国产的：用的是"书生S2"科学大模型，不是通用聊天模型，定位在科学场景。
- 方式是协作：人机协作完成证明，不是模型单打独斗，人的判断和模型的推演各占一块。
- 验证是独立的：形式化机器验证由北京大学团队完成，证明过程经过了机器层面的核验。
三个环节串起来，构成一条完整的链路：提出问题、给出证明、机器验证。数学证明最怕的就是"看起来对"，形式化验证把这一步堵上了。
科学大模型的价值，往往不在它能聊什么，而在它能不能参与真正没有答案的问题。三维Ghys猜想属于后者——30多年没有严格证明，说明它不是靠算力堆量就能推平的类型。
人机协作这个提法也值得留意。它意味着团队没有把模型当成自动证明机，而是当成推演过程中的一个参与者。这种分工方式，可能比"模型独立证明"更接近当下的真实能力边界。
国产模型在基础科学问题上拿出可验证的结果，这类案例目前还不多。这一次，验证环节也落在了国内团队手里。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
