★加星zzllrr小樂公眾號(hào)數(shù)學(xué)科普不迷路！

接上文

本文介紹文藝復(fù)興慈善基金會(huì)揭曉首批1800萬(wàn)美元AI數(shù)學(xué)基金資助的29個(gè)項(xiàng)目（三）[21 ~ 28]

作者：文藝復(fù)興慈善基金官網(wǎng)（Renaissance Philanthropy）2025-9-17

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號(hào)）2025-9-26

21、學(xué)習(xí)與吸血鬼（Vampire）和蜘蛛（Spider）一起做數(shù)學(xué)題

項(xiàng)目簡(jiǎn)介

該項(xiàng)目旨在通過(guò)將無(wú)窮級(jí)數(shù)和超越函數(shù)等特定數(shù)學(xué)結(jié)構(gòu)集成到全自動(dòng)定理證明器Vampire（吸血鬼）的推理程序中，增強(qiáng)其性能。本項(xiàng)目旨在通過(guò)創(chuàng)新的機(jī)器學(xué)習(xí)方法和針對(duì)特定數(shù)學(xué)理論定制的策略組合開發(fā)，提升Vampire在標(biāo)準(zhǔn)數(shù)學(xué)上的表現(xiàn)。該項(xiàng)目還將建立一個(gè)網(wǎng)絡(luò)服務(wù)，以促進(jìn)自動(dòng)定理證明器的使用，并創(chuàng)建開放數(shù)據(jù)集，以支持全球自動(dòng)定理證明工作。

團(tuán)隊(duì)簡(jiǎn)介

安德烈·沃倫科夫（Andrei Voronkov）

安德烈· 沃倫科夫從7歲起就癡迷于證明定理，而從15歲第一次接觸穿孔卡片起，他同樣癡迷于編寫計(jì)算機(jī)程序。毫不奇怪，他的第一個(gè)非玩具計(jì)算機(jī)程序是一個(gè)用于證明定理的程序。

他對(duì)計(jì)算機(jī)定理證明的熱情促成了定理證明器Vampire的設(shè)計(jì)和初步開發(fā)，該程序自1999年以來(lái)在一階定理證明中贏得了70個(gè)世界冠軍頭銜。

他在自動(dòng)推理的諸多領(lǐng)域做出了貢獻(xiàn)，包括理論、實(shí)現(xiàn)技術(shù)和應(yīng)用。2007年，他為Vampire開發(fā)了首個(gè)基于機(jī)器學(xué)習(xí)的策略調(diào)度程序Spider（蜘蛛）。在業(yè)余時(shí)間，他還開發(fā)了會(huì)議管理系統(tǒng)EasyChair，該系統(tǒng)目前已被超過(guò)400萬(wàn)研究人員使用。

他認(rèn)為，當(dāng)數(shù)學(xué)家和計(jì)算機(jī)程序互相傳授數(shù)學(xué)知識(shí)、互相學(xué)習(xí)時(shí)，世界將會(huì)變得更加美好。他相信，最近在自動(dòng)推理領(lǐng)域發(fā)展起來(lái)的技術(shù)，例如理論推理和歸納法，能夠在未來(lái)20到50年內(nèi)引領(lǐng)計(jì)算機(jī)輔助數(shù)學(xué)的革命。

邁克爾·羅森（Michael Rawson）

邁克爾·羅森認(rèn)為計(jì)算機(jī)應(yīng)該能夠推理并從過(guò)去的經(jīng)驗(yàn)中學(xué)習(xí)。他對(duì)自動(dòng)定理證明尤其感興趣：能夠進(jìn)行嚴(yán)密邏輯論證的計(jì)算機(jī)系統(tǒng)。他是“古董吸血鬼”（Antique Vampires）團(tuán)隊(duì)的一員：該團(tuán)隊(duì)負(fù)責(zé)監(jiān)督和指導(dǎo)世界領(lǐng)先的定理證明器“吸血鬼”（Vampire）的設(shè)計(jì)和開發(fā)。

22、數(shù)學(xué)基準(zhǔn)（Mathbench）——評(píng)估自然語(yǔ)言證明

項(xiàng)目簡(jiǎn)介

