Author: 木遥

艺术是创造能力的一种状态，包括了真正的推理过程。 ──亚里士多德 刘慈欣在一篇科幻小说《诗云》中，设想了一个化身为李白的外星人试图利用技术来实现诗歌的创作。尽管外星人的科技水平发达到了不可思议的程度，然而用程序创作出媲美李白的诗歌似乎仍然是不可能完成的任务，甚至让程序来鉴赏一首诗是否出色也过于困难了。 刘慈欣本人写过一个作诗机的软件。但是很显然，他并不相信机器算法能够成为像人类一样的诗人。他是过于悲观了么？ 大多数人都会根深蒂固地认为，艺术创作（特别是高质量的精英艺术创作）和人的心灵密切相关，而任何形式和技巧层面的解析和实现都只能触及它的皮毛。尽管这种作用多少显得有些神秘而难于言表，可是恐怕没有谁会怀疑，在巴赫的恰空和达芬奇的蒙娜丽莎之中，有某种专属于人性的神圣和崇高之处。 但是另一方面，一部人类的文明史，基本上也就是人类的领地不断被人类所发明的机器占领和取代的历史。人工智能和机器学习技术的发展使得让机器程序创作出能够以假乱真的艺术作品早已不是幻想。侯世达，《集异璧》一书的作者，曾经这样描述他在听到并亲自弹奏一首短小精致的钢琴作品后的感受： 尽管能间或听出些小瑕疵，这首曲子还是给我留下了深刻的印象，因为它似乎在「倾诉」着什么。如果谁告诉我它是出自人手，我绝不会怀疑它的表现力。这首曲子听来有些怀旧，带点波兰味道，而全无抄袭嫌疑。它是崭新的，而又毫无疑问地刻上了「肖邦风格」的烙印，却不令人觉得情感空乏。我的的确确受到了震撼：抒情的乐曲怎么能从一个从未听过一个音、从未活过一秒钟、从无一丝一毫情感的程序中写出来？ 这首作品是一首仿制的肖邦马祖卡舞曲，出自加州大学圣克鲁兹分校作曲学教授 David Cope 的 EMI （音乐智能实验）程序「之手」。这个程序的原理是首先研究一名真实的作曲家的作品中不同层面不同类型的抽象结构，然后以新的形式重组这些结构，从而得到一部仿制作品。 这听起来像是儿戏，但其效果惊人。侯世达曾经在一次纽约 Eastman 音乐学院举办的讲座中，先后播放了上面提到的那首伪肖邦作品和另一首真正的肖邦作品，并且让听众们（大多数是音乐专业的师生）判断哪一首是真正的肖邦。大多数听众选择了错误的答案。毫无疑问，这是极其戏剧性的一幕。 我们知道，在计算机科学中有一条著名的图灵实验法则：一个人使用任意一串问题去询问一个正常思维的人和一个机器，如果经过若干询问以后他不能得出实质的区别，则我们认为此机器具备人工智能。与此类似，如果机器创作的艺术作品和人类作品在人类欣赏者眼中是不可分辨的，我们有什么理由不认为机器在艺术创作领域里完全可以取代人的作用呢？ 如果一个人放弃关于艺术创作的种种玄学般的神秘信仰，而认定一切艺术作品都只不过是某种抽象的形式组合，那么用逻辑和数学来研究美的奥秘就是一种顺理成章的尝试。1933 年，哈佛大学数学系教授，当时美国最重要的数学家之一 George Birkhoff 出版了一本出乎同行意料的小书：《美学测度》，讨论了用数学公式衡量并刻画艺术作品的美学价值的可能性。在书中他断言到： 如果美学理论是科学的，那么它就必须从分析的角度加以审视，必须将其自身理解为艺术的纯形式的一面。 这本书并没有引起很大反响，反而招致了不少批评，这恐怕是因为他的理论实在过于粗糙。作为他的理论的核心，他认为一个对象的「美丽程度」可以用下面的公式来计算： 美 = 有序度 / 复杂度 其中有序程度和复杂程度对于不同类型的艺术作品有不同的定义方式。例如对于每一个多边形而言都可以用一种特定的算法算出一个美丽得分： 同样的方式也被他应用在音乐、绘画、建筑和诗歌上。毫不令人意外地，这种异想天开的「美学理论」很快就被人们抛诸脑后了。 但是这一理想并未消失。在二十世纪下半叶，它以崭新的形式重新出现在人们面前。一方面，这得益于电子计算和人工智能理论的迅猛发展；另一方面，现代艺术观念极大地改变了人们对艺术作品的认识和期望。毕竟，让今天的电脑模仿米开朗基罗或者黄宾虹的创作仍然是过于困难的任务，但是对普通欣赏者来说，很多现代艺术作品看起来不过只是幼稚随机的线条和色彩的涂抹，而这样的作品用机器算法实现起来一点也不困难。 从 1977 年开始，加州大学圣地亚哥分校的艺术家 Harold Cohen 开始编写一组名为 Aaron 的电脑程序，赋予其绘画的模式和功能。这些作品起初只是纯然随机的线条色块，随着程序日渐复杂，它开始「学会」画出更复杂的对象，例如石块和植物，以至于人像。下面是两幅 Aaron 的作品，分别名为《在高更的海滩上相遇》（1988）以及《Aaron 和装饰板》（1992）。 Cohen 曾经带着这些 Aaron 的作品在国际上的多家画廊内进行展出。一开始，大多数观众拒绝相信这是纯粹由电脑生成的作品。当 Cohen 解释了这些作品的创作原理之后，观众们又断言说这些作品中体现出了某种统一的「个性」。这是个有趣的事实，因为这些作品除了都生成自同一算法之外别无共同点。这是不是意味着，所谓的艺术个性其实不过是一种程序性的算法模式而已呢？ 编写 Aaron 程序的基本思路，是像教会一个没有见过大自然的孩子画出大自然一样教会电脑画画。也就是说，用语言为它定义出所有可能的物体的样子，以及这些物体会倾向于如何排列在空间中，然后令其自由随机发挥即可。这一过程可以是完全技术性的，不牵涉任何层面的美学观念，例如「平衡」或者「和谐」之类，然而其作品却会自发的体现出特定的艺术性选择。 当然，我们可以认为，电脑在这里并不真的是进行完全「自发」的创作。虽然每一幅画的生成过程不受干预，但是 Cohen 本人的美学观念毕竟以一种并不直接的方式隐藏在编程的过程之中。如果换了一个人来编写 […]

