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余篇。擔任中國中文信息學會理事，語言與知識計算專業委員會副主任。入選中國科協青年人才托舉計劃、中科院青促會、北京智源青年科學家，獲中國中文信息學會漢王青年創新獎一等獎及科學技術獎一等獎。 

　　“認知啟發的自然語言理解”項目將圍繞語言認知圖譜、語言-知識-情景一體化理解模型、知識自引導學習技術開展研究，聚焦從形式語義到認知語義的突破，探索讓機器真正理解語言的新路徑。