MathBench項(xiàng)目旨在通過(guò)引入一個(gè)全新的帶注釋證明數(shù)據(jù)集，來(lái)提升AI模型在數(shù)學(xué)推理方面的評(píng)估能力。該數(shù)據(jù)集包含與多個(gè)不同證明配對(duì)的定理，每個(gè)證明被分解為關(guān)鍵步驟，并附有摘要、錯(cuò)誤論證和邏輯結(jié)構(gòu)元數(shù)據(jù)的注釋。通過(guò)利用MathBench，該項(xiàng)目旨在評(píng)估AI模型識(shí)別關(guān)鍵證明步驟、糾正錯(cuò)誤以及區(qū)分有效和無(wú)效證明的能力，從而了解大語(yǔ)言模型在數(shù)學(xué)推理和理解方面的能力。

團(tuán)隊(duì)簡(jiǎn)介

悉達(dá)多·巴特（Siddharth Bhat）

劍橋大學(xué)的博士生。他是形式化驗(yàn)證、函數(shù)式編程語(yǔ)言實(shí)現(xiàn)和應(yīng)用范疇論方面的專家。他是Lean定理證明器前20名貢獻(xiàn)者之一。他在高性能計(jì)算和循環(huán)優(yōu)化方面也擁有豐富的經(jīng)驗(yàn)。他的長(zhǎng)期愿景是構(gòu)建可擴(kuò)展的數(shù)學(xué)定理證明系統(tǒng)，并已為此發(fā)表了多項(xiàng)研究成果。

亞歷克斯·哈夫里拉（Alex Havrilla）

佐治亞理工學(xué)院數(shù)學(xué)與機(jī)器學(xué)習(xí)博士生。他的研究方向是生成模型的理論與實(shí)踐，重點(diǎn)是通過(guò)強(qiáng)化學(xué)習(xí)和合成數(shù)據(jù)改進(jìn)推理能力。他曾在Meta、微軟和谷歌實(shí)習(xí)，并共同創(chuàng)立了開源RLHF研究小組CarperAI。

斯特拉·比德曼（Stella Biderman）

EleutherAI的執(zhí)行董事，EleutherAI是一家由草根研究團(tuán)體轉(zhuǎn)型而來(lái)的非營(yíng)利性研究機(jī)構(gòu)，開創(chuàng)了現(xiàn)代開源AI運(yùn)動(dòng)。Stella在 GPT-Neo、Pythia、BLOOM、OpenFold和VQGAN-CLIP等模型上的工作，極大地提升了基礎(chǔ)模型的可訪問性，同時(shí)也為AI的透明度和開放科學(xué)樹立了標(biāo)桿。除了開發(fā)新模型外，Stella還投入了大量時(shí)間致力于開發(fā)開源AI庫(kù)、構(gòu)建和記錄公共數(shù)據(jù)集以及開展可解釋性研究。

帕萬(wàn)·薩?？āぐ⒙{曼奇（Pawan Sasanka Ammanamanchi）

Ritual的研究員，也是EleutherAI的志愿研究員。他擁有印度理工學(xué)院海得拉巴分校的碩士學(xué)位，專攻大語(yǔ)言模型的評(píng)估。他的貢獻(xiàn)包括BLOOM模型和GEM基準(zhǔn)測(cè)試。他尤其熱衷于推動(dòng)AI在數(shù)學(xué)領(lǐng)域的應(yīng)用。

23、AI和機(jī)器學(xué)習(xí)的新范疇和拓?fù)浠A(chǔ)

項(xiàng)目簡(jiǎn)介

該項(xiàng)目探索基于更定制的數(shù)學(xué)表示空間和結(jié)構(gòu)（包括層論sheaf theory和范疇論category theory）的新型神經(jīng)網(wǎng)絡(luò)架構(gòu)。這些新型架構(gòu)或許能夠融入數(shù)學(xué)對(duì)象的關(guān)鍵結(jié)構(gòu)對(duì)稱性和屬性，從而能夠創(chuàng)建輔助證明構(gòu)建的新工具，并提供超越當(dāng)前AI Copilot范式的實(shí)用優(yōu)勢(shì)。探索能夠在豐富類型理論中表示和操縱證明狀態(tài)的模型的可能性，或許能幫助我們彌合機(jī)器學(xué)習(xí)與傳統(tǒng)數(shù)學(xué)領(lǐng)域之間的差距。

