作者丨巴里
编辑丨海腰
一个创立了自动驾驶公司，一个创立了股票交易平台，这两家公司的创始人凑在一起又会干出什么事儿来呢？
答案是数学超级智能（MSI）。
这两位大佬都对用AI解决“千年大奖难题”（Millennium Prize Problems）的顶级数学问题所着迷。
于是，俩人在2023年走到了一起，成立了Harmonic公司，致力于研发数学超级智能（Mathematical Superintelligence，MSI），目标是让AI拥有超越人类的数学能力，进而推动科学、工程等领域的知识再上一个台阶。
日前，这家人工智能初创公司Harmonic宣布完成7500万美元（约合5.3亿元人民币）的A轮融资。本轮融资由红杉资本领投，Index Ventures、Jasper Lau的Era Funds、GreatPoint Ventures、DTS Global Partners、Palo Alto Networks Inc.等公司参投。公司投后估值达到3.25亿美元（约合23亿元人民币）。
可以说，数学是一门最能集中体现出人类推理思维的学科。即使是大获成功的深度学习神经网络，在数学推理方面也没有取得太多进展。但最近，谷歌、OpenAI、阿里等巨头以及Harmonic这样的创业公司所推出的AI模型，正在改变这种现状。
现有包括ChatGPT在内的大模型，都有各种各样的限制和缺陷，包括无法避免“幻觉”问题、难以进行严密推理等。大模型训练的“原料”来自于庞大的互联网，但却缺乏解决复杂问题所需的深入、结构化的推理。
“AI在回答数学题时之所以成绩不佳，核心还是由于基础模型的数学能力有限。”
阿里达摩的研究人员就曾表示，虽然在面对解答题和证明题时，AI可以通过知识检索等方式拿到基础分，但一旦涉及到后续的深入分析，AI就开始出现“知识幻觉”。尤其是在面临选择题时，多数AI出现了“蒙题”的现象。
那么，如何弥补这一推理差距呢？
Harmonic认为，推理的最纯粹形式就是通过数学，这也是弥补这一差距并最终超越人类的关键。解决复杂的数学问题需要一个严密的步骤框架和逻辑证明。如果一个AI模型擅长解决数学问题，它就能够进行更高级的结构化推理。
两位创始人Tudor Achim和Vlad Tenev都是连续创业者。
在专业上，两人也可谓十分互补，Tudor Achim积累了丰富的大模型训练经验，Vlad Tenev则拥有快速的产品化和平台运营能力。
Harmonic联合创始人Vlad Tenev和Tudor Achim，图源：index ventures
Tudor Achim拥有卡内基梅隆大学计算机科学学士学位，曾是斯坦福大学计算机科学博士候选人。他作为联合创始人兼前首席技术官参与创立的Helm.ai，也可谓是自动驾驶+大模型领域的明星公司，今年8月推出了面向自动驾驶汽车和机器人的VidGen-1模型。
睿兽分析显示，Helm.ai已经至少融资5轮，不仅有本田、Goodyear Ventures固特异创投等产业资本参与，还吸引来了美版知乎Quora的联合创始人Charlie Cheever和Adam D’Angelo、职业NBA球星凯文·杜兰特（Kevin Durant）和前美国中央情报局局长大卫·霍威尔·彼得雷乌斯上将（Gen. David Petraeus）等的天使投资。
Vlad Tenev则拥有斯坦福大学数学学士学位和加州大学洛杉矶分校数学硕士学位，还是美国互联网券商（在线股票交易平台）Robinhood Markets的联合创始人兼首席执行官，其美股市值达到约227亿美元（约合1605亿元人民币）。
他们迅速组建起了一支AI和数学专家团队，并提出了一个大胆的理念：数学是推理的语言，是人类发现宇宙基本真理的工具。
其目标是构建一个数学能力超越人类的AI系统，来实现数学超级智能（MSI），从而克服当前AI面临的“幻觉”问题，即模型对无法正确回答的问题编造答案。
Harmonic表示，数学超级智能（MSI）是实现逻辑推理的关键，有助于确保模型的回答总是正确和真实的。他们补充道，AI系统必须具有“强大且可验证的推理能力”。具有数学超级智能（MSI）的AI系统能够大大推进在科学和工程等领域的知识与理解。
市面上的大模型，都没能达到人类的推理水平，这也就是它们为什么会经常产生“幻觉”的原因。
Harmonic认为，“幻觉”问题非常危险，特别是随着AI正在人们生活在扮演越来越重要的角色，可能会导致AI系统发生不可预测的行为，增加潜在的社会风险。
而数学超级智能（MSI）能够增强模型的数学推理的能力，从而在很大程度上避免“幻觉”的产生。与当前模型不同，这种具有透明和可验证的“推理轨迹”的模型从根本上保证了安全。
Tudor Achim注意到，整个AI行业已经开始意识到数学是构建真正的超级智能所必需的环节。
为此，今年8月，Harmonic推出了第一个MSI模型亚里士多德（Aristotle），命名灵感来源于古希腊的哲学家与数学家。
创新之处在于其采用了与传统自然语言大模型截然不同的训练方法，使其在高难度数学问题上表现优异。
据悉，亚里士多德基于微积分编程语言Lean 4（一种基于微积分的函数编程语言）开发，能够将自然语言中的数学问题形式化，并验证推理过程的正确性。亚里士多德已在MiniF2F数学基准测试中取得了90%的成绩，这是全球数学AI系统的一大突破。
Aristotle 在 MiniF2F 基准测试中的表现，图源：Harmonic
这种处理方式极大降低了模型产生幻觉的风险，确保了其结果的正确性和透明性。相比现有的大模型，亚里士多德所提出的“推理轨迹”技术无疑是一个重要的保障。
这一模型的潜力不止于解决数学问题。随着对精确性需求的上升，Harmonic所研发的数学超级智能（MSI），未来的实际应用场景极为广泛，包括航空航天、计算机芯片设计、工业系统和医疗等领域，确保这些关键领域的系统稳定性和安全性。
此外，数学超级智能（MSI）还可以推动人们对AI技术的进一步研究，创造出更加强大的AI系统，甚至可以创建自己的合成数据，不断增强模型的知识和学习能力。
Harmonic希望借助融资加速亚里士多德的研发，让它成为第一个数学技能超越人类的AI系统。
“之所以投资Harmonic，是因为相信AI能够将人类的数学能力推到一个新的高度，帮助创造出更多的AI杀手级应用”，红杉资本的合伙人Andrew Reed表示。
近年来，包括OpenAI、谷歌在内的公司都在试图用AI“征服”数学。
“过去22个月，AI的发展速度超过历史上的任何时期。”阿里巴巴集团CEO吴泳铭打了个形象的比方，去年大模型的数学能力还只是中学生水平，但今天已经可以拿到国际奥赛金牌，尤其在物理、化学生物等多方面学科，已经接近博士生。
去年底，谷歌DeepMind公司发布的数学大模型FunSearch，针对人类历史上的诸多数学难题给出了新的解法。这是大模型第一次对数学领域中具有挑战性的开放性问题给出新的发现或解法，也将为解决悬而未决的数学难题开辟新的途径。
另一支DeepMind团队建立起一个名为“阿尔法几何”（AlphaGeometry）的数学大模型，解决了国际数学奥林匹克（IMO）中的复杂几何问题。
解答国际数学奥林匹克的数学题，需要强大的头脑创造力，而AI历来在解答此类问题中的表现不佳。
但“阿尔法几何”经过针对性训练后，在逻辑检查系统的加持下，其几何学的解题表现几乎与最优秀的人类选手不相上下。
计算机科学家克里斯蒂安·塞格迪则致力于用AI进行数学运算和自动形式化。他相信，“超人AI数学家”到2026年就会出现，“一旦拥有了推理这种新技能，AI不仅可以拥有人类的直觉，而且还将大大超越”。
在Harmonic看来，数学超级智能（MSI）的影响将是惊人的，未来触手可及。
它可以帮助我们运行复杂的数值求解器，优化工厂的产线提升效率，帮助程序员验证代码的正确性和质量等等。有一天，它甚至可能发现下一个伟大的科学突破。
Tudor Achim预言道，数学超级智能（MSI）将成为AI的下一个重要前沿。
正如伽利略所说，大自然是用数学语言写成的书。
