2022年11月，ChatGPT的發(fā)布如同一顆石子投入湖心，在全球范圍內(nèi)激起了大語(yǔ)言模型的浪潮。一年后的2023年，在復(fù)旦校園里，一支名為“數(shù)院大神”的學(xué)生志愿團(tuán)隊(duì)，迎來(lái)成立10周年的日子。
十多年來(lái)，這支來(lái)自復(fù)旦數(shù)學(xué)科學(xué)學(xué)院的團(tuán)隊(duì)，為超過(guò)12000名同學(xué)提供數(shù)學(xué)學(xué)習(xí)支持，累計(jì)志愿服務(wù)超過(guò)16000個(gè)小時(shí)。2025年，他們又一次獲評(píng)復(fù)旦大學(xué)“十佳志愿服務(wù)先進(jìn)集體”。
然而，大模型時(shí)代的到來(lái)，也給團(tuán)隊(duì)帶來(lái)了新的思考。作為上海數(shù)學(xué)中心2025級(jí)直博生、“數(shù)院大神”團(tuán)隊(duì)負(fù)責(zé)人的馬行健與成員們不禁自問(wèn)：如果未來(lái)AI能實(shí)現(xiàn)全天候、跨學(xué)科的即時(shí)答疑，“數(shù)院大神”將如何持續(xù)發(fā)揮價(jià)值？
為此，團(tuán)隊(duì)對(duì)各類(lèi)大模型開(kāi)展深入測(cè)評(píng)，結(jié)果發(fā)現(xiàn)：面對(duì)“實(shí)變函數(shù)學(xué)十遍，泛函分析心泛寒”這類(lèi)讓數(shù)院學(xué)子也犯難的數(shù)學(xué)專(zhuān)業(yè)課，其抽象與艱深也讓大模型“幻覺(jué)”頻生，給出的答案常常出現(xiàn)邏輯跳躍或步驟缺失，看似合理卻難以推敲，有時(shí)甚至調(diào)用超綱知識(shí)，讓初學(xué)者無(wú)從跟進(jìn)，也難以自我評(píng)估。
正是看到通用模型局限與團(tuán)隊(duì)轉(zhuǎn)型的需要，馬行健與隊(duì)員們決定發(fā)揮數(shù)學(xué)專(zhuān)長(zhǎng)，探索AI與教學(xué)的深度融合，打造一個(gè)真正“懂?dāng)?shù)學(xué)”的智能輔助平臺(tái)——AI4Math應(yīng)運(yùn)而生。
這一設(shè)想迅速獲得學(xué)院公共數(shù)學(xué)教研室、學(xué)工團(tuán)隊(duì)及學(xué)校人工智能教育教學(xué)創(chuàng)新中心的認(rèn)可與支持，為項(xiàng)目落地鋪平道路。
瞄準(zhǔn)兩大教學(xué)痛點(diǎn)
參與AI4Math的“數(shù)院大神”成員，都有豐富的答疑或授課經(jīng)歷。
馬行健大一加入“大神體驗(yàn)崗”，大二成為正式隊(duì)員，大三時(shí)已擔(dān)任團(tuán)隊(duì)負(fù)責(zé)人與高等數(shù)學(xué)習(xí)題課老師。這種既是學(xué)生、又當(dāng)“老師”的雙重身份，讓他能同時(shí)理解學(xué)習(xí)者的困惑，也從授課者視角出發(fā)，去設(shè)計(jì)一套科學(xué)的數(shù)字方案。
馬行健（左）正在答疑
在數(shù)學(xué)科學(xué)學(xué)院謝納慶教授領(lǐng)銜的公共數(shù)學(xué)教研室的支持下，團(tuán)隊(duì)充分吸收學(xué)院在高等數(shù)學(xué)數(shù)字化建設(shè)中積累的經(jīng)驗(yàn)與一線(xiàn)教學(xué)反饋，最終瞄準(zhǔn)了兩個(gè)核心教學(xué)痛點(diǎn)：一是學(xué)習(xí)診斷閉環(huán)缺失，快節(jié)奏的標(biāo)準(zhǔn)化課程使得同學(xué)們“學(xué)完即忘”，師生互動(dòng)不足也導(dǎo)致難以及時(shí)給予學(xué)習(xí)反饋，讓同學(xué)們“不知學(xué)了什么、不知學(xué)的如何、不知為何而學(xué)”。
二是大模型數(shù)學(xué)推理的可信度問(wèn)題。“簡(jiǎn)單來(lái)說(shuō)，大模型的輸出來(lái)自概率化的生成機(jī)制，更擅長(zhǎng)給出‘看起來(lái)最可能’的推導(dǎo)表達(dá)，而不是自動(dòng)確保每一步都滿(mǎn)足嚴(yán)格的邏輯約束?！彼忉尩?，“因此在證明題里，一旦出現(xiàn)跳步或漏條件，對(duì)初學(xué)者可能適得其反?！?/p>
基于此，AI4Math項(xiàng)目設(shè)定三大目標(biāo)：讓同學(xué)們能夠看見(jiàn)知識(shí)結(jié)構(gòu)、了解學(xué)習(xí)進(jìn)展、相信模型推理。
“學(xué)生主導(dǎo)開(kāi)發(fā)的產(chǎn)品，其優(yōu)勢(shì)在于需求來(lái)源于學(xué)生長(zhǎng)期參與一線(xiàn)教輔工作的經(jīng)驗(yàn)?！?項(xiàng)目指導(dǎo)教師、計(jì)算與智能創(chuàng)新學(xué)院副教授、人工智能教育教學(xué)創(chuàng)新中心副主任朱東來(lái)評(píng)價(jià)道，“這與教學(xué)專(zhuān)家和授課教師的角度有明顯不同，同時(shí)又結(jié)合了數(shù)學(xué)形式化證明方面的專(zhuān)業(yè)知識(shí)，具有一定的先進(jìn)性。”
來(lái)自一線(xiàn)教學(xué)積累的數(shù)據(jù)底氣
如何實(shí)現(xiàn)目標(biāo)？馬行健與團(tuán)隊(duì)擁有大模型時(shí)代最珍貴的資源——長(zhǎng)期積累的教學(xué)與答疑實(shí)踐數(shù)據(jù)。
“AI4Math項(xiàng)目的數(shù)據(jù)基礎(chǔ)是數(shù)院和‘?dāng)?shù)院大神’團(tuán)隊(duì)的長(zhǎng)期積累，主要來(lái)自進(jìn)階數(shù)學(xué)教材評(píng)述體系、真題與習(xí)題精講資源庫(kù)、結(jié)構(gòu)化筆記與專(zhuān)題講座資源、進(jìn)階學(xué)習(xí)誤區(qū)數(shù)據(jù)庫(kù)這四個(gè)方面”，馬行健介紹。
其中，教材評(píng)述體系尤為珍貴，由數(shù)學(xué)科學(xué)學(xué)院的教授團(tuán)隊(duì)親自參與構(gòu)建。這一體系系統(tǒng)整合《微積分》《線(xiàn)性代數(shù)》等12門(mén)經(jīng)典數(shù)學(xué)課程的107本教材評(píng)述，是同學(xué)們打基礎(chǔ)的重要依托。
真題與習(xí)題精講資源庫(kù)的構(gòu)建，源自“數(shù)院大神”團(tuán)隊(duì)在指導(dǎo)老師、2025級(jí)輔導(dǎo)員丁宇哲推動(dòng)下持續(xù)數(shù)年的沉淀與系統(tǒng)梳理。資源庫(kù)整合了超過(guò)500期“每日一題/每周好題”，收錄多門(mén)數(shù)學(xué)專(zhuān)業(yè)進(jìn)階課程近年真題，以及全國(guó)大學(xué)生數(shù)學(xué)競(jìng)賽專(zhuān)題題庫(kù)，形成一套覆蓋廣泛、內(nèi)容精煉的學(xué)習(xí)資源體系。
“這些數(shù)據(jù)是我們?cè)陂L(zhǎng)期工作過(guò)程中積累下來(lái)的獨(dú)特財(cái)富?！瘪R行健說(shuō)。與互聯(lián)網(wǎng)上廣泛流通的公開(kāi)資料不同，這些資源經(jīng)過(guò)“數(shù)院大神”團(tuán)隊(duì)的反復(fù)驗(yàn)證和整理，質(zhì)量更高，針對(duì)性更強(qiáng)。
團(tuán)隊(duì)還依托“香蕉空間”建立子空間，積累了結(jié)構(gòu)化的課程筆記與習(xí)題解答，并整合了“數(shù)海啟航”討論班講義和復(fù)習(xí)講座資料。這些并非簡(jiǎn)單的課堂記錄，而是經(jīng)過(guò)系統(tǒng)梳理、便于復(fù)習(xí)和查詢(xún)的知識(shí)集合。
此外，團(tuán)隊(duì)持續(xù)記錄學(xué)生在進(jìn)階課程中的高頻疑問(wèn)，逐步構(gòu)建起“進(jìn)階學(xué)習(xí)誤區(qū)數(shù)據(jù)庫(kù)”?！斑@個(gè)數(shù)據(jù)庫(kù)是持續(xù)更新的，我們會(huì)在每次授課中不斷補(bǔ)充完善。”馬行健表示。
自研形式化語(yǔ)言Litex
為了更好地解決現(xiàn)有大模型存在的“幻覺(jué)”問(wèn)題，在朱東來(lái)的建議與幫助下，馬行健為AI4Math項(xiàng)目組建了一支跨學(xué)科團(tuán)隊(duì)。
23級(jí)數(shù)學(xué)科學(xué)學(xué)院博士生、AI Lab實(shí)習(xí)生沈嘉辰帶領(lǐng)小組，負(fù)責(zé)推進(jìn)自研形式化語(yǔ)言Litex的開(kāi)發(fā)；22級(jí)數(shù)學(xué)科學(xué)學(xué)院本科生、“數(shù)院大神”團(tuán)隊(duì)負(fù)責(zé)人李昕昊帶領(lǐng)小組，負(fù)責(zé)基于團(tuán)隊(duì)原有數(shù)據(jù)的進(jìn)一步數(shù)據(jù)集制作；馬行健負(fù)責(zé)的“形式化語(yǔ)言與大模型微調(diào)”討論班，吸引多位來(lái)自數(shù)學(xué)科學(xué)學(xué)院、計(jì)算與智能創(chuàng)新學(xué)院等院系的本科生以及研究生共同參與，通過(guò)閱讀文獻(xiàn)與動(dòng)手實(shí)踐，研究如何將形式化語(yǔ)言用于解決“幻覺(jué)”問(wèn)題并增強(qiáng)大模型推理以及教學(xué)能力，這種交叉融合也為項(xiàng)目注入了獨(dú)特優(yōu)勢(shì)。
“團(tuán)隊(duì)面臨的首要課題是如何在現(xiàn)有大模型技術(shù)基礎(chǔ)上實(shí)現(xiàn)自主創(chuàng)新。”馬行健坦言。團(tuán)隊(duì)選擇了“深耕既有研究，尋求差異突破”的策略，希望站在巨人的肩膀上，先把國(guó)內(nèi)外頂尖數(shù)學(xué)大模型的研究“完完全全深入學(xué)習(xí)一遍”，再尋找突破點(diǎn)。
對(duì)抗大模型在數(shù)學(xué)推理中的“幻覺(jué)”，也是AI4Math必須攻克的核心難題。馬行健對(duì)此有清醒認(rèn)識(shí)：“目前已有的工作暫時(shí)沒(méi)有完全解決這個(gè)問(wèn)題?！币虼?，團(tuán)隊(duì)正在探索一條不完全相同的技術(shù)路徑。
朱東來(lái)對(duì)此表示認(rèn)同：“對(duì)抗大模型‘幻覺(jué)’是目前學(xué)術(shù)界比較有挑戰(zhàn)的問(wèn)題。在數(shù)學(xué)大模型這個(gè)細(xì)分領(lǐng)域，目前一種可能的思路是將形式化語(yǔ)言與大模型相結(jié)合，實(shí)現(xiàn)數(shù)學(xué)推理的可驗(yàn)證性?！?/p>
為此，團(tuán)隊(duì)嘗試邁出了大膽的一步——自主研發(fā)形式化語(yǔ)言Litex，將數(shù)學(xué)證明過(guò)程轉(zhuǎn)化為計(jì)算機(jī)可驗(yàn)證的代碼。
“像Lean4這樣的現(xiàn)有形式化語(yǔ)言已經(jīng)比較成熟，但學(xué)習(xí)成本高，”馬行健介紹，“沈嘉辰學(xué)長(zhǎng)選擇了一個(gè)與傳統(tǒng)形式化語(yǔ)言不同的新體系，在開(kāi)發(fā)時(shí)更兼顧與自然語(yǔ)言的相似度，目標(biāo)是保持嚴(yán)謹(jǐn)?shù)耐瑫r(shí)，大幅降低表達(dá)和學(xué)習(xí)難度，把學(xué)習(xí)門(mén)檻縮短到小時(shí)級(jí)別?！?/p>
這門(mén)語(yǔ)言目前已在GitHub開(kāi)源，并登上Hacker News全球趨勢(shì)榜前十，引發(fā)全球開(kāi)發(fā)者圍繞形式化語(yǔ)言可用性的討論。核心開(kāi)發(fā)者沈嘉辰在相關(guān)文章中寫(xiě)道：“Litex致力于將形式化證明學(xué)習(xí)周期從傳統(tǒng)的3-6個(gè)月縮短至1-2小時(shí)，讓形式化推理過(guò)程變得如同編寫(xiě)數(shù)學(xué)算式一般自然?！?/p>
六大功能支持從智能答疑到個(gè)性化學(xué)習(xí)路徑搭建
2025年5月，“數(shù)院大神”團(tuán)隊(duì)?wèi){借AI4Math項(xiàng)目的初始版本“登堂入釋——定制你的數(shù)學(xué)個(gè)性學(xué)習(xí)管家”榮獲復(fù)旦大學(xué)首屆AI應(yīng)用開(kāi)發(fā)大賽金獎(jiǎng)，這次經(jīng)歷不僅驗(yàn)證了技術(shù)路線(xiàn)的可行性，更跑通了“從數(shù)據(jù)到服務(wù)”的工作流模式，為后續(xù)發(fā)展積累了關(guān)鍵經(jīng)驗(yàn)。
基于扎實(shí)的數(shù)據(jù)基礎(chǔ)和技術(shù)創(chuàng)新，AI4Math平臺(tái)在此基礎(chǔ)上開(kāi)發(fā)完善了智能答疑、答案評(píng)估、定理查詢(xún)、學(xué)術(shù)檢索、個(gè)性推薦和學(xué)情分析等六大核心功能。
學(xué)生可以上傳題目照片獲得解答思路，也可以提交自己的解題步驟獲得邏輯完整性評(píng)估。平臺(tái)還接入arXiv全球論文庫(kù)，支持學(xué)術(shù)檢索與前沿論文推薦。
“根據(jù)使用學(xué)生的過(guò)往問(wèn)答數(shù)據(jù)，平臺(tái)能生成個(gè)性化的能力評(píng)估報(bào)告，并推薦適合的題目和教材?！瘪R行健演示道，“我們還提供了知識(shí)圖譜，清晰展示知識(shí)點(diǎn)之間的關(guān)聯(lián)，如推出、包含、前提等關(guān)系?！被谶@些深度的關(guān)聯(lián)性分析，當(dāng)檢測(cè)到學(xué)生在某個(gè)知識(shí)點(diǎn)上存在薄弱環(huán)節(jié)時(shí)，平臺(tái)能夠給出一些學(xué)習(xí)建議。
團(tuán)隊(duì)希望平臺(tái)不僅能覆蓋基礎(chǔ)數(shù)學(xué)課程，還能支持高年級(jí)數(shù)學(xué)專(zhuān)業(yè)課。“對(duì)于‘實(shí)變函數(shù)’、‘泛函分析’這些硬課，希望我們獨(dú)特的結(jié)構(gòu)化筆記和題庫(kù)能夠在未來(lái)起到作用?！?馬行健說(shuō)。
一種“師生共創(chuàng)”新范式
項(xiàng)目能夠順利推進(jìn)，離不開(kāi)“師生共創(chuàng)”模式的支持。
“我們的項(xiàng)目入選了復(fù)旦大學(xué)人工智能教育教學(xué)創(chuàng)新中心的‘AI+師生共創(chuàng)重點(diǎn)項(xiàng)目’，學(xué)校給了我們師資、算力和資金等多方面的支持?！瘪R行健說(shuō)。
“這種模式打破了以往高?！處熤鲗?dǎo)、科研導(dǎo)向’的常規(guī)路徑，構(gòu)建起‘師生共創(chuàng)、場(chǎng)景驅(qū)動(dòng)’的新范式。從教師側(cè)來(lái)看，從單純的知識(shí)傳授者轉(zhuǎn)變?yōu)閷W(xué)生學(xué)習(xí)的設(shè)計(jì)者、引導(dǎo)者和協(xié)同創(chuàng)新者；從學(xué)生側(cè)來(lái)看，核心在于讓學(xué)生在解決真實(shí)問(wèn)題的過(guò)程中，實(shí)現(xiàn)能力結(jié)構(gòu)的整體升級(jí)?！敝鞏|來(lái)在項(xiàng)目中主要提供三方面支持：明晰應(yīng)用場(chǎng)景和需求、指導(dǎo)技術(shù)路線(xiàn)和框架、協(xié)助對(duì)接開(kāi)發(fā)和算力資源。
“我不給團(tuán)隊(duì)下指令、做決定，而是以提問(wèn)題、給建議為主?！彼窒?，當(dāng)團(tuán)隊(duì)提交早期的功能列表和界面設(shè)計(jì)后，他引導(dǎo)團(tuán)隊(duì)思考潛在用戶(hù)有哪些、他們會(huì)通過(guò)什么方式使用、希望達(dá)到什么目標(biāo)……這種引導(dǎo)幫助沒(méi)有系統(tǒng)開(kāi)發(fā)經(jīng)驗(yàn)的學(xué)生團(tuán)隊(duì)逐步完善了產(chǎn)品設(shè)計(jì)。
對(duì)馬行健來(lái)說(shuō)，參與這個(gè)項(xiàng)目帶來(lái)的成長(zhǎng)是全方位的?！耙环矫妫屛疑钤竽Ｐ图夹g(shù)前沿，完成了深度的相關(guān)知識(shí)網(wǎng)絡(luò)構(gòu)建；另一方面，它也鍛煉了我獨(dú)立開(kāi)展研究和團(tuán)隊(duì)管理的能力?！?/p>
目前，AI4Math平臺(tái)已在復(fù)旦大學(xué)校園ehall平臺(tái)的“智匯島”和AI3A共創(chuàng)平臺(tái)上線(xiàn)，并在《高等數(shù)學(xué)（D）》的班級(jí)中進(jìn)行了初步試用，正在收集師生使用反饋。下一學(xué)期將逐步擴(kuò)展至《高等數(shù)學(xué)》《線(xiàn)性代數(shù)》，再之后將面向數(shù)學(xué)專(zhuān)業(yè)課。
談及未來(lái)，團(tuán)隊(duì)有著明確規(guī)劃：推動(dòng)數(shù)學(xué)課程教學(xué)向智能化、精準(zhǔn)化和規(guī)?；?jí)，并在此基礎(chǔ)上推動(dòng)數(shù)學(xué)形式化證明與數(shù)學(xué)大模型的科研突破。
“我們希望這個(gè)平臺(tái)能服務(wù)更多同學(xué)，真正實(shí)現(xiàn)多覆蓋、全天候、個(gè)性化的智能化教學(xué)，從‘被替代’到‘全面升級(jí)’?！?/strong>馬行健說(shuō)。
