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

接上文

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

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

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

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

項目簡介

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

團(tuán)隊簡介

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

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

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

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

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

邁克爾·羅森（Michael Rawson）

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

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

項目簡介

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

團(tuán)隊簡介

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

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

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

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

斯特拉·比德曼（Stella Biderman）

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

帕萬·薩?？āぐ⒙{曼奇（Pawan Sasanka Ammanamanchi）

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

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

項目簡介

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

團(tuán)隊簡介

皮埃特羅·利奧（Pietro Lio）

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

杰米·維卡里（Jamie Vicary）

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

24、Polymath Plus（Polymath +）

項目簡介

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

團(tuán)隊簡介

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

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

杰森·戴爾 (Jason Dyer)

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

薩姆·沙班（Sam Shaaban）

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

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

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

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

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

蒂莫西·高爾斯（Timothy Gowers）

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

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

項目簡介

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

團(tuán)隊簡介

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

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

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

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

安德魯·薩瑟蘭（Andrew Sutherland）

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

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

項目簡介

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

團(tuán)隊簡介

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

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

Mai Luo（羅麥——音譯）

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

拉里·保爾森（Larry Paulson）

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

辛華劍

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

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

項目簡介

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

團(tuán)隊簡介

亞倫·庫維爾（Aaron Courville）

蒙特利爾大學(xué)計算機(jī)科學(xué)與運籌學(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)性教科書。他目前的研究重點是深度學(xué)習(xí)模型和方法的開發(fā)。他對強(qiáng)化學(xué)習(xí)、多智能體強(qiáng)化學(xué)習(xí)、深度生成模型和推理尤其感興趣。

納文·戈亞爾（Navin Goyal）

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

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

項目簡介

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

團(tuán)隊簡介

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

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

宋曉冬（Dawn Song）

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

何靜軒

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

Zhe Ye（葉哲——音譯）

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

阿米塔尤什·塔庫爾（Amitayush Thakur）

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

喬治·蘇卡拉斯（George Tsoukalas）

德克薩斯大學(xué)奧斯汀分校的博士生，致力于研究用于自動數(shù)學(xué)推理和程序合成的神經(jīng)符號技術(shù)。他領(lǐng)導(dǎo)創(chuàng)建了PutnamBench，這是一個前沿的AI數(shù)學(xué)基準(zhǔn)測試，并在ICML 2024 AI數(shù)學(xué)研討會上榮獲最佳論文獎。他還為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é)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

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

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

加星★

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