Skip to content

Progsynth

  • Second-order problem reduction
    • Reduce to first order (SMT/SAT-able)
  • Templates/DSL
    • vs. Sketch: Sketch is bounded, integer hole-filling.
  • Distinguishing inputs
    • Exists a complete but expensive validation oracle (VALIDATION ORACLE)
    • Find a distinguishing input that identified the incorrect candidate

    • BuildIOConstriant, BuildDistConstraint

  • Syntactic Bias: restricting the syntax of possible programs to consider
    • SKETCH
    • SyGuS: Formalizing program synthesis
  • Optimization: needs a cost-model
    • Ranking
      • MCMC: Metropolis-Hasting
      • Version space algebra: beam-search
      • ML
      • Meta-Sketch: CEGIS in subspace
  • ILP: Automatic inference of logical programs from examples
    • FOCUS: first-order rules and relations
    • Examples <-> Knowledge-base