赴德心得体会分享

 本次分享的是来自于李建霖师兄的赴德学习交流的经验和心得体会。

 

一、第一年在国内

1、取得的相关成绩

       在2018-2019学年,我作为一年级学生主要在雁栖湖进行课程学习,均分90.31分,在2018级硕士中排名第二名,与研究方向相关的科目取得了比较好的成绩,如,高等分析基础99分,形式语言与自动机理论98分,形式化方法 96 分。
       在刚开学作为志愿者参与了实验室举办的CONFEST 大会的服务、摄影和新媒体(微信推送)宣传工作。同时我参与的文章也被大会接收并且在现场进行了报告。在研究生一年级期间我和同课题组杨鹏飞师兄在导师张立军老师的指导下与国防科大刘江潮老师、陈立前老师展开合作,我们使用抽象解释的方法对神经网络局部鲁棒性的验证问题展开了研究,我们在现有的方法中引入了符号传播技术,取得了一些理论成果并实现了一个验证工具称为DeepSymbol,文章《Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification》被SAS 2019接收。
       除了课程学习和科研工作,在业余时间我积极参与校园文化活动,在国科大宣传部记者团作为摄影记者参与了开学典礼、四十周年校区等活动的新闻报道工作,有多幅照片刊登在校刊的彩页和正文中。作为国科大官方微信公众号影像部的成员参与了考研加油 MV 的拍摄,主要负责摄像工作,成片推送《国科大班夜空中最亮的星,送给为梦想冲刺的你》阅读量达2.3万,参与摄影作品供稿和后期设计制作国科大专属电脑手机壁纸,两篇推送累计阅读量约2万,壁纸受到同学们的好评。在2018至2019广场跨年活动中,在中国青年报·中青在线网站直播中担任出境记者对直播观众进行活动介绍,采访校园内的同学,展现了国科大学生的风采。

2、文章和荣誉称号

  • 《Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification》(第一作者)被 SAS 2019接收(CCF-B)。
  • 《Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties》(第三作者,通讯作者)被QEST 2018接收。
  • 2018-2019学年中国科学院大学“三好学生”、“优秀共青团员”。
  • 2018-2019学年中国科学院大学党委宣传部国科大记者团“优秀摄影记者”。

3、课程成绩:

二、出国手续的大概流程

        我们去德国最初的计划是访问一年,申请了学术访问签证。签证的申请说明详见“德国大使馆网站首页 > 服务>签证和入境>长期停留>文件下载区>就业、互惠生、实习和志愿服务>学术访问(研究)签证申请须知”。当时从上海同去的同学搞不清楚状况,她还咨询了APS和其他签证类型,导致她浪费了一些时间和精力。整个过程中要做的第一件事是尽快在大使馆预约排队递交签证,尤其是暑假前有大量留学生申请签证,大使馆会比较繁忙,预约排队也比较长。我是2019年7月17日在网上预约到了2019年9月16日08:00到大使馆递交签证。中间有两个月的时间用来准备签证材料,非常充足。
 准备签证材料主要分两个方面,一个是准备好提交给大使馆的文件(前面提到的签证申请须知中有清淡),一个是在所内提交出访申请。在所内办理出访申请的过程中就会获得一些申请签证所需要的问题(比如所里开具的资金支持证明和软件所的事业单位法人证书复印件)。出访申请表见软件所官方网站“首页>研究生教育>下载区>研究生(博士后)公派出国(境)审批表”。这个表格内容不多,填表时注意两点。第一是预算不要算少了。第二是尽早提交,因为研究生部和所领导都要签字,能签字的老师不一定在办公室,有时候需要放到办公室等签好字再去取,还要去科技处领资金支持证明和软件所的事业单位法人证书复印件。提交给大使馆的材料中,首先要处理的Hosting Agreement和邀请信,Hosting Agreement表格是申请人自己填完能填的内容后给德方,德方导师签字后和邀请信一起邮寄纸质版来中国,然后我们申请人提交原件和复印件给大使馆。剩下的材料都是自己准备的。签证申请表可以用德文和英文填写,我用英文填的。我的本科毕业证、学位证、研究生在学证明、从所里领的资金证明和法人证复印件需要翻译成英文和德文,师兄是自己中译英,用谷歌翻译英译德,然后找David帮忙校对了,我是找了淘宝翻译,翻译质量也不高,我用谷歌翻译英译德和德译英校对了一下。

