程序合成

发表于 更新于 分类于

程序合成

经典程序合成定义

输入:

  1. 一个程序空间, 通常用文法表示.
  2. 一条规约, 通常为逻辑表达式.

输出: 一个程序, 满足.

一个例子: max问题

语法:

规约: .

期望答案为: .

程序合成方法

1
2
3
4
graph LR
	A[生成程序] --程序--> B[验证正确性]
	B --正确--> 输出
	B --错误--> A

  1. 如何产生下一个被搜索的程序?

    1. 枚举法——按照固定格式搜索.
    2. 约束求解法——转成约束求解问题.
    3. 空间表示法——一次考虑一组程序而非单个程序.
    4. 基于概率的方法——基于概率模型查找最有可能的程序.

  2. 如何验证程序的正确性? 抽象解释, 符号执行.

    1. 基于反例的优化: CEGIS. 保存约束求解器的反例, 首先采用测试. 要选择一个好的反例, 就要估算它可以排除的程序的个数.
    2. LearnSy: 通过近似输出相同的程序对的个数来估计被排除的程序. 输出相同的程序对越多，被一个输入输出对排除的程序期望数量就越少.
    3. …

枚举 （enumerate）