即可将网页分享至朋友圈
教师发展中心“学者论坛”活动特别邀请北京大学文再文教授、北京航空航天大学韩德仁教授来校作学术交流。具体安排如下,欢迎广大师生参加。
一、主 题: 运筹学的形式化与定理证明、随机优化理论前沿进展
二、时 间:2025年8月31日(周日)15:00-18:00
三、地 点:清水河校区六号科研楼A461
四、主讲专家:北京大学文再文教授、北京航空航天大学韩德仁教授
五、主持人:数学科学学院 肖义彬 教授
六、内容简介:
主题一:智能数学推理:形式化与定理证明
本报告探讨通过数学形式化推动智能数学推理的技术路线。与传统依赖直觉的证明方式不同,形式化要求每一步都经过严格论证,具有验证可靠性高、定理可复用、支持模块化思维、可自动化验证等优势。我们将介绍数学优化形式化进展和在线协作ReasLab IDE,随后阐述利用Lean核心表达式树实现基于树状结构的前提选择,通过状态链将自然语言证明翻译为形式化证明方法,以及从结构到实例的定理自动形式化框架。
主题二:Enhanced randomized Douglas-Rachford method: Improved probabilities and adaptive momentum
Randomized iterative methods have gained recent interest in machine learning and signal processing for solving large-scale linear systems. One such example is the randomized Douglas–Rachford (RDR) method, which updates the iterate by reflecting it through two randomly selected hyperplanes and taking a convex combination with the current point. In this talk, we enhance RDR by introducing improved sampling strategies and an adaptive heavy-ball momentum scheme.
七、主讲人简介:
文再文,北京大学博雅特聘教授,国家级人才。主要研究最优化算法与理论、机器学习和人工智能。与合作者开拓了正交约束优化研究领域,推动了流形优化的发展,提出了求解非光滑优化的原始-对偶半光滑牛顿法,研发了OptSuite优化软件和ReasLab在线形式化平台。主编的《最优化方法与理论》入选教育部101计划核心教材,该系列教材累计印刷2.6万余本,得到了北大和清华等超百所高校采用。获中国青年科技奖。现任中国运筹学会副理事长。(主题一)
韩德仁,北京航空航天大学教授、数学科学学院院长,教育部数学类专业教指委秘书长。2002年获南京大学计算数学博士学位。从事大规模优化问题、变分不等式问题的数值方法的研究。曾获中国运筹学会青年科技奖,江苏省科技进步奖等奖项。主持国家自然科学基金杰出青年基金、重点基金等项目。(主题二)
八、主办单位:教师发展中心
承办单位:数学科学学院 计算机科学与工程学院(网络空间安全学院) 航空航天学院
编辑:刘瑶 / 审核:李果 / 发布:陈伟