團(tuán)隊(duì)簡(jiǎn)介

皮埃特羅·利奧（Pietro Lio）

劍橋大學(xué)計(jì)算機(jī)科學(xué)系的計(jì)算生物學(xué)教授，他于2004年加入該系任教。他最初在佛羅倫薩和帕維亞學(xué)習(xí)，專注于遺傳學(xué)和復(fù)雜系統(tǒng)，之后在南安普頓和劍橋擔(dān)任研究職位。他的工作重點(diǎn)是利用AI和計(jì)算生物學(xué)來(lái)理解疾病過(guò)程。

杰米·維卡里（Jamie Vicary）

劍橋大學(xué)計(jì)算機(jī)科學(xué)系未來(lái)計(jì)算教授。他獲得物理學(xué)和數(shù)學(xué)學(xué)士學(xué)位后，在牛津大學(xué)擔(dān)任計(jì)算機(jī)科學(xué)研究員十年，2018年加入伯明翰大學(xué)擔(dān)任高級(jí)講師，并于2020年調(diào)至劍橋大學(xué)任教。他的研究興趣廣泛，涵蓋量子計(jì)算、理論計(jì)算機(jī)科學(xué)和機(jī)器學(xué)習(xí)。

24、Polymath Plus（Polymath +）

項(xiàng)目簡(jiǎn)介

Polymath Plus是一個(gè)新一代在線協(xié)作平臺(tái)，它將大規(guī)模的人類互動(dòng)與基于AI的推理相結(jié)合，以推進(jìn)數(shù)學(xué)探索。在Polymath原項(xiàng)目的基礎(chǔ)上，它既利用AI作為管理員來(lái)管理討論，又利用AI作為協(xié)作者來(lái)貢獻(xiàn)想法并驗(yàn)證證明。Polymath Plus旨在將人類直覺與機(jī)器輔助的嚴(yán)謹(jǐn)性相結(jié)合，簡(jiǎn)化既定定理，解決尚未解決的挑戰(zhàn)，并加速數(shù)學(xué)界的協(xié)作。

團(tuán)隊(duì)簡(jiǎn)介

皮埃特羅·米切魯奇（Pietro Michelucci）

人類計(jì)算研究所的執(zhí)行主任，也是康奈爾大學(xué)的訪問學(xué)者。作為一名專注于人機(jī)混合智能的認(rèn)知科學(xué)家，他致力于運(yùn)用人機(jī)互補(bǔ)的優(yōu)勢(shì)來(lái)解決社會(huì)問題。他創(chuàng)立了“Stall Catchers”公民科學(xué)項(xiàng)目，并擔(dān)任《人類計(jì)算手冊(cè)》的編輯。

杰森·戴爾 (Jason Dyer)

在高中任教11年；在此期間，他參與了Polymath項(xiàng)目，該項(xiàng)目發(fā)現(xiàn)了Hales-Jewett定理密度版的新組合證明。之后，他加入了數(shù)學(xué)和科學(xué)學(xué)習(xí)應(yīng)用程序Brilliant.org，負(fù)責(zé)開發(fā)課程，并與服務(wù)成員安排小型Polymath項(xiàng)目。他目前為歐洲、北美和亞洲的客戶提供教育游戲設(shè)計(jì)咨詢服務(wù)。

薩姆·沙班（Sam Shaaban）

自1999年創(chuàng)立NuRelm以來(lái)，Sam Shaaban一直致力于為研究人員和創(chuàng)新者開發(fā)軟件。他熱衷于幫助創(chuàng)作者集思廣益、制作原型、制定預(yù)算并交付數(shù)字健康應(yīng)用程序、被動(dòng)傳感器數(shù)據(jù)收集系統(tǒng)、研究門戶、數(shù)據(jù)處理管道以及改善生活的創(chuàng)造性方法。

邁克爾·斯蒂爾曼（Michael Stillman）

本科就讀于伊利諾伊大學(xué)，研究生就讀于哈佛大學(xué)。在芝加哥大學(xué)、布蘭迪斯大學(xué)和麻省理工學(xué)院擔(dān)任博士后后，他加入康奈爾大學(xué)數(shù)學(xué)系任教。他的研究興趣圍繞計(jì)算代數(shù)幾何，包括算法、實(shí)現(xiàn)和應(yīng)用（例如生物學(xué)和理論物理學(xué)）。他是Macaulay2計(jì)算機(jī)代數(shù)系統(tǒng)的創(chuàng)始人之一。

