作者:胡珉琦 来源: 中国科学报 发布时间:2023-1-19
选择字号:
少数者蔡少伟:孤独只是别人眼中的我

 

蔡少伟   软件所供图

■本报记者 胡珉琦

少数者

“我不怕坐冷板凳,怕的是连板凳都没有了。”这是国内约束求解研究人员的一句自嘲。

求解器研究者、中科院软件研究所(以下简称软件所)研究员蔡少伟第一次感觉到自己开始“出圈”是在2020年——不是因为他的团队频频在约束求解领域布尔可满足性问题(SAT)国际竞赛中拿到重量级冠军,而是因为华为芯片断供,“卡脖子”问题倒逼攻坚。

芯片领域的一些会议、项目咨询纷纷向他发出邀请。但每一次他都会诚实地告诉对方,他的研究领域距解决目前的工业挑战还有很长一段距离。

芯片制造过程是一个漫长的链条,越靠近链条前端,问题越基础、越隐蔽。

2022年8月,美国宣布对GAAFET(全栅场效应晶体管)架构集成电路所必需的EDA软件实施出口管制,引发舆论关注。因为作为重要工业软件之一的EDA软件,掌握着芯片设计的命门。

其实,不仅是芯片,在操作系统、航空航天、能源、制造业等对精确度要求很高的核心工业领域,工业软件充当“大脑”的角色,而工业软件的核心就是各种求解器,它好比引擎之于汽车一样重要。

从本质上说,约束求解是数理逻辑的根本性问题,而数理逻辑又是整座数学大厦的根基,所以,约束求解研究者就是一群守在科学基座上的人。

可在国内,从约束求解器到工业软件,都严重依赖进口。直到近两年,华为、阿里等企业才开始布局求解器研究。

2022年4至6月,蔡少伟组织举办了36课时的“约束求解基础与应用”训练营,吸引了来自高校和企业的200多人报名,仅华为就来了近30人。

2012年,当时在北京大学攻读博士的蔡少伟参加了SAT国际竞赛,拿到了属于中国人的首个冠军,且把第二名远远甩在身后。在欧美学者眼中,这无异于“横空出世”,可到了国内,却悄无声息。因为那时,国内专门从事约束求解研究的学者一只手就数得过来。

这个底层的、隐性的基础科研问题,在国内天生与热点绝缘,这就意味着,科研人员申请相关项目、发表论文都十分不易。

过去十几年里,也有来自北京航空航天大学、西南交通大学、华中科技大学、东华大学的同行者,但来来往往,最终只有蔡少伟坚持了下来。

浪漫瞬间

用的人多,做的人少,是因为求解器研究的高门槛。

约束求解的一个核心问题是SAT,其本质是探求布尔变元之间的逻辑推理关系是否成立。蔡少伟经常举一个例子——甲、乙、丙想参会,甲说:乙参会我就参会,乙说:丙参会我就参会,而丙说:甲参会我就不参会,那么能不能同时满足甲乙丙的参会需求?

这就是一个典型的SAT问题,求解的答案是——他们的需求不可同时满足。

但是,在现实工业领域,命题要复杂得多,无法通过人脑来判定逻辑推理关系是否成立。随着布尔变元和约束的条件越来越多,SAT的求解就必须借助算法来进行推理与计算。

蔡少伟说,约束求解是一个古老的命题,可以追溯到图灵时期。它发展至今,传统的、简单的算法已经被许多外国学者研究过,剩下的全是“硬骨头”。

“它就像百米赛跑,100米谁都能跑,但要想打破世界纪录就非常困难了。”这意味着,研究者必须拿出更优的算法,从而提升求解效率。

从事约束求解研究,要求兼具很强的数理逻辑和编程能力。蔡少伟自认并不是天才型选手,两方面的表现都不惊艳,但胜在均衡且扎实。

2006年,在华南理工大学计算机科学与技术专业读大二的他,受到班主任王家兵的启蒙,开始接触约束求解问题。两年后,他直博北大,正式确立了自己的研究领域,他也是同届学生中唯一选择这个方向的。

