Type guided program synthesis: at the intersection of programmer tools, proof assistance and explainable AI

类型引导程序综合：程序员工具、证明辅助和可解释人工智能的交叉点

• 批准号: 2054778
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2018
• 资助国家: 英国
• 起止时间: 2018 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2054778
• 关键词: Type; guided; program; synthesis; intersection

EPSRC research areas: Artificial intelligence technologies, Logic and combinatorics, Programming languages and compilers, Theoretical Computer Science, Verification and correctness.Potential impact: Program synthesis, among the oldest problems in computer science, has great potential for addressing the newly arising problem of explainable AI. Programming often involves small tasks that seem trivial and tedious. Program synthesis will soon become a mainstream tool to either quickly solve such problems (by generating a program) or to let the programmer know that a non-trivial task is at hand. At the same time synthesis can be understood as automated proof search, iteratively applying formal rules until a valid proof has been found. Within AI, program synthesis has great promise as a paradigm for generating programs that are not just understood by machines, but also allow humans to effectively reason about their behaviour.Context: The starting off point will be research conducted for a master's thesis on the effectiveness of types in reducing the program hypothesis space in the setting of Inductive Logic Programming (ILP), i.e. generating logic programs from examples. Having identified typing of programs as important structure for synthesis, the DPhil will focus on leveraging refinement types (and related concepts) as a tool for the specification of synthesis problems, as well as letting types guide the search.A type refinement are propositions which restrict the values that belong to that type. Refinements allow us to reason about when composing programs makes sense. As automation of program/proof generation is the goal, deciding on whether combined refinements describe programs that are still compatible with the synthesis specification is important. For synthesis to be useful it needs to be done rapidly. The issue is that for each partial program considered, during synthesis, the satisfiability of the refinements in the program needs to be determinded. Especially promising are Satisfiability Modulo Theories (SMT) solvers, as they have proven to be very efficient on restricted logics.Major trends that influence the direction of the work are the Meta-Interpretive Learning (MIL) framework originating in ILP and the automation that is available in proof assistants (e.g. Coq.). Both approaches rely on the user to supply programs/proofs and metarules/tactics to inform the synthesizer of the kinds of hypotheses to consider. The correspondence between programs and proofs is well known; the relation between metarules, an encoding of the allowed structure of the program, and that of tactics, aggregations of rules for backward reasoning in proof construction, has yet to be considered in detail.Aims and objectives: Vastly improve on the master's thesis approach of utilizing SMT solving to decide on compatibility of type refinements. The prime interest is in identifying encoding to logic fragments that are effective for synthesis. Use the MIL framework as a testbench.Evaluate whether it is possible to encode the synthesis problem in a logic as a SMT problemDetermine whether the strong structural properties of logic programs, captured by metarules, lead to an description of structural patterns in functional programs/proofs useful in synthesis. Investigate how metarules and tactics relate, respectively (logic) program synthesis and proof search in proof assistants, and find areas where they can reinforce each other.Determine how users' intuitions for strong structural properties, such as the need for nested induction/mutually recursion (on particular variables), can be captured as high level rules in these frameworks and how such hints can be used to restrict the search space.Collaborators:Prof. Luke Ong (DPhil & MSc thesis supervisor)Prof. Jeremy Gibbons (DPhil supervisor)Dr. Andrew Cropper (MSc thesis supervisor)

EPSRC研究领域：人工智能技术、逻辑和组合学、编程语言和编译器、理论计算机科学、验证和正确性。潜在影响：程序合成是计算机科学中最古老的问题之一，对于解决新出现的可解释人工智能问题具有巨大潜力。编程经常涉及一些看起来琐碎而乏味的小任务。程序合成很快就会成为一种主流工具，它可以快速解决这些问题（通过生成程序），或者让程序员知道手头有一个重要的任务。与此同时，程序合成可以被理解为自动化的证明搜索，迭代地应用形式化规则，直到找到有效的证明。在人工智能中，程序合成作为一种范式，不仅可以生成机器理解的程序，还可以让人类有效地推理他们的行为。出发点将进行研究的硕士论文类型的有效性，减少程序假设空间的设置归纳逻辑编程（ILP），即从例子中生成逻辑程序。在确定了程序的类型化是综合的重要结构之后，哲学博士将集中精力利用精化类型（和相关概念）作为综合问题的规范化工具，以及让类型指导搜索。精化允许我们推理什么时候编写程序是有意义的。由于程序/证明生成的自动化是目标，因此决定组合改进是否描述仍然与合成规范兼容的程序是重要的。为了使合成有用，它需要迅速完成。问题是，对于每个部分程序考虑，在合成过程中，在程序中的细化的可满足性需要被确定。特别有前途的是可满足性模理论（SMT）求解器，因为它们已被证明是非常有效的限制逻辑。影响工作方向的主要趋势是元解释学习（MIL）框架起源于ILP和自动化，可在证明助手（例如Coq。）。这两种方法都依赖于用户提供程序/证明和元规则/策略，以告知合成器要考虑的假设类型。程序和证明之间的对应关系是众所周知的;元规则之间的关系，允许的程序结构的编码，和策略，在证明建设中向后推理的规则集合，还没有被考虑details.Aims和Objectives：极大地提高了利用SMT解决决定类型改进的兼容性的硕士论文方法。主要的兴趣是在识别编码的逻辑片段是有效的合成。使用MIL框架作为测试平台。评估是否有可能将逻辑中的综合问题编码为SMT问题。确定逻辑程序的强结构属性（由元规则捕获）是否导致对综合中有用的函数程序/证明中的结构模式的描述。研究元规则和策略如何相互关联，分别是（逻辑）程序合成和证明助手中的证明搜索，并找到它们可以相互加强的领域。确定用户对强结构属性的直觉，例如嵌套归纳/相互递归的需求（关于特定变量），可以被捕获为这些框架中的高级规则，以及如何使用这些提示来限制搜索空间。Luke Ong教授（哲学博士和理学硕士论文导师）Jeremy Gibbons教授（哲学博士导师）Andrew Cropper博士（理学硕士论文导师）