格雷格·利普斯坦（Greg Lipstein）

DrivenData的聯(lián)合創(chuàng)始人兼負(fù)責(zé)人。DrivenData是一家致力于將AI的變革力量帶給應(yīng)對(duì)全球最嚴(yán)峻挑戰(zhàn)的組織的社會(huì)企業(yè)。DrivenData的競(jìng)賽平臺(tái)匯聚了全球數(shù)據(jù)科學(xué)家的技能和熱情，旨在構(gòu)建造福社會(huì)的解決方案。我們與杰出的社區(qū)以及NASA、微軟、Meta AI和世界銀行等組織合作，已提供超過(guò)480萬(wàn)美元的獎(jiǎng)金，評(píng)估了超過(guò)20萬(wàn)份參賽作品，并為公共服務(wù)、健康、科學(xué)、自然、教育等領(lǐng)域提供了先進(jìn)的解決方案。

蒂莫西·高爾斯（Timothy Gowers）

法蘭西學(xué)院的組合數(shù)學(xué)教授，同時(shí)兼任劍橋大學(xué)數(shù)學(xué)系教授和三一學(xué)院研究員。在劍橋大學(xué)，他領(lǐng)導(dǎo)著一個(gè)自動(dòng)定理證明小組，專注于理解人類數(shù)學(xué)家尋找證明的過(guò)程。他于1981年在國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）中獲得滿分，并于1998年因其在泛函分析和組合數(shù)學(xué)領(lǐng)域的杰出貢獻(xiàn)榮獲菲爾茲獎(jiǎng)。他是牛津通識(shí)讀本《數(shù)學(xué)：極簡(jiǎn)導(dǎo)論》Mathematics: A Very Short Introduction一書的作者，也是《普林斯頓數(shù)學(xué)指南》的主編。

25、通過(guò)數(shù)學(xué)數(shù)據(jù)庫(kù)進(jìn)行可擴(kuò)展定理證明

項(xiàng)目簡(jiǎn)介

該項(xiàng)目旨在通過(guò)在Lean數(shù)學(xué)庫(kù)(mathlib)和L-函數(shù)及模形式數(shù)據(jù)庫(kù)(LMFDB)之間建立接口，擴(kuò)大自動(dòng)定理證明器可訪問的數(shù)學(xué)內(nèi)容規(guī)模。通過(guò)將mathlib約10萬(wàn)個(gè)數(shù)學(xué)結(jié)果集合與LMFDB超過(guò)10億個(gè)具體語(yǔ)句的存儲(chǔ)庫(kù)連接起來(lái)，我們的目標(biāo)是擴(kuò)展人類數(shù)學(xué)家和AI智能體的能力。該項(xiàng)目將開發(fā)新的Lean策略，并建立一個(gè)將其他數(shù)學(xué)數(shù)據(jù)庫(kù)與形式化定理證明系統(tǒng)集成的框架，為可擴(kuò)展的數(shù)學(xué)發(fā)現(xiàn)鋪平道路。

團(tuán)隊(duì)簡(jiǎn)介

克里斯托弗·伯克貝克（Christopher Birkbeck）

東英吉利大學(xué)純數(shù)學(xué)講師，專攻數(shù)論。他的研究領(lǐng)域包括p進(jìn)模形式的研究和計(jì)算，目前的研究方向是數(shù)學(xué)形式化，專注于Lean中的模形式理論。伯克貝克在華威大學(xué)獲得博士學(xué)位，導(dǎo)師是拉西娜·登貝萊（Lassina Dembele）和約翰·克雷莫納（John Cremona），隨后在倫敦大學(xué)學(xué)院（UCL）獲得博士后研究資格。

大衛(wèi)·羅（David Roe）

