模预言机下的可满足性与合成

Elizabeth Polgreen; Andrew Reynolds; Sanjit A. Seshia

模预言机下的可满足性与合成

计算机科学中的逻辑 2021-07-29 v1 机器学习编程语言

作者: Elizabeth Polgreen , Andrew Reynolds , Sanjit A. Seshia

摘要

在经典的程序合成算法中,例如反例引导归纳合成(CEGIS),算法在合成阶段与预言机(验证)阶段之间交替。许多合成算法使用基于可满足性模理论(SMT)求解器的白盒预言机来提供反例。但是,如果白盒预言机不可用或不易使用该怎么办?我们提出了一个用于求解一类通用预言机引导合成问题的框架,我们称之为模预言机合成。在此设定中,预言机可以是具有由合成问题定义的查询-响应接口的黑盒。作为该框架的必要组成部分,我们还形式化了模理论与预言机的可满足性问题,并提出了求解该问题的算法。我们实现了一个模预言机可满足性与合成的原型求解器,并证明,通过使用执行不易在SMT约束中建模的函数(例如递归函数或包含代码编译与执行的预言机)的预言机,SMTO与SyMO能够求解标准SMT与合成求解器能力之外的问题。

关键词

程序合成模理论可满足性预言机引导合成黑盒预言机 CEGIS SMT求解器 SyMO

引用

@article{arxiv.2107.13477,
  title  = {Satisfiability and Synthesis Modulo Oracles},
  author = {Elizabeth Polgreen and Andrew Reynolds and Sanjit A. Seshia},
  journal= {arXiv preprint arXiv:2107.13477},
  year   = {2021}
}

备注

12 pages, 8 Figures

模预言机下的可满足性与合成

摘要

关键词

引用

备注

相关论文