archivy logo

UZPG

  v1.7.7

program synthesis notes


program synth notes

  • met hastings approach is to use the hastings algorithm to sample from the markov chain of transformations where you define program quality as opposed to some correctness and perf criteria

In general, the MH approach can be a very powerful search method, particularly in cases where we need to search for programs larger than what explicit search techniques, and where we have enough intuition about the space to define good proposal distributions and scoring functions. Carefully defining these two functions is crucial for this method to actually work.

L6

  • formal synthesis approach to ML

    • hypothesis space of programs
    • dataset
    • version space of correct programs => emphasis on total correctness
  • there is a nice framework of like

    • take a lattice => set where given two elements they have a shared LUB and GLB
    • then define some order on your version space of functions
    • can you represent intervals and boundaries under your order, in which case it's boundary representable
    • if it is, you can maybe compute combinations of function spaces efficiently
  • sketch is really cool

    • you build out this abstract model/expressive hypothesis program space for the types of programs you want to generate
    • then you like compose these generators even recursively
    • and you solve against a harness
    • recursive generators have different shapes, they are not just waiting to be filled
  • read about abstract interpretation

L7

  • constraint based synthesis -> represent program spaces as functions of parameters and then have parametric programs
  • sketch creates a programming language to describe parametric programs
  • what's cool is sketch has generator functions where like you can
    • fill in with holes and then return a function with those holes filled
  • you can do a lot with this

L8/9

  • denotational semantics and semantics
  • sketch is doing symbolic execution
  • updating list of valoid assignments and state
  • confused about how if statements work, you need to somehow represent this idea of cond.
  • with loops you need to be careful because you don't know if it evaluates to true, so you need to do some recursive iterating up to soke bound
  • simplify expression tree with structural hashing for similar structures and simplification rules
  • one hot encoding for possibilities in translation to a CNF SAT instance
  • todo read sat solver

L10/11

  • look into reactive synthesis
  • functional synthesis
    • fom of spec
    • Establish correctness
    • search strategy
  • correctness -> pre condition and post condition
  • fully spec-ing is hard, so you use different formalisms
  • this predicate approach is nice because you can SAT solve constraints but it's very slow, so you:
    • eliminate quantifiers #todo how does that work
    • basically you look at the constraints and notice extra forcing conditions on the variables in terms of each other
  • counter example guided inductive synthesis
  • synthesize good counter examples and trim search
    • how do you find them #todo
  • abstraction based synthesis
    • push values through the program
  • Hoare triples/hoare program logics as a way to ensure validity of state jumps
  • confused here #todo
    • reread L11

L12

  • look into distillations of neural nets <-> programs

    • RL/Time series modeling

    #todo