[spam][julia][wrong] Probabilistic Program Synthesis?

[Undiscussed Horrific Abuse, One Victim of Many]

The first thing you think when reading about julialang is probably
along the lines of, "oh i could totally make a hyperintelligent
computer virus that took over the world, with that". Imagine crowds
and crowds of engineers thinking this.

Well, I websearched for "julia function synthesis", and lo and behold,
it's in the standard library.

Or maybe they just centralise the docs for the package repository, I'm not sure.

https://docs.juliahub.com/Synthesizer/b8Maw/0.1.0/

I'll read this while typing it into this email, so that I might get
farther. It sounds cool.

Note: It may be productive to focus on speeding the crafting of tests.
Additionally, the function generator does not yet consolidate and
optimize its result.

-

This is the documentation for the Synthesizer.jl program synthesis
system. [ https://github.com/femtomc/Synthesizer.jl ]

The goal of this package is to provide a set of interfaces for
probabilistic program synthesis via sketching. he hope is to faciliate
research into probabilistic program synthesis, as well as provide a
pipeline to optimize synthesized programs as IR fragments, before
compilation into a method body in Julia.

The idea behind sketching is to provide a high-level skeleton of the
program (or function) you want to synthesize. This high-level skeleton
contains a number of "holes" which the synthesizer should fill with an
expression or function.

Let's say we wanted to synthesize a sorting program.

function sort!(x::Array{T}) where T <: Number
    while !check(x)
        x = hole(array_operation, x)
    end
    return x
end

Here, I've provided the high-level structure of the function (e.g.
control flow) but I've also inserted a hole, and I'm telling the
synthesizer what sort of hole it should be (an array_operation
function, which acts on x). array_operation is defined by a miniature
DSL.

@lang (array_operation) _1 expr = begin
    0.20 => swap!(_1)
    0.20 => reorder(_1)
    0.20 => swap_head!(_1)
    0.20 => swap_tail!(_1)
    0.20 => reverse(_1)
end

This DSL is probabilistic - the numbers on the left-hand side
correspond to probability of selection by the synthesizer.
Furthermore, we've specified that holes of array_operation take in a
single argument (here, by specifying _1 before defining the expr of
type array_operation).

In our high-level program, we've cheated a bit by providing a way for
the program to determine if it's sorted the list correctly. The
function check checks if the array satisfies the sorted condition.

function check(x::Array{T}) where T <: Number
    length(x) == 1 && return true
    i = x[1]
    for j in x[2 : end]
        if !(i < j)
            return false
        end
        i = j
    end
    return true
end

To summarize: in Synthesizer.jl, the user writes small probabilistic
DSLs (specifically, probabilistic context-free grammars) which can
then be used inside holes in other functions. The process of synthesis
is expressed using a universal trace-based probabilistic programming
system. [ https://github.com/femtomc/Jaynes.jl ]

The core of the engine is a multi-threaded rejection sampler.

function synthesize(sel::Array{K}, fn::Function, pair::T; iters = 50)
where {K <: Jaynes.ConstrainedSelection, T <: Tuple}
    in, out = pair
    success = Jaynes.CallSite[]
    Threads. at threads for s in sel
        for i in iters
            ret, cl, w = generate(s, fn, in)
            out == ret && push!(success, cl)
        end
    end
    return success
end

function synthesize(fn::Function, pairs::Array{T}; iters = 50) where T <: Tuple
    local cls
    constraints = [selection()]
    for p in pairs
        cls = synthesize(constraints, fn, p; iters = iters)
        cls == nothing && return cls
        constraints = map(cls) do cl
            get_selection(cl)
        end
    end
    return cls
end

Here, synthesize requires that the user pass in a function with holes,
as well as pairs of (input, output) tuples. generate generates a set
of possible solutions. This version of synthesize will return an Array
of successful traces (if the search succeeds). The CallSite
representation is a trace of the original function, as well as a
recording of the choices made by the PCFG.

In future versions, Synthesizer.jl will support the ability to compile
these traces into IR and generate a new (optimized) method body for
the synthesized function.