数值分析中形式化验证与算法发现的博士后职位
内容提要
陶哲轩博客发布Annalisa Buffa的客座文章，宣布EPFL数值建模与仿真教席招聘博士后，探索形式化验证与算法发现对数值分析的影响。研究方向包括用Lean形式化有限元稳定性与误差估计，或AI辅助发现新离散范式并形式验证。无固定项目，需主导新研究线并发表成果。申请需提交CV、动机信和两名推荐人，招满为止。
延伸解读
职位定位：探索性研究而非既定项目
该博士后职位没有预设的具体研究项目，目标是让入选者与团队共同确定方向，通过实验探索形式化验证和算法发现对数值分析的实际帮助与局限。这意味着候选人需要具备较强的自主研究能力，能够主导一条新的研究线，而非执行已有计划。
可能的研究切入点
文章给出了两个可能的起点：一是用Lean形式化有限元方法的稳定性和误差估计；二是利用AI辅助发现新的离散范式，并对其性质进行形式验证。这两个方向都结合了形式化方法与数值分析，但具体选择取决于候选人的兴趣和背景。
申请要点与时间安排
申请需通过指定链接提交CV、动机信和两名推荐人的联系方式。动机信中需简要描述一个希望研究的问题，将数值分析与形式化验证或算法发现联系起来。申请审核将持续到职位招满为止，开始日期灵活，可尽快入职。
Q&A
EPFL数值建模与仿真教席招聘的博士后职位主要探索什么方向？
该职位探索形式化验证和算法发现对数值分析的影响，具体包括用Lean形式化有限元稳定性与误差估计，或AI辅助发现新离散范式并形式验证。
这个博士后职位有固定的研究项目吗？
没有固定项目。目标是主导一条新研究线，通过具体实验探索这些方法在PDE数值格式设计与分析中的帮助和不足。
申请这个博士后需要提交哪些材料？
需要提交CV、动机信和两名推荐人的联系方式。动机信中需简要描述一个你想研究的问题，将数值分析与形式化验证或算法发现联系起来。
这个博士后职位的开始时间和申请截止日期是什么？
开始日期灵活，尽快开始。申请审核将持续到职位招满为止。
作为博士后，具体需要做哪些工作？
需要建立并主导这条新研究线，与团队共同选择方向，在国际上发表和展示成果。可能的起点包括用Lean形式化有限元稳定性与误差估计，或AI辅助发现新离散范式并形式验证。
这个职位对申请者有什么期望？
期望申请者能主导新研究线，选择研究方向，并发表和展示成果。理想候选人应能通过具体实验探索形式化验证和算法发现对数值分析的影响。
