月度归档:2020年03月

[Review] Dimensions in Program Synthesis (PPDP’10)

Author: Sumit Gulwani (Microsoft Research, Redmond, WA)

Applications of Program Synthesis

  1. Discovery of New Algorithms
    – bitvector algothms
    – mutual-exclusion algorithms
  2. Automated Repetitive Programming for End-Users
  3. Teaching
  4. General Purpose Programming Assistance
  5. Synthesis of Program Inverse
    – compression/decompression
    – encryption/decryption
    – serialization/deserialization
    – insert/delete operations on data structures
    – transactional memory rollback
    – bidirectional programming
    – client-server applications

Dimension 1: User Intent

  1. Logical Specification
    Example: sorting
    $ \forall k. (0 < k < n) \rightarrow (B[k-1] \leq B[k]) \quad \wedge $
    $ \forall k. \exists j. (0 \leq k < n) \rightarrow (0 \leq j < n \wedge B[j] = A[k])$
  2. Natural Language
  3. Input-Output Examples
    Trivial solution: switch-case on every I/O example (defense: restriction on search space)
    Interactive synthesizer: user-driven, synthesizer-driven
  4. Traces
    Appropriate model for program by demonstration.
  5. Programs
    Program deobfuscation, inversion, optimization.

Dimension 2: Search Space

Program Space

  1. Operators
    Arithmetic + bitwise operators for bitvector programs
  2. Control Structure
    Restricted to given looping template, program with bounded # of states, partial program with holes, or even loop-free programs.
    Loop-free programs: bitvector algorithms (arith+bitwise ops), text-editing programs (insert, locate, select, delete), geometrical construction (rule and compass), unbounded data type manipulation (matrix ops, set ops), API call sequences.

Challenge: # of possible programs is exponential to # of components

Grammars

  • Regular expressoins
  • DFAs
  • NFAs
  • Context-free grammars
  • Regular transducers

Logics

First-order logics and its subclasses.

Dimension 3: Search Technique

Brute-force Search

Success examples: bitvector algorithms, mutual-exclusion algorithms

Version Space Algebra (VSA)

ML-based Methods

  1. Probabilistic Inference
  2. Genetic Programming
  3. Logical Reasoning Based Techniques (SAT/SMT Solver)