專攻數(shù)學(xué)超級智能的Harmonic獲7500萬美元投資，紅杉領(lǐng)投，CEO：將是下一個AI前沿

　　來源|多知

　　作者|王上

　　今天，致力于創(chuàng)造數(shù)學(xué)超級智能(MSI)的人工智能初創(chuàng)公司Harmonic在其官網(wǎng)宣布，已經(jīng)完成了7500萬美元的A輪融資。本輪融資由紅杉資本領(lǐng)投，Index Ventures、Jasper Lau的Era Funds、GreatPoint Ventures、DTS Global Partners、Palo Alto Networks Inc.等公司參投。當(dāng)前，公司估值達(dá)到3.25億美元。

　　Harmonic成立于2023年，其目標(biāo)是創(chuàng)造數(shù)學(xué)超級智能（MSI），MSI是一種數(shù)學(xué)能力優(yōu)于人類的人工智能，在Harmonic看來，由于推理的語言是數(shù)學(xué)，而數(shù)學(xué)是人類發(fā)現(xiàn)關(guān)于宇宙的許多基本真理的手段，因此，具有MSI的人工智能系統(tǒng)應(yīng)該能夠極大提高人類在科學(xué)和工程等領(lǐng)域的知識和理解。

　　在Harmonic的官方博客文章中，Harmonic解釋說，數(shù)學(xué)超級智能(MSI)是實(shí)現(xiàn)邏輯推理的關(guān)鍵，這有助于確保人工智能模型的反應(yīng)始終是正確和真實(shí)的。它補(bǔ)充說，人工智能系統(tǒng)必須具有“強(qiáng)大和可驗(yàn)證的推理能力”。

　　也就是說，Harmonic認(rèn)為，數(shù)學(xué)超級智能(MSI)能克服傳統(tǒng)上“幻覺”的限制，即消除AI模型無法正確回答的問題編造答案的情況。

　　可以看到，越來越多人工智能公司聚焦數(shù)學(xué)領(lǐng)域，希望攻克大模型的推理能力。

　　在Harmonic 看來，帶有數(shù)學(xué)超級智能(MSI)的技術(shù)將應(yīng)用于特別需要準(zhǔn)確性的行業(yè)，包括軟件工程、工業(yè)設(shè)計(jì)和醫(yī)療技術(shù)等。

　　Harmonic聯(lián)合創(chuàng)始人兼首席執(zhí)行官Tudor Achim表示，數(shù)學(xué)超級智能（MSI）將是下一個人工智能前沿。

　　01

　　用新方法解決幻覺問題，在形式數(shù)學(xué)基準(zhǔn)中達(dá)到了90%的水平

　　Harmonic的大模型致力于解決高難度數(shù)學(xué)問題，并采用了和自然語言不一樣的訓(xùn)練方式。

　　對于自然語言大模型來說，一個致命的缺點(diǎn)是總產(chǎn)生幻覺問題，Harmonic希望能解決這個問題。

　　今年8月，Harmonic宣布了正在開發(fā)的第一個模型Aristotle(亞里士多德)，這是以希臘哲學(xué)家和數(shù)學(xué)家的名字命名的大模型。

　　當(dāng)遇到自然語言數(shù)學(xué)問題時，Aristotle有能力用Lean 4(一種基于微積分的函數(shù)編程語言)將這些問題形式化。以形式化驗(yàn)證的方式解決問題，并以自然語言和 Lean 輸出答案。“這是朝著我們‘解決研究數(shù)學(xué)中的高級問題和驗(yàn)證世界上所有推理’的長期目標(biāo)邁出的重要一步。”Harmonic團(tuán)隊(duì)提到。

　　在博客中，Harmonic團(tuán)隊(duì)提到，現(xiàn)有的大型語言模型在遇到問題時時常會產(chǎn)生幻覺?；糜X可能很危險，因?yàn)樗鼈儠?dǎo)致人工智能系統(tǒng)以不可預(yù)測的方式行事。更重要的是，隨著人工智能在人們的生活中扮演越來越重要的角色，幻覺的風(fēng)險也在增加。

　　Harmonic表示，如果它能為人工智能模型提供進(jìn)行數(shù)學(xué)推理的能力，就應(yīng)該能夠保證它們的反應(yīng)永遠(yuǎn)是正確的，因此不會產(chǎn)生幻覺。Harmonic認(rèn)為，與目前的模型不同，這種具有透明和可驗(yàn)證的“推理痕跡”的模型將“從根本上是安全的”。

　　今年9月，Harmonic 在數(shù)學(xué)超級智能方面取得最新進(jìn)展，比如：

　　1)MiniF2F 基準(zhǔn)測試中達(dá)到 90% 的最新水平(8月份的成績?yōu)?3%);

