Inductive synthesis theories and algorithms

归纳综合理论与算法

• 批准号: 2110414
• 金额: --
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2018
• 资助国家: 英国
• 起止时间: 2018 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2110414
• 关键词: Inductive; synthesis; theories; algorithms

Research has been active in the area ``inductive" program synthesis. Inductive approaches tend to iteratively compute programs by observing a few examples of expected input-output behaviour. Many state-of-the-art inductive program synthesis techniques are based on two main components: a verifier and a synthesiser. The synthesiser generates a candidate program, whilst a verifier (a human or another program) checks if the candidate meets the high-level description. If so, then a correct program is found. Otherwise, the verifier provides the synthesiser with an example demonstrating why the candidate program is incorrect. The synthesiser then attempts to find an alternative program guided by the example provided. This process continues until a correct program is found. Whether a solution is reached is determined by several factors including the correctness of the high-level description and the choice of examples provided to the synthesiser.However, in practice, high-level descriptions tend to be partial and sometimes incorrect, thus causing existing synthesis algorithms to fail. Furthermore, the set of examples from which a verifier may choose is often infinite, whose elements may lead the synthesiser to search for less efficient programs.The overall aim of this thesis is the development of new inductive synthesis theories and algorithms that (1) account for potentially incorrect descriptions and (2) intelligently select examples that are can direct the synthesis engine to efficient programs more quickly. For the former, the focus will be on the design of weakening and strengthening operators for repairing incorrect or partial descriptions in such a way that allows for new descriptions to be generated that (a) are semantically similar to the original ones, and (b) succeed in yielding a correct program. For the latter, new metrics will be defined to measure the goodness of an example with respect to the synthesis task.The research underlying this thesis is aligned with EPSRC's software engineering research area.

在“归纳”程序综合领域的研究一直很活跃。归纳法倾向于通过观察一些预期输入输出行为的例子来迭代计算程序。许多国家的最先进的归纳程序合成技术是基于两个主要组成部分：验证器和合成器。合成器生成候选程序，而验证器（人类或其他程序）检查候选程序是否符合高级描述。如果是，则找到正确的程序，否则，验证器向合成器提供一个示例，说明候选程序为什么不正确。然后，合成器尝试在所提供的示例的指导下找到替代程序。这个过程一直持续到找到一个正确的程序。是否得到一个解取决于几个因素，包括高层描述的正确性和提供给综合器的例子的选择。然而，在实践中，高层描述往往是部分的，有时是不正确的，从而导致现有的综合算法失败。此外，一个验证者可以选择的例子集往往是无限的，其元素可能导致合成器搜索效率较低的programmes.This论文的总体目标是新的归纳合成理论和算法的发展，（1）帐户潜在的不正确的描述和（2）智能选择的例子，可以直接合成引擎更快地高效的程序。对于前者，重点将放在设计的削弱和加强运营商修复不正确的或部分的描述，在这样一种方式，允许新的描述被生成，（a）是语义相似的原始的，和（B）成功地产生一个正确的程序。对于后者，新的指标将被定义来衡量一个例子的优良性方面的综合task.The研究基础，这篇论文是符合EPSRC的软件工程研究领域。