当时,同伴们都在拼命做研究、发论文,蔡少伟却不疾不徐,认认真真学好每一门课。而且高中时曾立志成为作家的他,从不间断阅读。

蔡少伟有个习惯,只要感觉在学业上有所进步,他就奖励自己一本喜欢的书,宿舍书柜里很快便积累了各种书——文学、数学、哲学……什么类型都有。

在SAT中,随机搜索是一种主要方法,而它面临的瓶颈就是如何克服搜索过程中的循环现象。蔡少伟觉得,采用传统数理逻辑的分析思维怎么也走不通。

一次,他翻看一本社会学通识书籍《社会学与生活》,里面谈到了群体环境对个体是如何产生影响的。当时,他的大脑就像过电一般,顿时联想到了搜索变量与环境信息之间的关系问题。

之后几天,蔡少伟不断琢磨两者的联系,却总是答案呼之欲出,只欠“东风”。

不久,法国华人教授李初民来北大作了一个报告,席间蔡少伟突然看到报告PPT上的几个单词,那似乎是来提醒他的,顿时那个日夜思索的方法就“自己冒了出来”。

“世界突然安静了,只有笔尖和纸张摩擦的声音,我飞快地写着,很怕是个幻觉,会马上消失。”蔡少伟记录下了当时的灵光一闪。

正是这一浪漫瞬间,帮助他交出了博士阶段最满意的作品——格局检测策略。通过避免局部结构循环减少无用搜索,大大提高了求解效率。

2011年,他的这一成果登上了《人工智能期刊》,并首次出现在美国举行的SAT会议上。作为全场唯一的中国人,大会主席主动和他打招呼。在后来的其他会议上,他也感受到了多位专家的热情。

“因为你生了一个金蛋,大家就都对这只母鸡产生兴趣了。”蔡少伟打趣道。

但他并未在成果上过多停留,开始反思孕育成果的过程,在科学方法以外,直觉、悟性都在潜移默化影响着他,“这是很根本性的东西”。

从一个难题到另一个难题

除了随机搜索外,SAT还有一种基于系统搜索和证明的方法,这也是最主流的SAT方法。然而,蔡少伟很快发现,无论哪种方法,想要改进它们,都存在边际效应递减的问题,且越坚持越容易走入死胡同。这也反映了科学研究中的轨迹依赖。

“必须跳出旧有框架,远观它、质疑它、批判它。”蔡少伟是这么想的,也是这么做的。

早在1997年,国际先进人工智能协会主席Bart Selman就指出过随机搜索和系统搜索各自的优缺点,在他提出的命题逻辑推理与搜索的十大挑战中,第七个挑战就是结合两种方法的优势设计出更好的方法。

博士阶段,蔡少伟曾花了半年时间思考这一问题,想累了就去看书,转换思维和视角,希望有所启发。“回想起那时候,我还挺幸福的,虽然研究上没什么突破,但我始终在探索一个自己认为值得的问题。”

而接下来的“剧情”并没有发生预期的转折,事实上,蔡少伟选择了放弃。

“我可以在原方法上做一些改进,不断累积,也能写出几篇不错的论文,但结果可能是我的论文越写越窄,这就跟我最初跳出原有方法路径的想法南辕北辙了。”在他看来,这样的研究一点也不酷。

因此,与其说是放弃,不如说是搁置。好的研究需要酝酿。

2012年,蔡少伟赴澳大利亚格里菲斯大学攻读第二个博士学位。但现实与理想的差距让他过上了被放养的生活。其间,他把车库改造成了实验室,独自一人在SAT方向上扎下根来。

“要说我个人经历中唯一的遗憾,可能就是我从来没有在一位大师手下贴身学习、成长过。”蔡少伟形容自己就是个“土娃”,只能靠自己摸爬滚打,“我也希望‘高山仰止’,但没机会”。

不过,事物都有两面性。没有“高山”压顶,给了蔡少伟最大程度的自由,也练就了他对一项研究的判断力和掌控力。一个人能活成一支队伍,那么未来当队伍真正出现时,他就有足够的信心和魄力带领好这支队伍。

