劃重點
01人工智能初創(chuàng)公司Harmonic完成7500萬美元A輪融資，由紅杉資本領(lǐng)投，估值達到3.25億美元。
02Harmonic致力于創(chuàng)造數(shù)學(xué)超級智能(MSI)，認(rèn)為這種技術(shù)將應(yīng)用于需要準(zhǔn)確性的行業(yè)，如軟件工程、工業(yè)設(shè)計和醫(yī)療技術(shù)。
03該公司的大模型Aristotle在形式數(shù)學(xué)基準(zhǔn)MiniF2F中達到90%的水平，展示了其在解決高級數(shù)學(xué)問題方面的能力。
04由于此，Harmonic計劃在未來關(guān)鍵數(shù)學(xué)基準(zhǔn)上跟蹤系統(tǒng)不斷增長的能力。
05紅杉資本合伙人安德魯里德表示，他投資Harmonic是因為相信人工智能可以加速人類的數(shù)學(xué)能力。
以上內(nèi)容由騰訊混元大模型生成，僅供參考
投后估值3.25億美元。
來源|多知
作者|王上
今天，致力于創(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)前，公司估值達到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)是實現(xiàn)邏輯推理的關(guān)鍵，這有助于確保人工智能模型的反應(yīng)始終是正確和真實的。它補充說，人工智能系統(tǒng)必須具有“強大和可驗證的推理能力”。
也就是說，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è)計和醫(yī)療技術(shù)等。
Harmonic聯(lián)合創(chuàng)始人兼首席執(zhí)行官Tudor Achim表示，數(shù)學(xué)超級智能（MSI）將是下一個人工智能前沿。
01
用新方法解決幻覺問題，在形式數(shù)學(xué)基準(zhǔn)中達到了90%的水平
Harmonic的大模型致力于解決高難度數(shù)學(xué)問題，并采用了和自然語言不一樣的訓(xùn)練方式。
對于自然語言大模型來說，一個致命的缺點是總產(chǎn)生幻覺問題，Harmonic希望能解決這個問題。
今年8月，Harmonic宣布了正在開發(fā)的第一個模型Aristotle（亞里士多德），這是以希臘哲學(xué)家和數(shù)學(xué)家的名字命名的大模型。
當(dāng)遇到自然語言數(shù)學(xué)問題時，Aristotle有能力用Lean 4(一種基于微積分的函數(shù)編程語言)將這些問題形式化。以形式化驗證的方式解決問題，并以自然語言和 Lean 輸出答案。“這是朝著我們‘解決研究數(shù)學(xué)中的高級問題和驗證世界上所有推理’的長期目標(biāo)邁出的重要一步。”Harmonic團隊提到。
在博客中，Harmonic團隊提到，現(xiàn)有的大型語言模型在遇到問題時時常會產(chǎn)生幻覺�；糜X可能很危險，因為它們會導(dǎo)致人工智能系統(tǒng)以不可預(yù)測的方式行事。更重要的是，隨著人工智能在人們的生活中扮演越來越重要的角色，幻覺的風(fēng)險也在增加。
Harmonic表示，如果它能為人工智能模型提供進行數(shù)學(xué)推理的能力，就應(yīng)該能夠保證它們的反應(yīng)永遠(yuǎn)是正確的，因此不會產(chǎn)生幻覺。Harmonic認(rèn)為，與目前的模型不同，這種具有透明和可驗證的“推理痕跡”的模型將“從根本上是安全的”。
今年9月，Harmonic 在數(shù)學(xué)超級智能方面取得最新進展，比如：
1）MiniF2F 基準(zhǔn)測試中達到 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é)課程。這些問題涵蓋了從簡單計算到極具挑戰(zhàn)性的證明等一系列難度：三道驗證集問題來自國際數(shù)學(xué)奧林匹克 (IMO)，即使對于訓(xùn)練有素的參賽者來說，這些問題也普遍被認(rèn)為極其困難。
未來，Harmonic 計劃在關(guān)鍵的數(shù)學(xué)基準(zhǔn)上跟蹤系統(tǒng)不斷增長的能力。
（Aristotle 在 MiniF2F 基準(zhǔn)測試中的表現(xiàn)）
Harmonic 在官方博客中提到：“MiniF2F 衡量了我們模型在面對形式化問題時的核心問題解決能力。這讓我們能夠?qū)ristotle與人類表現(xiàn)和先前的研究進行對比。展望未來，我們將繼續(xù)公開跟蹤 MiniF2F 等形式化基準(zhǔn)測試以及涉及自然語言理解的任務(wù)的進展。”
02
數(shù)學(xué)超級智能可應(yīng)用于多個行業(yè)，“是人工智能的下一個前沿”
Harmonic 聲稱，帶有MSI的人工智能模型將立即在目前無法依賴人工智能的一系列行業(yè)中發(fā)揮作用，包括航空航天、計算機芯片設(shè)計、工業(yè)系統(tǒng)和醫(yī)療保健，這些行業(yè)對軟件的可靠性至關(guān)重要。
此外，Harmonic 將幫助推動人工智能研究本身的邊界，使創(chuàng)建更強大的系統(tǒng)，甚至可以創(chuàng)建自己的合成數(shù)據(jù)，以增強他們的知識和學(xué)習(xí)。
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)基梅隆大學(xué)計算機科學(xué)學(xué)士學(xué)位，曾是斯坦福大學(xué)計算機科學(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，是因為他相信人工智能可以加速人類的數(shù)學(xué)能力，為新的人工智能應(yīng)用鋪平道路。
Vlad Tenev 表示：“我們相信數(shù)學(xué)超級智能是人工智能的下一個前沿。我們很高興與 Sequoia、Index 和許多其他偉大的投資者合作，加速準(zhǔn)確且尋求真相的人工智能模型的出現(xiàn)。”