麻省理工學(xué)院數(shù)學(xué)系的首席研究科學(xué)家，他研究計(jì)算數(shù)論和算術(shù)幾何，尤其關(guān)注p進(jìn)數(shù)（一種與實(shí)數(shù)類似但距離概念不同的數(shù)，用于測(cè)量被某個(gè)固定素?cái)?shù)整除的可能性）。p進(jìn)數(shù)在他為數(shù)學(xué)界構(gòu)建計(jì)算工具的歷程中扮演了核心角色，這始于他在SageMath中對(duì)p進(jìn)計(jì)算的研究。他擔(dān)任L-函數(shù)和模形式數(shù)據(jù)庫(kù)(LMFDB)的執(zhí)行編輯，該數(shù)據(jù)庫(kù)匯集了數(shù)論和算術(shù)幾何中出現(xiàn)的數(shù)學(xué)對(duì)象；他也是researchseminars.org的創(chuàng)始人之一，該網(wǎng)站是在疫情期間創(chuàng)建的，旨在幫助數(shù)學(xué)家參加在線研究研討會(huì)。

安德魯·薩瑟蘭（Andrew Sutherland）

麻省理工學(xué)院數(shù)學(xué)高級(jí)研究員，其研究項(xiàng)目專注于算術(shù)幾何和數(shù)論的計(jì)算方面。他在多項(xiàng)大型研究合作中發(fā)揮了重要作用，包括 “素?cái)?shù)間有界間隙”的Polymath項(xiàng)目 、 L-函數(shù)和模形式數(shù)據(jù)庫(kù)以及 “算術(shù)幾何、數(shù)論和計(jì)算”西蒙斯合作項(xiàng)目 。薩瑟蘭目前擔(dān)任《計(jì)算數(shù)學(xué)》Mathematics of Computation的編輯、《數(shù)論研究》Research in Number Theory的主編、《L-函數(shù)和模形式數(shù)據(jù)庫(kù)》 的執(zhí)行編輯、布朗大學(xué)數(shù)學(xué)計(jì)算與實(shí)驗(yàn)研究所的科學(xué)顧問委員會(huì)成員、數(shù)論基金會(huì)主席以及美國(guó)數(shù)學(xué)會(huì)會(huì)士。

26、畫板（Sketchpad）——高精度且易于使用的自動(dòng)形式草圖生成系統(tǒng)

項(xiàng)目簡(jiǎn)介

Sketchpad是一個(gè)由AI驅(qū)動(dòng)的系統(tǒng)，用于將自然語(yǔ)言證明轉(zhuǎn)換為結(jié)構(gòu)化的形式化草圖，旨在協(xié)助使用Isabelle和Lean進(jìn)行形式數(shù)學(xué)工作的從業(yè)者。通過(guò)引入基于圖形的表示，它能夠?qū)⒆C明分解為單個(gè)陳述，從而支持細(xì)粒度的自動(dòng)形式化，并與部分或不完整的證明進(jìn)行更高效的交互。

團(tuán)隊(duì)簡(jiǎn)介

Wenda Li（李文達(dá)——音譯）

愛丁堡大學(xué)混合AI助理教授，專攻數(shù)學(xué)AI。他為使用大語(yǔ)言模型進(jìn)行自動(dòng)形式化的開創(chuàng)性工作做出了貢獻(xiàn)，并探索了用非形式化證明指導(dǎo)形式化定理證明的方法。除此之外，他的工作還涵蓋了驗(yàn)證量詞消元法、格羅滕迪克的概形理論（scheme theory）以及解析數(shù)論的各個(gè)方面。他在這些領(lǐng)域的成就被評(píng)為BCS最佳論文獎(jiǎng)亞軍。

Mai Luo（羅麥——音譯）

愛丁堡大學(xué)副教授（西安電子科技大學(xué)學(xué)士、倫敦帝國(guó)理工學(xué)院碩博），領(lǐng)導(dǎo)大規(guī)模機(jī)器學(xué)習(xí)系統(tǒng)研究組。他擔(dān)任英國(guó)工程與物理研究理事會(huì)（EPSRC）機(jī)器學(xué)習(xí)系統(tǒng)博士培訓(xùn)中心聯(lián)合主任，以及英國(guó)ARIA項(xiàng)目“Scaling Compute – Charting the Course”的聯(lián)合負(fù)責(zé)人。他的研究涵蓋計(jì)算機(jī)系統(tǒng)、機(jī)器學(xué)習(xí)和數(shù)據(jù)管理。他領(lǐng)導(dǎo)的AI系統(tǒng)已被各大科技公司采用，并以開源軟件的形式廣泛發(fā)布，并獲得了廣泛的認(rèn)可。他是谷歌博士生獎(jiǎng)學(xué)金和微軟亞洲研究院StarTrack獎(jiǎng)的獲得者，并入圍了校長(zhǎng)新星研究獎(jiǎng)的最終角逐。

