來源|多知

作者|王上

今天，致力于創(chuàng)造數(shù)學超級智能(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.等公司參投。當前，公司估值達到3.25億美元。

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

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

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

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

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

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

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

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

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

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

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

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

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

1）MiniF2F 基準測試中達到 90% 的最新水平（8月份的成績?yōu)?3%）；

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

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

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

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

（Aristotle 在 MiniF2F 基準測試中的表現(xiàn)）

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

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

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

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

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

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

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

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

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

紅杉資本的合伙人安德魯·里德(Andrew Reed)表示，他之所以投資Harmonic，是因為他相信人工智能可以加速人類的數(shù)學能力，為新的人工智能應(yīng)用鋪平道路。

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