2014年,蔡少伟回国加盟软件所,正式在研究所开辟了约束求解方向,并在4年后重启了对那个十大挑战之一的难题的探索。

2021年,他带领学生提出了基于CDCL求解结合局部搜索采样的混合求解方法,终于让系统搜索与随机搜索完美合流。这一成果拿下了SAT 2021最佳论文奖。这是SAT会议自1996年设立以来,中国论文第一次获奖。

“我们做科研,无非是两个方向,要么改变对世界的认知,要么改变这个世界的现状。”

近年来,除了SAT外,蔡少伟开始着眼于SMT,该问题是限定背景理论的一阶逻辑公式判定问题。相较于前者,SMT求解更前沿也更具挑战性,在国内几乎无人问津。

事实上,尽管过去的2021—2022年,蔡少伟团队在SAT的一系列重要国际竞赛中一马当先,但真正让他兴奋的是团队设计了首个支持线性整数算术的SMT随机搜索算法LS-LIA。基于该方法,团队大幅度改进了著名求解器Z3,新求解器Z3++击败了来自美国斯坦福大学和微软研究院的顶级团队,在近两年SMT国际竞赛中都获得了金牌,这也是国内首个冠军。

从一个难题到另一个难题,蔡少伟没有任何犹豫。

“我的世界很丰富”

张昕荻是蔡少伟团队SAT 2021最佳论文的另一位作者,也是这些年竞赛团队的主要成员。

“跟着我,发论文可能比较困难,到时候可别羡慕其他同学。”2017年,还是吉林大学大三学生的张昕荻第一次见到蔡少伟,就被打了预防针。

张昕荻的同班同学大部分选择了一些与人工智能相关的热门方向,可他却避开人群,甚至为此放弃了去清华大学深造的机会。

之后,从研究生正式入学到发表他的第一篇SAT论文,整整过了4年。要不是转博,都赶不上顺利毕业。

同学、朋友圈里,一年发几篇好文章的年轻人大有人在,张昕荻承认,不羡慕是假的。“但导师总是告诉我们,有些难题,在国内没有人能帮我们,只能靠我们自己一点一点啃下来 。”

要么不做,要做就要一鸣惊人。这样的张昕荻多像十几年前那个独自亮相SAT会议的蔡少伟。

现在看来,在蔡少伟身上,孤独更像是一种祝福,不过他并不想把这种祝福传递给学生。

“我曾经一个人走了很久,其间踩过多少坑只有自己知道。我只是在某些交叉路口很幸运地走对了,或者在某些重要节点得到了一些机遇。”蔡少伟相信,单打独斗是走不远的。

“特别是当国内的这一研究力量还很弱小时,更需要年轻人保持队形,集智聚众攻关。这时候,走一个骨干,一个方向可能就断了。”这也是他现阶段的最大隐忧。

因此,出于对这群少数者的保护和“偏爱”,软件所一直以来都在帮助蔡少伟课题组争取最有竞争力的条件,好让他们的生活没有后顾之忧。

至于蔡少伟自己,至今无房无车。妻子偶尔也会因此向他提出“抗议”,“但我只要有足够的时间陪她散散步,思想工作一准成功”。

新的一年,蔡少伟点赞了一条微博:生命的意义本不在向外的寻取,而在向内的建立——来自史铁生的《病隙碎笔》。

对蔡少伟而言,他的内在世界早已落成,让它变得坚固且恒久的,是低音炮里流淌的音乐,是鲁迅、罗素、茨威格笔下的文字,是让人平心静气的一盏清茶,是偶尔沉醉的一杯小酒……

“我的世界很丰富。”蔡少伟不止一次提到。孤独,也许只是别人眼中的样子 。

《中国科学报》 (2023-01-19 第4版 人物)
 
 打印  发E-mail给: 
    
 
相关新闻 相关论文

图片新闻
应激颗粒异常是导致周围神经病的重要机制 “中山大学极地”号顺利完成渤海冰区试航
AI技术从零开始生成原始蛋白质 科学家模拟出末态粒子关联的三维结构
>>更多
 
一周新闻排行
 
编辑部推荐博文