拉里·保爾森（Larry Paulson）

亞馬遜學(xué)者、劍橋大學(xué)計(jì)算邏輯榮譽(yù)教授，也是形式邏輯和證明助手領(lǐng)域的知名專家。他領(lǐng)導(dǎo)了廣泛使用的Isabelle證明助手的開發(fā)，并率先推出了Sledgehammer，這項(xiàng)突破性的創(chuàng)新已被幾乎所有主流證明助手所采用。為了表彰他對(duì)證明助手和自動(dòng)推理的杰出貢獻(xiàn)，他被選為ACM院士、皇家學(xué)會(huì)院士，并獲得了Herbrand獎(jiǎng)。

辛華劍

愛丁堡大學(xué)的博士生（本科畢業(yè)于中山大學(xué)邏輯學(xué)專業(yè)，目前是字節(jié)跳動(dòng)倫敦Seed實(shí)習(xí)生），與Jacques Fleuriot和Wenda Li合作。他的研究重點(diǎn)是使用大語(yǔ)言模型進(jìn)行自動(dòng)定理證明，尤其關(guān)注能夠自動(dòng)形式化和知識(shí)庫(kù)學(xué)習(xí)的自主智能體。他的代表作包括：最先進(jìn)的開源定理證明模型DeepSeek Prover系列；以任務(wù)分解和知識(shí)積累為特色的LEGO-Prover；以及用于庫(kù)級(jí)證明工程評(píng)估的基準(zhǔn)數(shù)據(jù)集APE-Bench。

27、邁向自動(dòng)化數(shù)學(xué)發(fā)現(xiàn)

項(xiàng)目簡(jiǎn)介

該項(xiàng)目探索了一個(gè)多智能體猜想器-證明器框架，該框架利用大語(yǔ)言模型(LLM) 在Lean定理證明器中生成并證明新穎的數(shù)學(xué)猜想。該框架從實(shí)用性和新穎性的角度量化和形式化“趣味性”的概念，旨在簡(jiǎn)化開放式數(shù)學(xué)探索和發(fā)現(xiàn)。通過(guò)對(duì)猜想器和證明器進(jìn)行迭代改進(jìn)，這種創(chuàng)新方法旨在推進(jìn)自動(dòng)化定理證明，并為新的數(shù)學(xué)見解的發(fā)展做出貢獻(xiàn)。

團(tuán)隊(duì)簡(jiǎn)介

亞倫·庫(kù)維爾（Aaron Courville）

蒙特利爾大學(xué)計(jì)算機(jī)科學(xué)與運(yùn)籌學(xué)系(DIRO)的教授，也是IVADO的科學(xué)主任。他擁有卡內(nèi)基梅隆大學(xué)機(jī)器人研究所的博士學(xué)位。Courville是深度學(xué)習(xí)的早期貢獻(xiàn)者：他是Mila——魁北克AI研究所的創(chuàng)始成員之一。他與Ian Goodfellow和Yoshua Bengio共同編寫了深度學(xué)習(xí)的開創(chuàng)性教科書。他目前的研究重點(diǎn)是深度學(xué)習(xí)模型和方法的開發(fā)。他對(duì)強(qiáng)化學(xué)習(xí)、多智能體強(qiáng)化學(xué)習(xí)、深度生成模型和推理尤其感興趣。

納文·戈亞爾（Navin Goyal）

