上海交通大學(xué)“AI4Math：Lean4與數(shù)學(xué)形式化”暑期學(xué)校報(bào)名通知

發(fā)布時(shí)間：2025-05-23 編輯：保研喵

添加上海交通大學(xué)學(xué)姐微信，或微信搜索公眾號(hào)“保研喵”，關(guān)注[保研喵]微信公眾號(hào)，在保研喵微信號(hào)輸入[上海交通大學(xué)保研夏令營(yíng)條件、上海交通大學(xué)保研加分細(xì)則、上海交通大學(xué)保研群、上海交通大學(xué)保研學(xué)姐微信、上海交通大學(xué)保研真題、上海交通大學(xué)夏令營(yíng)]即可在手機(jī)上查看相對(duì)應(yīng)上海交通大學(xué)保研信息和免費(fèi)資源。
回復(fù)[夏令營(yíng)信息][保研去向][保研來(lái)源][入營(yíng)名單]即可查看蕞新蕞全的保研數(shù)據(jù)。

上海交通大學(xué)“AI4Math：Lean4與數(shù)學(xué)形式化”暑期學(xué)校報(bào)名通知內(nèi)容如下，更多考研資訊請(qǐng)關(guān)注我們網(wǎng)站的更新！敬請(qǐng)收藏本站，或下載我們的考研派APP和考研派微信公眾號(hào)。

上海交通大學(xué)“AI4Math：Lean4與數(shù)學(xué)形式化”暑期學(xué)校報(bào)名通知 正文

 

近年來(lái)，大語(yǔ)言模型的推理能力，尤其是在數(shù)學(xué)問(wèn)題求解和證明中的應(yīng)用成為一大研究熱點(diǎn)。然而，數(shù)學(xué)對(duì)推理的嚴(yán)謹(jǐn)性要求極高，單純依賴語(yǔ)言模型極易出現(xiàn)幻覺(jué)等錯(cuò)誤。如何將數(shù)學(xué)的知識(shí)與邏輯融入大語(yǔ)言模型，以消除幻覺(jué)、提升推理能力和保證嚴(yán)謹(jǐn)性受到日益增加的關(guān)注。過(guò)去幾年，數(shù)學(xué)形式化逐漸成為一個(gè)被廣泛采用的可行途徑。目前，數(shù)學(xué)形式化的主要工具為L(zhǎng)ean4等，該語(yǔ)言功能強(qiáng)大，但入門門檻較高，限制了它的普及度。
基于上述背景，上海交通大學(xué)數(shù)學(xué)科學(xué)學(xué)院機(jī)器學(xué)習(xí)研究所、自然科學(xué)研究院，北京大學(xué)國(guó)際數(shù)學(xué)研究中心和國(guó)際機(jī)器學(xué)習(xí)研究中心擬聯(lián)合舉辦“AI4Math：Lean4與數(shù)學(xué)形式化”暑期學(xué)校，以推廣Lean4語(yǔ)言和數(shù)學(xué)形式化，推動(dòng)AI4Math的發(fā)展。本次暑期學(xué)校將包含兩個(gè)專題，分別為專題一：Lean4基礎(chǔ)和專題二：數(shù)值代數(shù)形式化。
組織者：
羅濤，上海交通大學(xué)數(shù)學(xué)科學(xué)學(xué)院副教授
梁經(jīng)緯，上海交通大學(xué)自然科學(xué)研究院副教授
董彬，北京大學(xué)國(guó)際數(shù)學(xué)研究中心教授
文再文，北京大學(xué)國(guó)際數(shù)學(xué)研究中心教授
專題一： Lean4基礎(chǔ)
時(shí)間：2025年7月14 - 20日
規(guī)模：計(jì)劃招生人數(shù)為25人。
一、報(bào)名條件
1.數(shù)學(xué)或計(jì)算機(jī)科學(xué)等相關(guān)專業(yè)的本科生或低年級(jí)研究生。
2.具有較強(qiáng)的數(shù)學(xué)素養(yǎng)，對(duì)數(shù)學(xué)形式化感興趣。
3.具備一定編程基礎(chǔ)的學(xué)生優(yōu)先考慮。
二、食宿安排
為非上海地區(qū)的學(xué)生提供住宿補(bǔ)助1000元，為所有同學(xué)提供餐費(fèi)補(bǔ)助300元。
三、課程安排
完成分組課題，并進(jìn)行展示。在學(xué)員的意愿基礎(chǔ)上，擇優(yōu)選擇部分學(xué)生進(jìn)入專題二繼續(xù)學(xué)習(xí)。
專題二：數(shù)值代數(shù)與形式化
時(shí)間：2025年7月14日 - 2025年8月3日
規(guī)模：招生人數(shù)為20人。
一、報(bào)名條件
1.數(shù)學(xué)或計(jì)算機(jī)科學(xué)等相關(guān)專業(yè)的二三年級(jí)本科生優(yōu)先考慮。
2.有編程基礎(chǔ)、數(shù)值代數(shù)相關(guān)基礎(chǔ)的學(xué)生優(yōu)先考慮。
3.有數(shù)學(xué)或相關(guān)競(jìng)賽經(jīng)歷的學(xué)生優(yōu)先考慮。
4.結(jié)課后仍能持續(xù)投入時(shí)間和精力：積極參與交流討論，聽(tīng)從導(dǎo)師與助教的安排和指導(dǎo)。
二、食宿安排
為非上海地區(qū)的同學(xué)提供免費(fèi)住宿，為所有同學(xué)提供餐費(fèi)補(bǔ)助300元/周。
三、課程安排
1.第一階段（7月14-20日）：進(jìn)行Lean4的學(xué)習(xí)，完成Lean提供的Mathematics in Lean中10道練習(xí)題。
2.第二階段：
a.（7月21-27日）協(xié)助整理數(shù)學(xué)定理證明的自然言語(yǔ)版本；完成導(dǎo)師指定的數(shù)值代數(shù)相關(guān)的形式化證明。
b.（7月28日-8月3日）進(jìn)行數(shù)值代數(shù)的形式化。
3.第三階段：我們將從完成第二階段的學(xué)員中擇優(yōu)選擇10名同學(xué)，于8月底集中進(jìn)行數(shù)學(xué)形式化工作。具體細(xì)節(jié)將另行通知。
注：前兩周都設(shè)有考核，不達(dá)標(biāo)的同學(xué)不能繼續(xù)下一階段的學(xué)習(xí)。
報(bào)名材料與方式
一、報(bào)名材料
1.成績(jī)單（教務(wù)部門出具）。
2.競(jìng)賽獲獎(jiǎng)證書(shū)等補(bǔ)充材料。
3.個(gè)人簡(jiǎn)歷和陳述。
二、報(bào)名方式
1.網(wǎng)上報(bào)名：
通過(guò)網(wǎng)址https://wj.sjtu.edu.cn/q/bKSvNqG5填寫(xiě)在線報(bào)名表。（注：交大學(xué)生也要報(bào)名）
2.將報(bào)名材料按照?qǐng)?bào)名材料順序合并轉(zhuǎn)成一個(gè)PDF文檔，文檔命名格式為：“專題一/二+學(xué)生姓名+學(xué)校名稱”（如專題一+張三+上海交通大學(xué)）。將電子文檔發(fā)送至郵箱：AI4MathSJTU@163.com，郵件主題命名格式為：`專題一/二+學(xué)生姓名+學(xué)校名稱`。
注：以郵件收到的報(bào)名材料為準(zhǔn)，僅在網(wǎng)上報(bào)名而不按照要求發(fā)送電子材料視為報(bào)名無(wú)效。
3.報(bào)名截止日期為2025年6月15日。
結(jié)業(yè)形式