张生在普救寺第一眼见到崔莺莺就陷入了不可自拔的境地。「呀！正撞着五百年前风流业冤。」于是为了搭讪，张生插科打诨无所不用其极。「月色溶溶夜，花阴寂寂春；如何临皓魄，不见月中人？」诗是好诗，可惜是隔墙念的。 崔莺莺见了只沉吟不语。然而回到家里，「神魂荡漾，情思不快，茶饭少进。」红娘瞧了暗笑：「姐姐往常不曾如此无情无绪；自见了那张生，便觉心事不宁，却是如何？」 这开头如此典型，以至于可以套在古今中外无数或真或假的八卦前面。19岁的海涅第一眼见到15岁的表妹阿玛丽，就像维特见到了夏绿蒂，「一位天使！ ——没说的！谁谈起自己的意中人都这么说，不是吗？可是我却无法告诉你，她是多么完美，她为什么会那么完美；够了，她已经把我整个心都俘获了。」我不知道别人有没有产生过和我一样的疑惑，他们真的这么写情书么？收信人不觉得难受么…… 还是中国人含蓄，「这个妹妹我曾见过的。」妥帖多了，但也多少有点无趣。严格说起来，贾宝玉也真的从来不曾像张生或者维特那样追过女孩子。在元宵夜宴上贾母声色俱厉地指出过张生模式的不靠谱。贾宝玉听了作何想法，我们不知道。但是我们知道的是他多少算是个被动的人，连宝钗都算比他要勇敢些。 于是宝钗成功地和宝玉在一起了。这当然只是个和西厢记一样不靠谱的个案，但是也不是没有道理可言的。 花开两朵，各表一枝。话说在1962年，两个数学家 David Gale 和 Lloyd Shapley 提出了下面的问题： 给定若干个男生和同样多的女生，他们每个人都对所有的异性有一个心理的偏好次序。是否存在一种男女配对组合构成一种稳定的组合关系？这里稳定组合的意思是说，不存在两个非伴侣的异性对彼此的评价比对各自伴侣的评价还要高。（可以理解，这样的异性太容易红杏出墙了，所以是某种不稳定因素。）进一步的问题是，在已知每个人对异性的偏好顺序的情况下，怎样求出这种稳定组合方式（如果它存在的话）？你可以理解为这是数学家们替月老问的问题：给定一群孤男寡女，寻找一种牵红线的方式，以确保把红杏扼杀在摇篮里。 这一问题被称为稳定婚姻问题。它有很多种可能的解法。为了让大家相信数学家不是真得如此无聊，我要指出它确确实实是一个地道的组合数学问题，有其特定的数学价值。当然啦，它也有很多别的背景和应用，比如用来在若干个公司和应聘者之间进行招聘中介……但是数学家们怎么会放过如此八卦的一个名字呢？于是它就这样流传下来了。 话说回来，有很多组合数学问题都可以如此这般的翻译为生活中的问题。比如著名的 Hall 定理：给定 n 个有限集合（其间可以有交集），如果其中任意 m 个集合的并集的元素个数都不小于 m，那么一定存在 n 个不同的元素，使得它们正好依次存在于这 n 个集合之中。我相信没有人明白以上这是在说什么。可是它有一个很好的解释：把那 n 个集合想象成 n 个男生各自心仪的女孩子们（一般来说都不止一个），中间的那个条件是说，如果对于其中任意一部分男生，他们喜欢的女孩子的总数都不少于这组男生的人数（这个条件是必要的，否则就打起来了），那么总的说来一定存在一种办法给每个男生都分配一个女生恰好是他喜欢的。 听起来真是令人心情愉快啊…… （这个定理事实上还有很多别的解释方式，比如说，把 52 张扑克牌任意分成 13 堆，每堆 4 张牌，那么上面的定理告诉我们，一定存在一种方式从每堆牌中 抽出一张来一共 13 张恰好凑成一条不一定同花的顺子。这件事情乍一听也是挺奇妙的，不过在这个特殊的日子里，我们还是专注于我们的主题吧。） 回到一开始提到的稳定婚姻问题，给定每个人关于异性的偏好排序，要寻找一种男女配对组合构成稳定的组合。Gale 和 Shapley 不但提出了这个问题本身，而且给出了一种著名的解法。这个解法可以描述为如下的求偶过程： 首先，让这些男生去向他们最心仪的女生求婚——这是数学家们的原本的用词。如果你觉得太快了的话，让我们暂时改成表白吧…… 然后，等所有男生表白完毕后，所有的收到表白女生们都从自己的表白者中选择自己最喜欢的人接受为男朋友。没人表白的女生只能暂时等一等了，不要着急，表白会有的。 以上过程称为「一轮」。之后的每一轮都按照类似的方式进行。首先由还处于单身状态的男生们每个人再次向自己还没有表白过的女生中自己最喜欢的人表白（无论人家是否已经有了男朋友），然后，等所有单身男生表白完毕后，所有的收到表白女生们都从自己的表白者中选择自己最喜欢的人接受为男朋友。如果原来有男朋友而表白者中有自己更喜欢的，不要犹豫，换之。等到尘埃落定之后，再开始如上所述的新的一轮表白。 依此类推。可以证明的是，这个过程一定是会终止的，也就是说，不会陷入任何死循环。并且一旦终止，每个人都会找到一个伴侣。更关键的是，这个过程最终得到的一定是如前所述的「稳定组合」：不存在两个非伴侣的异性对彼此的评价比对各自伴侣的评价还要高。——这几个事实都不难证明，有兴趣的话可以自己试试看。 所以这就得到了稳定婚姻问题的一个解（顺便也证明了解的存在性）。但是真正有趣的部分还在后面。一般来说，给定若干个男生女生和他们之间的偏好关系，稳定组合存在不止一种。上述「算法」只是给出了所有可能的稳定组合其中之一而已。但是这个特定的解具有某些特别的性质：可以证明（这一次证明不很容易了），上述方式得到的稳定组合和所有其他的可能的稳定组合相比，是对男生最优而对女生最劣的。 确切地说是这样： 它是对男生最优的。也就是说，对每个男生来说，按照这种方式最后找到的伴侣，是在所有的稳定组合中自己可能具有的伴侣中自己评价最高的。——注意这并不等于说每个男生都能追到自己最喜欢的女生，而只是说，他一定能追到「有可能和他在稳定组合中在一起的女生」中自己最喜欢的。有些女生虽然很好，但是和她在一起是不可能形成稳定组合的。这就是人生啊…… 另一方面，它是对女生最劣的。也就是说，对每个女生来说，按照这种方式最后找到的伴侣是在所有的稳定组合中自己可能具有的伴侣中自己评价最低的。同样的，这也不等于说每个女生都只有和自己最不喜欢的男生在一起，而只是说她最后的男朋友会是所有「有可能」的男生中自己觉得最勉强的。不过这样听起来也已经很悲惨了。 这两个结论并不直观，因为看起来在上面所描述的过程中，女生是相对占有优势的。作为男生，需要很辛苦地去不断表白，然后被拒，再表白，再被拒……而女生只要随心所欲挑选就好，而且还有随时更换男友的权利（在上面的规则里男生是不能主动提出分手的）。为什么结局会是如此？ […]