1998年在孟買印度理工學(xué)院獲得理學(xué)學(xué)士學(xué)位，并于2005年在羅格斯大學(xué)獲得博士學(xué)位。在麥吉爾大學(xué)和佐治亞理工學(xué)院從事博士后研究后，他于2009年加入微軟印度研究院。他的研究始于理論計(jì)算機(jī)科學(xué)，研究范圍涵蓋算法設(shè)計(jì)和分析以及計(jì)算復(fù)雜性等諸多問題。逐漸地，他的工作轉(zhuǎn)向?qū)W習(xí)理論。他的理論研究有時(shí)涉及應(yīng)用數(shù)學(xué)各個(gè)領(lǐng)域的技術(shù)（例如組合學(xué)、信息論、傅里葉分析）。這使他對(duì)數(shù)學(xué)和理論計(jì)算機(jī)科學(xué)的多樣性和統(tǒng)一性產(chǎn)生了濃厚的興趣。最近，他一直在進(jìn)行實(shí)證研究，從多個(gè)角度理解神經(jīng)網(wǎng)絡(luò)，包括其歸納偏差和對(duì)其內(nèi)部工作原理的解釋，以及其解決數(shù)學(xué)問題的能力。他對(duì)數(shù)學(xué)和其他領(lǐng)域的人們?nèi)绾稳〉眯掳l(fā)現(xiàn)非常感興趣。

28、犢皮紙（Vellum）——AI輔助形式推理的可擴(kuò)展框架

項(xiàng)目簡(jiǎn)介

Vellum項(xiàng)目構(gòu)建了一個(gè)開源框架，其中大語(yǔ)言模型 (LLM) 充當(dāng)規(guī)劃器，并與多個(gè)交互式定理證明器 (ITP) 和自動(dòng)求解器交互，旨在簡(jiǎn)化數(shù)學(xué)探索和證明過(guò)程。通過(guò)與不同類型的求解器和工具交互，Vellum促進(jìn)了大規(guī)模的AI輔助形式推理，從而簡(jiǎn)化了自然語(yǔ)言陳述的自動(dòng)形式化，并顯著降低了數(shù)學(xué)推理研究的門檻。

團(tuán)隊(duì)簡(jiǎn)介

斯瓦拉特·喬杜里（Swarat Chaudhuri）

德克薩斯大學(xué)奧斯汀分校計(jì)算機(jī)科學(xué)教授，同時(shí)也是谷歌Deepmind的研究科學(xué)家。他的研究融合了自動(dòng)推理、機(jī)器學(xué)習(xí)和編程語(yǔ)言的理念，旨在創(chuàng)建功能強(qiáng)大、可靠、透明且安全的AI系統(tǒng)。Chaudhuri博士于2001年獲得印度理工學(xué)院（Kharagpur）計(jì)算機(jī)科學(xué)學(xué)士學(xué)位，并于2007年獲得賓夕法尼亞大學(xué)計(jì)算機(jī)科學(xué)博士學(xué)位。他是2025年古根海姆學(xué)者，并曾獲得美國(guó)國(guó)家科學(xué)基金會(huì)杰出人才獎(jiǎng)、ACM SIGPLAN John Reynolds論文獎(jiǎng)、賓夕法尼亞大學(xué)Morris and Dorothy Rubinoff論文獎(jiǎng)、Meta獎(jiǎng)和谷歌研究獎(jiǎng)，以及多項(xiàng)ACM SIGPLAN和SIGSOFT杰出論文獎(jiǎng)。 Chaudhuri博士曾擔(dān)任機(jī)器學(xué)習(xí)、形式化方法和編程語(yǔ)言領(lǐng)域所有主要會(huì)議的項(xiàng)目委員會(huì)成員，并擔(dān)任CAV 2016和ICLR 2024的項(xiàng)目主席。

宋曉冬（Dawn Song）