三、萨尔大学注册,分数认定流程及注意事项:

 
       萨尔大学注册不是很麻烦,出发前按照学校的邮件在系统中上传身份信息和照片,到德国后去学校欢迎中心会有工作人员详细介绍,工作人员会帮忙指路一个银行,去银行办一个汇款交两百多欧的学期费。校园卡大概要等一周到两周,只能本人来欢迎中心取,学期费是包含公交票的,拿到校园卡就可以凭卡在萨尔州内免费乘坐公共交通了。
       萨尔大学的硕士学位需要 120 个CP (course point)。详细的培养计划在谷歌搜索“Saarland University Study Rregulations”。(http://www.ps-ntf.uni-saarland.de/fileadmin/user_upload/_imported/fileadmin/Benutzerdaten/Downloads/Formulare/Informatik/StO_PO/StO_MA_Informatik_2015_en_komplett.pdf)。其中包括7CP的seminar、12CP的硕士毕业论文seminar和30CP 的毕业论文。剩下的71个学分就是需要按照培养计划主要选修Core lecture(每个9CP)和 Advanced lecture (每个6CP) 来完成。
        因为认定学分认定成Advanced lecture比较容易,而且培养计划要求至少选三门Core lecture,所以选课上课尽量先选择Core lecture,我在萨尔大学选修了三个Core lecture,包括Automated Reasoning,Introduction to Computational Logic 和 Semantics。一个Advanced lecture叫做Constructive Theory of Computation。Automated Reasoning 课程没什么特色,比较像国内的数理逻辑课程加入了关于CDCL, resolution, tableaux和rewriting的内容。Semantics实际上讲的是lambda 演算(从无类型到 System F)和semantic typing, 这些内容非常有特色,在国内应该非常难找到类似的课程。Introduction to Computational Logic这个课程理论上是在讲构造主义的类型论,编程是在教交互式定理证明器,写 Coq代码,这个课程让我从编程中深刻而直观的体会到了逻辑和编程的联系(柯里霍华德对应,即函数的类型相当于命题,函数的实现相当于证明)。这两个课程解答了一个困扰了我多年的问题。我之前知道lambda演算发展的历史,是阿隆佐·邱奇先提出了无类型lambda演算,但是这个演算有不终止的项,所以不协调。为了解决这个问题又提出了更弱的简单类型 lambda 演算。但是我许多年了都不理解协调这个讲逻辑系统的词,为什么用来形容无类型 lambda 演算,更不理解为什么不终止和不协调有联系。在这两门课里,柯里霍华德对应回答了第一个问题,一个在带递归类型的演算中定义不动点算子的练习题回答了第二个问题。有了不动点算子,我们可以定义一个函数,接受unit type的参数,返回empty type 的返回值,这个函数的定义是简单地不终止调用自己,而这就是一个True蕴含False的证明。
        学分认定的流程因为这是我们第一次比较而复杂,由于我想要兑换的学分太多,而且国科大和萨尔大学使用的学分规格不同,这对萨尔大学来说也是比较少见的一个情况,所以经过Holger帮忙协调,我们最后终于争取到了这样的结果:首先我要在萨尔大学正常修读一个学期,并且在期末考试中表现优秀,证明我有能力在萨尔大学完成学业。然后Holger作为萨尔大学的教授,帮我写一封推荐信提交到萨尔大学计算机系,系里讨论同意后才能进入常规的认定流程,以国科大一个学分认定为萨尔大学两个CP的比例进行认定。这里值得注意的一点是我选修的课程中有三门是smolka负责的,而smolka在系里担任的工作会让他参与这个是否同意兑换学分决定,所以在这三门的考试中取得好的成绩是很重要的。
        当兑换学分进入常规流程后就变得非常漫长,我需要向系里提交学分认定申请表,里面写明了我希望认定的在国科大修读课程的课时数、学分等关键信息。并且需要额外提交一个Modulhandbuch(module description)写明课程的修读要求、课程内容和考核要求等详细信息。这个是我自己从国科大 SEP 网站选课系统收集了中文版约两万两千字,然后自己翻译成英文(约六千词)。我2020年8月7日提交了这两个材料,然后秘书安排教授审核这些材料,到2021年1月21日,这个流程依旧没有完成,不过秘书反馈只剩一个审核结果没有提交,秘书有信心本学期内(2021年3月31日前)完成全部手续。

四、德方导师及课题:

     在德国我参与了Holger负责的CPEC项目,跟MPI-SWS的Maria Christakis小组合作,模拟的方式探索在含有深度神经网络的的软件系统的安全性性质验证。我们案例学习的对象叫做Race Track,是一个含有深度神经网络的模拟小车控制器C程序。含有的神经网络是通过强化学习方法得到的,我们正在结合基于抽象解释的程序验证框架Crab和神经网络的验证工具去进行验证。这个工作投稿TACAS 2021收到的评审意见分歧较大(一个2分一个-2分),最终被拒稿。现在修过后已经投稿CAV 2021等待评审。