　　2)對 MiniF2F 內(nèi)部更新的公開發(fā)布;

　　3)全新的自然語言界面。

　　MiniF2F是標(biāo)準(zhǔn)的形式數(shù)學(xué)基準(zhǔn)，它將形式定理證明問題與自然語言和形式數(shù)學(xué)之間的轉(zhuǎn)換分離開來。這些問題來自國內(nèi)和國際高中數(shù)學(xué)競賽，以及高中和本科數(shù)學(xué)課程。這些問題涵蓋了從簡單計(jì)算到極具挑戰(zhàn)性的證明等一系列難度：三道驗(yàn)證集問題來自國際數(shù)學(xué)奧林匹克 (IMO)，即使對于訓(xùn)練有素的參賽者來說，這些問題也普遍被認(rèn)為極其困難。

　　未來，Harmonic 計(jì)劃在關(guān)鍵的數(shù)學(xué)基準(zhǔn)上跟蹤系統(tǒng)不斷增長的能力。

　　Harmonic 在官方博客中提到：“MiniF2F 衡量了我們模型在面對形式化問題時的核心問題解決能力。這讓我們能夠?qū)ristotle與人類表現(xiàn)和先前的研究進(jìn)行對比。展望未來，我們將繼續(xù)公開跟蹤 MiniF2F 等形式化基準(zhǔn)測試以及涉及自然語言理解的任務(wù)的進(jìn)展。”

　　02

　　數(shù)學(xué)超級智能可應(yīng)用于多個行業(yè)，“是人工智能的下一個前沿”

　　Harmonic 聲稱，帶有MSI的人工智能模型將立即在目前無法依賴人工智能的一系列行業(yè)中發(fā)揮作用，包括航空航天、計(jì)算機(jī)芯片設(shè)計(jì)、工業(yè)系統(tǒng)和醫(yī)療保健，這些行業(yè)對軟件的可靠性至關(guān)重要。

　　此外，Harmonic 將幫助推動人工智能研究本身的邊界，使創(chuàng)建更強(qiáng)大的系統(tǒng)，甚至可以創(chuàng)建自己的合成數(shù)據(jù)，以增強(qiáng)他們的知識和學(xué)習(xí)。

　　2023 年，Tudor Achim與Vlad Tenev共同創(chuàng)立了 Harmonic，旨在打造世界上最先進(jìn)的推理引擎。

　　Tudor Achim與Vlad Tenev都是連續(xù)創(chuàng)業(yè)者：

　　udor Achim還是Helm.ai的聯(lián)合創(chuàng)始人兼前首席技術(shù)官，Helm.ai為高級駕駛輔助系統(tǒng)(ADAS)、自動駕駛(AV)和機(jī)器人自動化提供先進(jìn)人工智能(AI)軟件的供應(yīng)商。Tudor Achim擁有卡內(nèi)基梅隆大學(xué)計(jì)算機(jī)科學(xué)學(xué)士學(xué)位，曾是斯坦福大學(xué)計(jì)算機(jī)科學(xué)博士候選人。

　　Vlad Tenev還是 Robinhood Markets (美國在線股票交易平臺)的聯(lián)合創(chuàng)始人兼首席執(zhí)行官，Vlad Tenev擁有斯坦福大學(xué)數(shù)學(xué)學(xué)士學(xué)位和加州大學(xué)洛杉磯分校數(shù)學(xué)碩士學(xué)位。

　　Harmonic聯(lián)合創(chuàng)始人兼首席執(zhí)行官Tudor Achim表示，人工智能行業(yè)已經(jīng)意識到數(shù)學(xué)是構(gòu)建真正的超級智能所需的缺失環(huán)節(jié)。他說：“Harmonic正在引領(lǐng)這些發(fā)展，同時解決了其他人工智能模型中常見的局限性。”

　　這家初創(chuàng)公司表示，今天這輪融資的資金將幫助它加速Aristotle的開發(fā)，并創(chuàng)建第一個數(shù)學(xué)技能優(yōu)于人類的人工智能系統(tǒng)。

　　紅杉資本的合伙人安德魯·里德(Andrew Reed)表示，他之所以投資Harmonic，是因?yàn)樗嘈湃斯ぶ悄芸梢约铀偃祟惖臄?shù)學(xué)能力，為新的人工智能應(yīng)用鋪平道路。

　　Vlad Tenev 表示：“我們相信數(shù)學(xué)超級智能是人工智能的下一個前沿。我們很高興與 Sequoia、Index 和許多其他偉大的投資者合作，加速準(zhǔn)確且尋求真相的人工智能模型的出現(xiàn)。”

　　END

　　作者：王上