加州大學(xué)伯克利分校計(jì)算機(jī)科學(xué)教授（1974年出生于遼寧營(yíng)口，清華大學(xué)物理系學(xué)士，卡內(nèi)基梅隆大學(xué)計(jì)算機(jī)系碩士，加州大學(xué)伯克利分校博士），伯克利負(fù)責(zé)任去中心化智能中心聯(lián)合主任。她的研究領(lǐng)域包括AI與深度學(xué)習(xí)、安全與隱私以及去中心化技術(shù)。她曾獲得多項(xiàng)獎(jiǎng)項(xiàng)，包括麥克阿瑟獎(jiǎng)、古根海姆獎(jiǎng)、美國(guó)國(guó)家科學(xué)基金會(huì)杰出青年獎(jiǎng)、阿爾弗雷德·P·斯隆研究獎(jiǎng)、《麻省理工科技評(píng)論》TR-35獎(jiǎng)、ACM SIGSAC杰出創(chuàng)新獎(jiǎng)，以及十余項(xiàng)計(jì)算機(jī)安全和深度學(xué)習(xí)領(lǐng)域頂級(jí)會(huì)議的“經(jīng)得起時(shí)間考驗(yàn)”獎(jiǎng)和最佳論文獎(jiǎng)。她是計(jì)算機(jī)安全領(lǐng)域被引用次數(shù)最多的學(xué)者，被評(píng)為最具影響力學(xué)者（AMiner獎(jiǎng)）。她是ACM會(huì)士和IEEE會(huì)士，也是美國(guó)藝術(shù)與科學(xué)學(xué)院當(dāng)選院士。她在加州大學(xué)伯克利分校獲得博士學(xué)位。她還是一位連續(xù)創(chuàng)業(yè)者，并被《Inc.》雜志評(píng)選為百?gòu)?qiáng)女性創(chuàng)始人，并被《Wired25》評(píng)選為創(chuàng)新者。

何靜軒

加州大學(xué)伯克利分校的博士后研究員。他的研究領(lǐng)域廣泛，涵蓋計(jì)算機(jī)安全、機(jī)器學(xué)習(xí)和編程語(yǔ)言，近期專注于提升AI軟件程序的安全性和可靠性。他于蘇黎世聯(lián)邦理工學(xué)院獲得博士學(xué)位，并榮獲蘇黎世聯(lián)邦理工學(xué)院杰出博士論文獎(jiǎng)?wù)隆Ｋ€曾榮獲ACM CCS 2023杰出論文獎(jiǎng)。

Zhe Ye（葉哲——音譯）

加州大學(xué)伯克利分校和伯克利研發(fā)中心的博士生（上?？萍即髮W(xué)信息科學(xué)與技術(shù)學(xué)院計(jì)算機(jī)科學(xué)學(xué)士）。他的研究方向包括大語(yǔ)言模型輔助形式化驗(yàn)證、形式化規(guī)范合成和計(jì)算機(jī)安全。他在相關(guān)領(lǐng)域發(fā)表了多篇論文，其中一些已被IEEE S&P和ISSTA等頂級(jí)會(huì)議錄用。

阿米塔尤什·塔庫(kù)爾（Amitayush Thakur）

德克薩斯大學(xué)奧斯汀分校的博士生，致力于“數(shù)學(xué)AI”和“代碼AI”的交叉研究。他的興趣在于通過(guò)大語(yǔ)言模型進(jìn)行自動(dòng)化數(shù)學(xué)推理，以及其在完全驗(yàn)證的程序合成中的意義，這對(duì)于從AI生成工業(yè)級(jí)代碼至關(guān)重要。他是Copra（一個(gè)用于形式化定理證明的智能體框架）的首席開發(fā)者。加入德克薩斯大學(xué)之前，他曾在微軟擔(dān)任軟件工程師，此前曾在微軟研究院擔(dān)任研究實(shí)習(xí)生。

喬治·蘇卡拉斯（George Tsoukalas）

德克薩斯大學(xué)奧斯汀分校的博士生，致力于研究用于自動(dòng)數(shù)學(xué)推理和程序合成的神經(jīng)符號(hào)技術(shù)。他領(lǐng)導(dǎo)創(chuàng)建了PutnamBench，這是一個(gè)前沿的AI數(shù)學(xué)基準(zhǔn)測(cè)試，并在ICML 2024 AI數(shù)學(xué)研討會(huì)上榮獲最佳論文獎(jiǎng)。他還為COPRA做出了貢獻(xiàn)，COPRA是一種基于智能體的LLM形式化定理證明方法。

參考資料

https://www.renaissancephilanthropy.org/ai-for-math-fund-projects

https://www.renaissancephilanthropy.org/news-and-insights/ai-for-math-fund-announces-18-million-in-grants-to-accelerate-breakthrough-discoveries-in-mathematicsnbsp

小樂數(shù)學(xué)科普近期文章

出版社和作家自薦通道

小樂數(shù)學(xué)科普薦書

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點(diǎn)擊zzllrr小樂

公眾號(hào)主頁(yè)

加星★

數(shù)學(xué)科普不迷路！