ACM通信
2013首届海德堡桂冠论坛
海德堡桂冠论坛允许来自世界各地的200名研究人员与计算机科学和数学领域最负盛名的奖项的桂冠获得者见面并互动。
信贷:HLFF
我你真的很幸运能在海德堡桂冠论坛(HLF) 2013在那里，200名年轻的研究人员将与40名研究人员见面并向他们学习图灵奖，菲尔兹奖，阿贝尔奖而且Nevanlinna奖2013年9月22日至27日为期一整周。并不是每天都这样40位数学和计算机科学领域最优秀的人才聚集在一个地方，不仅要发表关于深奥技术的演讲，关于计算和数学的未来，还要讲授“如何做研究”。
能见到所有的获奖者并聆听他们的演讲真的是一种令人谦卑的经历。让我印象最深的是他们都是那么平易近人。
论坛的目的是通过与聚集在美丽而迷人的校园里的40位获奖者的互动来激励年轻的研究人员海德堡大学．这当然是鼓舞人心的。在许多方面，这个论坛是模仿朗道诺贝尔奖得主会议把诺贝尔奖得主和年轻的研究人员联系起来。
2013年9月22日，周日:颁奖前的介绍，欢迎和乐队：
HLF活动于2013年9月22日周日开始，首先是对获奖者的正式介绍，然后是年轻研究人员和获奖者之间的非正式交流，最后以一场音乐剧结束，这出音乐剧提出了一个极具挑衅意味的问题:“计算机是否能够擅长制作音乐这样需要品味、创造力和情感的任务?”整个演出是德语的，背景音乐是管弦乐队演奏莫扎特的作品。故事有两个主角，一男一女。男人认为电脑无法创造出莫扎特那样的崇高音乐，而女人则极力主张电脑能够创造出伟大的音乐。为了证明她的观点，她演示了一个程序，该程序将观众挑选的莫扎特音乐片段随机拼接在一起，听起来像，嗯，莫扎特。她还对男主角进行了“图灵测试”，问题是“以下是一位专业钢琴家演奏的两首曲子。告诉我们哪一首是莫扎特写的，哪一首是电脑写的?”显然，两者都是计算机生成的。
在我未经训练的耳朵看来，所有电脑合成的音乐听起来和我听过的任何作曲家一样好。
2013年9月23日星期一:第一天讲座(计算机科学)：
拉杰·雷迪关于“谁发明了计算机?”
教授Reddy(图灵奖)，他对从莱布尼茨到图灵的计算机历史进行了精彩的描述。他给出了一个非常全面的多维标准来判定谁发明了“我们今天所知道的”计算机。标准包括诸如“某人X是否第一次设计了通用可编程设计”，“他们的设计是否包含了存储程序的想法”，“它是否具有跳跃和条件分支”，以及“发明者是否真的设法构建了一个原型”(巴贝奇在这一点上被排除了)。
进入决赛的有图灵、冯·诺伊曼、祖斯、巴贝奇和阿塔那索夫。最后的赢家是图灵，他的ACE计算机设计满足了所有要求(通用、存储程序、迭代和分支、RISC体系结构和实际原型)。约翰·冯·诺伊曼(John Von Neumann)的EDVAC原型紧随其后。
Curtis T. McMullen关于“模空间中的台球”的演讲(数学)
来自哈佛大学的麦克马伦教授(菲尔兹奖牌获得者)做了一个关于预测台球在无摩擦的表面上如何(永远地)反弹，当台球桌呈现出奇怪的形状时，会产生非常有趣的图案。因为我不是这方面的数学专家，所以我在这里没什么可说的。然而，让我着迷的是他使用计算机程序来发现不寻常的结构和模式。这是计算机程序在数学中用于寻找模式、反例猜想和证明定理的应用越来越多但并不为人所知的一个实例。
Steve Smale关于蛋白质折叠问题的演讲(数学)
史蒂夫·斯梅尔(菲尔兹奖牌获得者)，来自香港城市大学和伯克利分校，介绍了蛋白质折叠问题背后的数学原理，以及他的团队如何开发出获奖算法，可以预测蛋白质的折叠。问题是“从代表蛋白质中氨基酸的字母序列开始，你能预测蛋白质的最终3D结构吗?”建模这个问题所需的数学可能没有那么复杂，但提出有效的算法及其实现是非常重要的。
埃德•克拉克“模型检验与维数的诅咒”讲座(计算机科学)
来自CMU的Ed Clarke(图灵奖)做了一场精彩的演讲，主题是根据定义良好的规范来验证计算机程序的正确性模型检查．这个主题非常贴近我的心，因为我从事的是形式化方法，这个领域致力于通过模型检查器、定理证明器、类型检查器和基于编程语言的验证方法，根据逻辑规范半自动地验证程序的正确性。
模型检查(由Clarke、Emerson、Sifakis和Quille发明)是一种检查以状态转换系统表示的程序是否符合某些类型的属性的技术。Ed描述了使模型检查成功的核心思想:1)符号模型检查，2)有界模型检查，3)反例指导的抽象细化(CEGAR)， 4)高效的SAT和SMT求解器。
考虑到我从事SAT/SMT求解器的工作，看到它们对形式化方法和软件工程的影响得到认可是令人鼓舞的。
在许多会谈、非正式讨论和小组讨论中反复出现的一个问题是“计算机能做真正的数学吗?”这个问题是在验证程序正确性的正式方法的背景下直接提出的(我稍后会讨论这个问题)。
莱斯利勇敢的“学习是生活现象的根源”讲座
来自哈佛的Leslie Valiant(图灵奖获得者)第一天的演讲可能是最有趣的，关于如何应用计算学习理论来“解释进化”。他提出的问题是，如果你简单地假设一个达尔文的随机突变和适者生存的模型，它无法解释进化是如何在“仅仅”40亿年里发生的(宇宙本身被认为大约有137亿年的历史)。Valiant认为，达尔文的理论只是一个大纲，并不是一个具有精确数学描述和预测能力的物理理论。
为了将一个问题定义为机器学习问题，我们必须有一个目标函数。Valiant提出，在这种情况下，目标函数是一个“理想函数”，它表明在任何可能的环境条件下的最佳行为(正在学习的电路的输出)。T生命进化有多快的问题现在可以用复杂性理论来分析，我们可以问代表“适者生存”的目标函数是否可以“容易学习”。
第一天的小组讨论:Shafi Goldwasser, Leslie Valiant, Ed Feigenbaum, Alan Kay, Butler Lampson和John Hopcroft(都是计算机科学奖得主)
小组讨论非常鼓舞人心，涉及的问题/主题包括“如何进行研究”(Ed Feigenbaum)、“计算机能否被用来构造数学证明”(Lampson和Shafi)、“工程师和数学家对可证明密码的进化和接受”(Shafi)。
对我来说，最精彩的部分是“计算机辅助”数学证明，这似乎是一个反复出现的话题。Shafi指出，在这方面存在三个问题:1)计算机能否自动提出要证明的猜想/定理?2)能有效地找到这些猜想的证据吗?3)这种证明能有效地检查吗?
对于一个数学全能定理证明是否指日可待，人们还没有达成明确的共识。然而，小组成员也承认，计算机在数学研究中已经发挥了作用，从使用程序寻找几何和数论中有趣的结构到猜想的反例。文中还介绍了计算机辅助证明的一些成功案例，如四色定理的证明。另一个亮点是提到了由英国剑桥微软研究院的研究人员对简单组分类证明的计算机辅助验证。
我还发现Butler Lampson对软件系统的描述是“精确的”和“近似的”，这非常吸引人。根据Lampson的说法，具有严格规范的软件系统可以被认为是精确的(例如，空中交通管制)，而大多数软件是近似的，因为对不同的人的需求不一样(例如，搜索引擎)。当一个人需要大量的软件工程方法(如形式化方法)来确保软件符合精确的规范时，这通知并区分了场景，以及其他场景(如在近似软件中)，对于这些场景，大量的测试应该足够了(尽管安全性是一个同样影响精确软件和近似软件的问题，并且无论使用哪种方法都仍然是一个棘手的问题)。
维贾伊甘是加拿大滑铁卢大学电子与计算机工程系的助理教授。
没有发现记录