1.兩個(gè)專題的學(xué)生完成相應(yīng)的課程任務(wù)后可獲得結(jié)業(yè)證書(shū)。
2.表現(xiàn)優(yōu)異的學(xué)生將獲得組委會(huì)頒發(fā)的榮譽(yù)證書(shū)。
聯(lián)系方式

郵箱：AI4MathSJTU@163.com
課程大綱

課程時(shí)間：2025年7月14日 - 2025年8月3日
專題一： 2025年7月14日 - 2025年7月20日
 
專題二： 2025年7月14日 - 2025年8月3日
數(shù)值代數(shù)授課老師：羅濤，梁經(jīng)緯
 

上海交通大學(xué)相關(guān)保研資源下載：

上海交通大學(xué)歷年保研筆試/面試真題匯編.pdf
上海交通大學(xué)保研夏令營(yíng)信息匯總表.xls
上海交通大學(xué)預(yù)推免信息匯總表.xls
上海交通大學(xué)保研生源分析表.xls
上海交通大學(xué)本科生保研去向分析表.xls
各重點(diǎn)院校保研夏令營(yíng)信息匯總表（報(bào)名截止時(shí)間）.zip
各重點(diǎn)院校推免生條件及要求匯總表.zip

上海交通大學(xué)

添加上海交通大學(xué)學(xué)姐微信，或微信搜索公眾號(hào)“保研喵”，關(guān)注【保研喵】微信公眾號(hào)，在保研喵公眾號(hào)輸入【上海交通大學(xué)保研夏令營(yíng)條件、上海交通大學(xué)保研加分細(xì)則、上海交通大學(xué)保研群、上海交通大學(xué)保研學(xué)姐微信、上海交通大學(xué)保研真題、上海交通大學(xué)夏令營(yíng)】即可在手機(jī)上查看相對(duì)應(yīng)上海交通大學(xué)保研信息和免費(fèi)資源。
回復(fù)【夏令營(yíng)信息】【保研去向】【保研來(lái)源】【入營(yíng)名單】即可查看蕞新蕞全的保研數(shù)據(jù)。
上海交通大學(xué)保研


本文來(lái)源：http://www.vzpo.com.cn/shanghaijiaotongdaxue/byxly_960508.html

推薦閱讀