《熊英飞-算法合成——自动应用算法模式合成高效程序.pdf》由会员分享,可在线阅读,更多相关《熊英飞-算法合成——自动应用算法模式合成高效程序.pdf(42页珍藏版)》请在三个皮匠报告上搜索。
1、算法合成自动应用算法模式合成高效程序熊英飞 北京大学演讲嘉宾熊英飞北京大学副教授熊英飞于2009年从日本东京大学获得博士学位,2009-2011年在加拿大滑铁卢大学工作,2012年加入北京大学,现任新体制长聘副教授。熊英飞的研究兴趣是程序设计语言和软件工程,特别是程序合成、修复和分析。他提出了理论和方法降低程序编写和缺陷修复的代价。比如,基于差别的双向变换框架是最广泛使用的双向变换框架之一,概率和逻辑结合的程序合成框架玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用,比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他获得CCF-IEEE CS青
2、年科学家奖、MODELS十年最有影响力论文奖,5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖。他是SATE18的程序委员会联合主席,也在PLDI、ICSE、FSE等会议担任PC。知乎问题课程名点赞数算法数据结构47大学语文23马克思主义12汇编语言5体系结构1算法为什么难:示例 最大子段和问题:输入一个整数的列表,求列表上连续一段的最大和。1,-2,3,-2,3 4 穷举算法非常容易实现 算法复杂度为(3)能否应用算法课的知识来进行优化?算法为什么难:示例 算法课教了一系列算法设计模式,尝试应用分治 算法复杂度:(/),m:处理器个数 应用算法设计模式并不容易 分治:把原问题分解
3、成规模更小的问题 对具体问题并没有给出分解方法,需要程序员的智慧 分治后的程序长度、理解难度均远超原来的程序研究目标:自动应用算法模式应用分治降低难度:算法设计是困难耗时的步骤节省成本:会算法的程序员需要更高人力成本同一时间、同一地点、同一公司、同一部门的两个招聘岗位提高质量:算法优化是缺陷来源 SeL4:著名经验证操作系统内核 第一阶段:采用Haskell的算法设计 验证导致500+修改 第二阶段:采用C的系统实现 验证导致50+修改优化前程序简洁、优雅、模块化优化后程序冗长、繁杂、破坏边界提升效率:自动优化程序目前的编译优化技术只能进行局部小替换,通常很难显著降低程序复杂度。自动应用算法模
4、式有望对程序进行整体大幅优化。常见编译优化技术大型语言模型是否解决这个问题?Can you optimize this program as a parallel program using D&C?The expected time complexity is O(n/p),where n is the length of the input list x,and p is the number of CPU cores.mss=-INF for i in range(len(x):for j in range(i,len(x):mss=min(mss,sum(xi:j+1)return m
5、ssmin而不是max北京大学目前成果 两类算法设计模式的自动应用方法分治类问题arXiv:2202.12193分治(并行化)、增量计算、流算法、线段树、最长子段问题等动态规划问题OOPSLA23根据不同的算法设计模式实例化成不同的合成工具 例:列表上的()分治算法的合成工具输入:一个程序,从列表产生输出可以用任意编程语言、任意算法编写也可从形式化需求自动导出输出:一个列表上的分治程序和输入程序等价算法复杂度是(),其中为CPU的数量传统求解方法:程序演算 通过一系列程序变换半自动得到优化后的程序 但算法设计往往需要“根据具体问题设计关键模块”这样的操作 通用程序变换规则难以完成问题特定的设计
6、 因此,程序演算保持半自动求解14方法概览分治/并行化增量计算单通道/流算法线段树提升问题Lifting Problem求解算法AutoLifter规约基于搜索的归纳程序合成求解动态规划MPF和LOF合成问题求解算法SynMem手动应用分治算法 第二小问题:输入整数列表 查找列表中的第二小的元素 输入程序 时间复杂度:O(nlogn)目标:采用分治优化程序 得到O(n/m)并行程序return sorted(xs)l手动应用分治算法 分三步应用分治:1.将输入列表分成两份+2.在两份列表上分别递归计算sndmin3.合并结果得到原列表上的结果 但是,这样的合并操作是不存在的1,3,52,4,6
7、1,3,5,2,4,634sndminsndmin2sndmincomb手动应用分治算法 从原列表中产生辅助值 然后可以写出合成函数1,3,52,4,61,3,5,2,4,634sndminsndmin2sndmincomb1fstmin2fstmin1fstmin,=(min,max,min(,)=min()寻找一个辅助函数aux,使得可以找到comb函数,将两个子列表上算出来的结果合并为原列表的结果手动应用增量算法 问题:假设已经对一个很长的列表求出了第二小 现在列表后面新增了一个元素 如何快速计算新列表的第二小?和之前类似,这样的合并函数不存在 增量算法通常从原输入产生辅助值使得结果可以
8、快速更新2,4,64sndmin2,4,6+12sndmin1comb手动应用增量算法 从原列表中产生辅助值 然后可以写出合成函数,=(min,max,min(,)=min()寻找一个辅助函数aux,使得可以找到comb函数,将原列表上算出来的结果和修改合并为新列表的结果2,4,64sndmin2,4,6+11comb2fstmin2sndmin1fstmin提升问题Lifting Problem 输入:1.a:某种数据结构的实例2.c:附加值3.orig:从数据结构上计算某种结果4.op:从已有数据结构实例构造新实例 输出:满足下面条件的辅助值程序 和合并程序 ,1,=,1,=(,)=()1
9、=1,3,52=2,4,6:1+2:列表上的分治提升问题Lifting Problem 输入:1.a:某种数据结构的实例2.c:附加值3.orig:从数据结构上计算某种结果4.op:从已有数据结构实例构造新实例 输出:满足下面条件的辅助值程序 和合并程序 ,1,=,1,=(,)=11=2,4,6:1+:增量算法提升问题Lifting Problem 输入:1.a:某种数据结构的实例2.c:附加值3.orig:从数据结构上计算某种结果4.op:从已有数据结构实例构造新实例 输出:满足下面条件的辅助值程序 和合并程序 ,1,=,1,=(,)更通用的增量算法=“delete 2ndelement”1
10、=2,4,6:,1:线段树 高效回答子段查询/修改操作的数据结构 查询:序列中第4-5000个数的第二小是多少?修改:将序列第2-3000个数都加一 通过分治来完成查询 通过增量算法来完成修改,1,2 1+2 =1,1 提升问题Lifting Problem 其他很多算法模式的应用也可以转成提升问题 分治/并行化 增量计算 流算法 线段树 最长子段问题 动态规划(进行中)如何求解提升问题?背景:程序合成 从规约中自动生成程序规约合成器程序“One of the most central problems in the theory of programming.”-Amir Pneuli图灵奖
11、获得者“(软件自动化)提升软件生产率的根本途径”-徐家福先生中国软件先驱程序合成问题定义 输入:一个程序空间Prog,通常用语法表示 一条规约Spec,通常为逻辑表达式 输出:一个程序prog,满足progProgprogSpec例子:max问题 语法:规约:期望答案:ite(x=y)y x如何求解提升问题?提升问题是程序合成问题 输入:规约,1,=,1,=(,)的语法 的语法 输出:和的实现如何求解程序合成问题 程序合成基本方法:枚举+验证 其他高级算法可以看做是这个基本形式的优化枚举程序验证正确性程序正确错误从小到大枚举程序:x,y,x+y,x+x,y+y,(x+y)+x,(x+y)+y,
12、通过约束求解工具自动验证或者通过大量测试概率验证程序合成的瓶颈:可伸缩性 从小到大的枚举不可能枚举到很大的程序 程序空间随程序大小呈指数增长 当目标程序使用超过5个运算符的时候,现代程序合成工具就经常失效 提升问题的解远远超过这个规模()=snd1,fst1,2,2=min 1,2,max 1,2,min 1,2应对可伸缩性问题 分治:把解程序分解成小部分单独合成()=snd1,fst1,2,2=min 1,2,max 1,2,min 1,2 两套分解方法 变量消除 组件消除组件消除+=(),()where =(,)(,)可以分成两部分()=1,1,2,2=min 1,2,max 1,2,mi
13、n 1,2 第一部分的规约 +=1(),()where =(,)求解后,代入原规约得到只有第二部分的规约 +=2(),()where =(,)2.提供辅助值1.提供原来的输出变量消除 规约中同时包括 和 1,无法单独合成 能否得到只包含的规约?+=1(),()where =(,)变量消除 1是一个函数 即同样的输入得到同样的输出 变形可得 该规约只包含,可以用传统程序合成技术求解得到+=1(),()where =(,)=+=(+)+=消除规则的性质 通过上述方法获取的规约是一个近似 如,在变量消除中,只保证存在一个函数 1 但该函数不一定能用目标语言实现出程序 在这种情况下,第二步合成1会失败
14、,需要回溯 回溯过多会影响效率 我们证明几乎不会出现回溯通用情况 产生辅助值时可能需要用到更多的辅助值 反复应用组件消除,直到没有更多的辅助值产生 完整算法请见论文分治类算法效果96个已有数据集、论文和中的分治和其他问题最大子段和字符串转换成数字检查字符串中括号是否匹配线段树问题Petrozavodsk冬令营题目(全球243支队伍只有26支解出)动态规划合成效果 40个问题,取自Leetcode使用频率最高的动态规划问题和近十年NOIP中的动态规划问题 背包问题 最长公共子序列 最大独立集 网格上的最短路径 斐波那契数列39算法数据集ASAC 进行中包含CSP/NOIP近十年左右的比赛题目所有题目用MiniZinc形式化描述可以直接采用现有CSP/OMT求解器求解所有题目同时包含自然语言描述、测试用例40小结 各种软件都需要大量算法算法合成是重要的 研究只是整理出算法设计模式 能否应用全凭程序员能力算法设计是困难的 初步研究已经在一大类算法模式上成功 算法合成的一个通用问题:提升问题 通过寻找合适的近似,提升问题可通过分治高效求解能否自动应用算法设计模式?期待更多人投入算法合成的研究和实践!感 谢 聆 听