Axiom是一家人工智慧初創企業，由洪樂潼（Carina Hong）創立於2024年，主要面向對沖基金、量化交易公司等金融機構提供基於AI的量化解決方案和“數學即服務”，其公司使命為“從AI數學家起步，打造自我改進的超級智慧型推理器”。其核心技術是開發基於形式數學證明訓練的可驗證人工智慧系統，利用Lean程式語言確保AI推理過程的每一步都可被數學驗證；2025年其AxiomProver系統在普特南數學競賽中取得滿分成績，並使用Lean語言完成了埃爾德什問題集中題目的形式化證明。
公司起源於2024年洪樂潼與Meta前AI研究總監Shubho Sengupta的交流後輟學創業，核心團隊包括CTO Shubho Sengupta（曾任Meta AI研究總監）、創始數學家Ken Ono和核心科學家François Charton。2025年完成6400萬美元種子輪融資（由B Capital領投），投後估值3億美元；2026年3月完成2億美元A輪融資（由Menlo Ventures領投），投後估值16億美元，進入獨角獸行列。
基本介紹
- 外文名：Axiom
- 創始人：洪樂潼
- 定義：人工智慧初創企業
創始人,發展歷程,基本特徵,套用,公司文化,
創始人
曾獲美國數學協會頒發的Alice T. Schafer獎、摩根獎。2022年底獲得牛津大學羅德獎學金，隨後在牛津大學學習神經科學，獲碩士學位。2024年進入史丹福大學攻讀數學博士和法學博士，後輟學創業。
發展歷程
2026年3月，Axiom完成2億美元A輪融資，投後估值達16億美元，正式進入獨角獸行列，公司成立僅1年多。本輪融資由知名風險投資機構Menlo Ventures領投，公司原有股東均參與跟投。
基本特徵
Axiom的核心技術是開發基於形式數學證明訓練的AI系統。Axiom採用Lean程式語言將數學證明轉化為可執行程式，確保每一步推理都可被機器驗證，以實現可驗證的人工智慧。該系統專注於讓AI理解數學本質和邏輯結構，進行嚴格推理。其長期目標是從輔助數學證明開始，逐步發展出更強大的推理能力。
套用
Axiom的核心技術當前主要套用於金融量化領域，其目標客戶為對沖基金、量化交易公司等金融機構，旨在幫助其快速解決投資、股市等金融領域的複雜數學問題，提供“數學即服務”的解決方案。Axiom的技術在基礎數學研究領域也已取得驗證性成果，其開發的AxiomProver系統在2025年的普特南數學競賽中取得了滿分成績，並自主證明了多個開放數論猜想，該系統還使用Lean語言完成了埃爾德什問題集中題目的形式化證明。
未來，Axiom計畫將其研究與套用擴展到金融建模、晶片架構、量化交易等更多領域。公司的長期願景是通過數學驗證，提高AI生成代碼的可靠性，為未來的AI基礎設施提供基礎能力。
公司文化
Axiom（公理）的公司名稱寓意其業務以數學公理為出發點，旨在構建能夠進行嚴格數學推理的人工智慧系統。公司內部環境體現了對數學傳統的尊重，例如會議室以高斯、阿達·洛夫萊斯等數學家的名字命名。
Axiom倡導的工作理念是“人類直覺由機器驗證來‘落地’，而機器驗證反過來激發人類直覺”，致力於構建人機協作的新範式。公司的核心追求是開發“可驗證人工智慧(Verified AI)”，即讓AI的每一步推理都可以被數學驗證，而不僅僅是機率輸出，以確保結果的嚴謹性和可靠性。公司在官方介紹中強調了數學在人工智慧發展中的基礎作用。
