Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs

• URL: http://arxiv.org/abs/2102.12553v1
• Date: Thu, 18 Feb 2021 13:40:16 GMT
• Title: Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs
• Authors: Rolf Morel
• Abstract summary: We show that type checking is able to prune large parts of the hypothesis space of programs. We are able to infer polymorphic types of synthesized clauses and of entire programs.
• Score: 2.28438857884398
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The program synthesis problem within the Inductive Logic Programming (ILP) community has typically been seen as untyped. We consider the benefits of user provided types on background knowledge. Building on the Meta-Interpretive Learning (MIL) framework, we show that type checking is able to prune large parts of the hypothesis space of programs. The introduction of polymorphic type checking to the MIL approach to logic program synthesis is validated by strong theoretical and experimental results, showing a cubic reduction in the size of the search space and synthesis time, in terms of the number of typed background predicates. Additionally we are able to infer polymorphic types of synthesized clauses and of entire programs. The other advancement is in developing an approach to leveraging refinement types in ILP. Here we show that further pruning of the search space can be achieved, though the SMT solving used for refinement type checking comes

Related papers

• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  A growing trend in program analysis is to encode verification conditions within the language of the input program. We propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features.
  arXiv  Detail & Related papers  (2024-07-11T12:51:08Z)
• A Divide-Align-Conquer Strategy for Program Synthesis [8.595181704811889]
  We show that compositional segmentation can be applied in the programming by examples setting to divide the search for large programs across multiple smaller program synthesis problems. A structural alignment of the constituent parts in the input and output leads to pairwise correspondences used to guide the program search.
  arXiv  Detail & Related papers  (2023-01-08T19:10:55Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems [0.0]
  We introduce a formal meta-language for probabilistic programming, capable of expressing both programs and the type systems in which they are embedded. We draw on the frameworks of cubical type theory and dependent typed metagraphs to formalize our approach.
  arXiv  Detail & Related papers  (2022-03-30T01:07:37Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  We take the first step to synthesize C programs from input-output examples. In particular, we propose La Synth, which learns the latent representation to approximate the execution of partially generated programs. We show that training on these synthesized programs further improves the prediction performance for both Karel and C program synthesis.
  arXiv  Detail & Related papers  (2021-06-29T02:21:32Z)
• Leveraging Language to Learn Program Abstractions and Search Heuristics [66.28391181268645]
  We introduce LAPS (Language for Abstraction and Program Search), a technique for using natural language annotations to guide joint learning of libraries and neurally-guided search models for synthesis. When integrated into a state-of-the-art library learning system (DreamCoder), LAPS produces higher-quality libraries and improves search efficiency and generalization.
  arXiv  Detail & Related papers  (2021-06-18T15:08:47Z)
• A Reinforcement Learning Environment for Polyhedral Optimizations [68.8204255655161]
  We propose a shape-agnostic formulation for the space of legal transformations in the polyhedral model as a Markov Decision Process (MDP) Instead of using transformations, the formulation is based on an abstract space of possible schedules. Our generic MDP formulation enables using reinforcement learning to learn optimization policies over a wide range of loops.
  arXiv  Detail & Related papers  (2021-04-28T12:41:52Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• Type-driven Neural Programming by Example [0.0]
  We look into programming by example (PBE), which is about finding a program mapping given inputs to given outputs. We propose a way to incorporate programming types into a neural program synthesis approach for PBE.
  arXiv  Detail & Related papers  (2020-08-28T12:30:05Z)
• BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
  We present a new synthesis approach that leverages learning to guide a bottom-up search over programs. In particular, we train a model to prioritize compositions of intermediate values during search conditioned on a set of input-output examples. We show that the combination of learning and bottom-up search is remarkably effective, even with simple supervised learning approaches.
  arXiv  Detail & Related papers  (2020-07-28T17:46:18Z)
• OptTyper: Probabilistic Type Inference by Optimising Logical and Natural Constraints [26.80183744947193]
  We introduce a framework for probabilistic type inference that combines logic and learning. We build a tool called OptTyper to predict missing types for TypeScript files.
  arXiv  Detail & Related papers  (2020-04-01T11:32:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.