8月18日，国家自然科学基金委公布了2021年国家自然科学基金评审结果，我所张健研究员申报的“面向形式化验证的可信编译和程序分析”项目获得重点项目资助，蔡少伟研究员申报的“可满足性问题求解”项目和韩先培研究员申报的“认知启发的自然语言理解”项目获得优秀青年科学基金项目资助。 

　　张健研究员长期从事自动推理、约束求解、程序静态分析与检错、软件测试数据生成等研究工作，担任《中国科学：信息科学》、《计算机学报》、《Journal of Computer Science and Technology》、《Frontiers of Computer Science》、《IEEE Transactions on Reliability》等期刊编委，先后获得中国科学院青年科学家奖、中创软件人才奖、国家杰出青年科学基金、王选新闻科学技术奖一等奖等，享受国务院政府特殊津贴。 

　　“面向形式化验证的可信编译和程序分析”项目将围绕程序分析和加固技术的验证、语义增强的程序分析、面向形式验证的程序化简、形式规约的检查等方面开展研究。 

　　蔡少伟研究员长期从事约束求解和组合优化研究，发表CCF A类论文40余篇，有7篇论文发表在AIJ上，在SAT（命题逻辑可满足性）、SMT（可满足性模理论）和MaxSAT（最大可满足性）比赛多次获得冠军，获得SAT会议最佳论文奖，发起了IJCAI workshop “ Heuristic Search in Industries”并担任程序委员会主席。成果在华为芯片验证项目、腾讯地图优化、 微软云平台故障检测与优化、美联邦通讯委员会频谱分配等重要项目得到了应用，入选北京智源青年科学家。 

　　“可满足性问题求解”项目将围绕表达能力更丰富的逻辑公式可满足性问题的算法开展研究，致力于大规模和复杂理论的SMT公式的判定与优化。 

　　韩先培研究员长期从事知识驱动的自然语言理解研究，包括信息抽取、知识图谱、语义解析以及智能问答系统。承担和参与中科院战略先导、AI 2030、自科重点、国家重点研发专项等十余项课题。在ACL、SIGIR、IJCAI、AAAI等重要国际会议发表论文60余篇。担任中国中文信息学会理事，语言与知识计算专业委员会副主任。入选中国科协青年人才托举计划、中科院青促会、北京智源青年科学家，获中国中文信息学会汉王青年创新奖一等奖及科学技术奖一等奖。 

　　“认知启发的自然语言理解”项目将围绕语言认知图谱、语言-知识-情景一体化理解模型、知识自引导学习技术开展研究，聚焦从形式语义到认知语义的突破，探索让机器真正理解语言的新路径。