Offord 教授和我最近发现我们在《数学年鉴》中的论文存在一个蹊跷的错误。一个公式中的加号被写成了一个乘号，而后面那个命题的证明则是依赖于这个错误的公式的，因而也是无法成立的。不过，聊以自慰的是，我们最终能够确定那篇论文总的结论其实还是正确的。 ——《Littlewood 文集》 如果回忆一下中学数学的两门分支课程——代数和几何，就能清楚地看到，在数学的两种最基本的推演过程——计算和证明——之间一直存在着一种巨大的差别。在初等代数问题里，一个问题的求解（例如解一个方程或者计算一个多项式乘法）是可以通过规范化的步骤顺序实现的，这使得这门课程本质上同一门按照操作手册动手的劳技课并无不同。然而，几何定理（哪怕是最基本的初中平面几何）的证明却不然，发现一个证明的过程中一定存在着那样一些「灵光一闪」的时刻，它们可遇而不可求，使得几何这门课程几乎成为本质上「不可学」的一门课程。我们都曾经面对过无从下手的证明题目而摇头叹息过，也都在阅读一个自己想不出来的证明过程时体会过那种羚羊挂角无迹可循的美感。纵然掌握了再多的定理和证明技巧，在脑海中发现完整的逻辑道路的过程仍然是一个自发而偶然的事件，反映了人类思维的某些最难于用语言刻画的能力。从某种程度上说来，这正是数学这门学科的神秘感的终极来源。 也正因为如此，计算——无论多么繁琐——本质上都是可以被机械实现的，在今天更是借助电脑的辅助成为一种相对平凡的任务。而证明才被认为是数学本质的困难所在，是人类智慧的高度结晶。阅读并验证一个证明是否正确（或者哪怕仅仅是理解它在说什么）是一项辛苦而困难的任务，只有受过训练的数学家才能够得以完成。并且，和物理化学生物等牵涉到真实世界的学科不同，数学定理是不能被实验所证明的，从而数学家的阅读就成为本质上唯一可行的验证手段。这其实也正是今天数学界的真实运作方式：一个人写出一篇文章来宣称证明了一个定理，他的某些同行们会在特定的审议机制下阅读这篇文章并且宣布是否接受其论证。如果大家都认为证明无误，这个定理就被接纳为数学的一部分而存在下来。 这一流程的有效性已经为数学科学的茁壮生命力所证明，然而，任何人也都能看出这个过程中蕴含的极大风险：我们究竟在什么意义上能够宣称一个定理真的是正确的？其作者可能犯错，审阅者也可能犯错，我们都知道数学证明中的微小错误有时候是多么难于发现，而这些错误也许永远都不会有人知道。当然，这并不是说数学这门学问完全是空中楼阁：越是重要的定理，其阅读者也就越多，出错的概率也就越是无限趋近于零。我们不能想象一个从阿基米德时代就流传至今，被无数学生学习过的四五行的证明还会存在逻辑错误。但是即便如此，只要翻开数学史，我们还是能看到大量重要的错误由于极其偶然的原因才在事隔多年之后被人们发现的例子。 到了现代，这个问题更是严重得多，数学的复杂程度和专业化程度已经使得任何一个分支的专业人员数量同证明的普遍难度完全不成正比。这种矛盾在某些极端的例子里尖锐到了荒谬的程度：图论中的 Robertson–Seymour 定理的证明一共耗费了大约五百页的篇幅，Almgren 对几何测度论中的一个定理的证明总长为 1728 页，而代数中著名的有限单群定理（确切来说这不是一个定理而是一组定理）的证明总共包含超过五百篇论文，总页数估计在一万页以上。世界上恐怕不存在任何一个人真地把这个证明从头读到尾过，遑论验证其正确性了。有限单群方面的专家之一 Aschbacher 曾经不无自嘲的说过：「一方面，当证明长度增加时，错误的概率也增加了。在有限单群分类定理的证明中出现错误的概率实际上是 1。但是另一方面，任何单个错误不能被容易地改正的概率是 0。随着时间的推移，我们将会有机会推敲证明，从而对它的信任度也必定会增加的。」 我们也希望如此，但是以严谨而著称的数学体系是以这样远远难于称为严谨的方式被建立，终究构成某种吊诡而令人心生疑虑的现实。不仅如此，这一体系在某些情况下还会完全失效，一个著名的例子是四色定理在 1976 年的证明。Appel 和 Haken 在那个证明中把所有的地图用通常的逻辑推演的方式化归为 1936 种类型，然后——这是充满争议性的一步——编写了一个电脑程序逐个验证这些类型都满足四色定理的结论，从而完成了整个证明。一个立即存在的问题是：就算前面的逻辑部分是正确的，谁能证明后面的电脑程序中没有错误？难道数学家们应当逐行阅读代码以理解其正确性么？（写过程序的人一定晓得，阅读程序代码是比阅读一个通常的逻辑证明还要痛苦的经验。）另一个时间上稍近的例子是 Hales 对开普勒堆球定理的证明。这一证明包含了三百页的文本部分和四千行的代码部分，被投稿至数学界最重要的杂志《数学年鉴》，杂志的编辑最终接受了这篇论文，但是指出： 在我的经验里，还没有一篇论文曾经得到过这样的审查。审读人专门建立了一个讨论班研究这篇文章，他们检查了证明中大量的论述并且确认其正确性，这种检查常常需要耗时数个星期。……总的说来，他们并不能确认证明总体的正确性，而且估计永远无法做到这一点，因为他们在到达终点之前精力就耗尽了。” 至于代码部分，估计并没有被任何人认真地审阅过。 于是在一部分数学家那里，另一种可能性开始渐渐浮上水面。既然一般来说数学定理的证明及其审查是如此困难和繁琐的一件事，我们有没有可能从根本上把它转化成电脑能够承担的任务呢，就像我们已经成功让电脑代替人类实现的大多数繁琐劳动一样？注意，这种电脑的参与并不是像上面的例子里那样仅仅负责某些验证性的工作，而是从最底层介入逻辑推演的部分，从而严格的建立整个证明过程。这种思路，一般被称为形式证明（Formal Proof），有时也称为机器证明。 两个哲学家之间的争论并不比两个会计师之间的争论更复杂，他们只需要掏出纸笔，然后对彼此说：让我们来算一算吧。 ——《莱布尼茨通信》，1666 用计算的方式进行逻辑推演并不是什么新鲜想法，事实上，这是人类极为古老的梦想之一，它可以上溯到笛卡儿和莱布尼茨乃至霍布斯，甚至也许更早。霍布斯有名言曰：「推理就是计算」，不过考虑到他的数学（特别是几何）程度之糟糕，人们一向怀疑他根本不知道自己到底想说什么。莱布尼茨的观念则要清晰的多，在他看来，只要能够把一切逻辑论断用统一的语言确切的表达出来，并且采用严密的规则进行逻辑推演，那么世间的所有道理都是可以被严格推导出来的。 让我们抛开其间的哲学意涵不谈（莱布尼茨的梦想事实上已经涵盖了人类理性的全部领域），单就数学层面而言，这一框架听起来并不算特别不靠谱。从欧几里德开始，数学家们就开始着手把全部数学定理建立在公理体系之上，于是从理论上来说，任何一个数学定理的证明，确实是可以用纯粹的逻辑语言「算」出来的。这里的计算当然不是说加减乘除这样的四则运算，而是形式逻辑的基本运算，例如命题 A 为真推出命题 B 为假，诸如此类。这种运算也有其特定的「运算法则」，也就是我们平时所默认的那些形式逻辑的法则，以此为基础，一个推导就是在这些法则下的一次「计算」，而一个复杂的证明只不过是一道复杂的「计算题」而已。 事实上，经过二十世纪初那一场著名的数学革命以及随后的 ZFC 公理体系（这是今天数学界普遍承认的公理体系）的建立，这种把全部数学建立在逻辑演算之上的想法实际上并不存在理论上的障碍。实际困难在于，从人们熟悉的「人脑证明」到这种完全依赖于逻辑算符的「形式证明」之间，存在一个复杂度上的巨大鸿沟。我们在脑海中所进行的逻辑推导其实大量的依赖于人类特有的直觉想象和经验，如果要把每一环逻辑链条都清清楚楚地写下来，每一次推理都追溯到公理体系那里去，任何一个简单的证明都会变得繁琐到超乎想象的程度。我们喜欢严格性，但是这样做的代价也太大了。 然而电脑的发明改变了一切。众所周知，电脑最擅长于做的就是这种严格而繁琐的工作。把基本公理告诉电脑，把推理法则教给电脑，不就万事大吉了么？ 差不多了，只剩下最后一步——非常微妙的一步。在上面的叙述里，一切传统的人脑证明都可以转化为逻辑算符的「计算」，这是对的，但是其前提是这种传统证明已经存在了，所需要的只是恰当的翻译过程而已。如何发现一个未知的证明则是一个完全崭新的挑战。我们对于人脑是如何想出一个证明的过程都不甚了了，又如何能教给电脑去自己发现一个证明？ 于是人们采用了一种实用主义的策略。一方面，把人们已经知道的证明翻译给电脑，这同时也构成了对这些证明的逻辑严密性的一次确认。——虽然这件事情听起来很简单，操作起来仍然是很困难的事情。另一方面，小心翼翼的探索让电脑尝试去自动「发现」一个证明，哪怕只是很简单的证明而已。 让我们看看半个世纪以来人们已经让电脑做到了哪些事情： 1954 年，Davis 成功地让电脑证明了定理：偶数加偶数仍然等于偶数。 1959 年，王浩让电脑证明了罗素和怀特海的名著《数学原理》中的所有谓词逻辑定理。 1968 年，de Bruijn 用电脑给出了 […]