Restructure synthesis experiments

Author: ReubenJ

Project.toml

@@ -8,6 +8,8 @@ AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"
 DocStringExtensions = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae"
 DynamicalSystems = "61744808-ddfa-5f27-97ff-6e42cc95d634"
 FileIO = "5789e2e9-d7fb-5bc7-8068-2c6fae9b9549"
+Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6"
+HerbConstraints = "1fa96474-3206-4513-b4fa-23913f296dfc"
 HerbCore = "2b23ba43-8213-43cb-b5ea-38c12b45bd45"
 HerbGrammar = "4ef9e186-2fe5-4b24-8de7-9f7291f24af7"
 HerbSearch = "3008d8e8-f9aa-438a-92ed-26e9c7b4829f"
@@ -21,6 +23,7 @@ Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
 DocStringExtensions = "0.9.3"
 DynamicalSystems = "3"
 FileIO = "1"
+HerbConstraints = "0.2.4"
 HerbSearch = "0.4.1"
 MLStyle = "0.4.17"
 MetaGraphsNext = "0.7"

experiments/Synth/Manifest.toml

@@ -2,7 +2,7 @@
 
 julia_version = "1.10.2"
 manifest_format = "2.0"
-project_hash = "19cda9b05e0584d6a0dc95f7351f7b83848951bf"
+project_hash = "db74a993eef408d9b910e97f9a72ec5fee351591"
 
 [[deps.ADTypes]]
 git-tree-sha1 = "72af59f5b8f09faee36b4ec48e014a79210f2f4f"
@@ -936,10 +936,8 @@ uuid = "7746bdde-850d-59dc-9ae8-88ece973131d"
 version = "2.82.4+0"
 
 [[deps.GraphDynamicalSystems]]
-deps = ["AbstractTrees", "DocStringExtensions", "DynamicalSystems", "FileIO", "HerbCore", "HerbGrammar", "HerbSearch", "MLStyle", "MetaGraphsNext", "Random", "SoleLogics", "Statistics"]
-git-tree-sha1 = "8ca1dbca624e42094220e1d15da56da999e82b1b"
-repo-rev = "feat/qn"
-repo-url = "../.."
+deps = ["AbstractTrees", "DocStringExtensions", "DynamicalSystems", "FileIO", "Graphs", "HerbConstraints", "HerbCore", "HerbGrammar", "HerbSearch", "MLStyle", "MetaGraphsNext", "Random", "SoleLogics", "Statistics"]
+path = "../.."
 uuid = "13529e2e-ed53-56b1-bd6f-420b01fca819"
 version = "0.2.0"
 
@@ -1004,9 +1002,7 @@ version = "0.1.6"
 
 [[deps.HerbSearch]]
 deps = ["DataStructures", "HerbConstraints", "HerbCore", "HerbGrammar", "HerbInterpret", "HerbSpecification", "MLStyle", "Random", "StatsBase"]
-git-tree-sha1 = "913c9d8549076d4e13dd5255656177b6893ce6c1"
-repo-rev = "compathelper/new_version/2024-12-13-01-52-34-511-01072321669"
-repo-url = "https://github.com/Herb-AI/HerbSearch.jl.git"
+git-tree-sha1 = "95a5c1e87cd61b14cf9785f293e5633b39a69fc5"
 uuid = "3008d8e8-f9aa-438a-92ed-26e9c7b4829f"
 version = "0.4.1"
 

experiments/Synth/Project.toml

@@ -7,6 +7,7 @@ CSV = "336ed68f-0bac-5ca0-87d4-7b16caf5d00b"
 CondaPkg = "992eb4ea-22a4-4c89-a5bb-47a3300528ab"
 DataFrames = "a93c6f00-e57d-5684-b7b6-d8193f3e46c0"
 Distributed = "8ba89e20-285c-5b6f-9357-94700520ee1b"
+DocStringExtensions = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae"
 DrWatson = "634d3b9d-ee7a-5ddf-bec9-22491ea816e1"
 DynamicalSystems = "61744808-ddfa-5f27-97ff-6e42cc95d634"
 Git = "d7ba0133-e1db-5d97-8f8c-041e4b3a1eb2"
@@ -39,6 +40,7 @@ SoleLogics = "b002da8f-3cb3-4d91-bbe3-2953433912b5"
 StatsPlots = "f3b207a7-027a-5e70-b257-86293d7955fd"
 Term = "22787eb5-b846-44ae-b979-8e399b8463ab"
 TidierData = "fe2206b3-d496-4ee9-a338-6a095c4ece80"
+UnicodePlots = "b8865327-cd53-5732-bb35-84acbb429228"
 XML = "72c71f33-b9b6-44de-8c94-c961784809e2"
 
 [compat]

experiments/Synth/scripts/synth_biodivine.jl

@@ -21,27 +21,73 @@ end
 @everywhere quickactivate(pwd())
 @everywhere using Synth
 
-@everywhere using ProgressMeter, DataFrames, HerbSearch, GraphDynamicalSystems
+@everywhere using ProgressMeter, DataFrames, HerbSearch, GraphDynamicalSystems, Random
+using MetaGraphsNext: labels
 
-res = collect_results(datadir("sims", "biodivine_split"))
-res.ID = ((x -> x[end-1]["id"]) ∘ parse_savename).(res.path)
-rename!(res, :path => "Trajectory Path")
-mg_df = collect_results(datadir("src_parsed", "biodivine_benchmark_as_metagraphs");)
-mg_df.ID = ((x -> parse(Int, x)) ∘ (x -> x[1]) ∘ splitext ∘ basename).(mg_df.path)
-rename!(mg_df, :path => "Model Path")
+traj_df = collect_results(datadir("sims", "biodivine_split"))
+path2id = path -> parse_savename(path)[end-1]["id"]
+traj_df.ID = path2id.(traj_df.path)
 
-res = innerjoin(res, mg_df, on = :ID)
+model_df = collect_results(datadir("src_parsed", "biodivine_benchmark_as_metagraphs");)
+path2id = path -> parse(Int, splitext(basename(path))[1])
+model_df.ID = path2id.(model_df.path)
+model_df.vertex = collect.(labels.(model_df.metagraph_model))
+# add a copy so that after flattening we have all of the vertices of a model in each row of df
+model_df.vertices = model_df.vertex
+
+# Filter only smaller models
+# model_df = model_df[length.(model_df.vertices).<15, :]
+
+per_vertex_df = flatten(model_df, :vertex)
+
+grammars_df = model_df[!, [:ID, :vertices]]
+grammars_df.dnf_grammar = build_dnf_grammar.(grammars_df.vertices)
+grammars_df.qn_grammar = build_qn_grammar.(grammars_df.vertices)
+
+get_evaluator = g -> Dict([:DNF => evaluate_bn, :QN => evaluate_qn])[g]
+
+function get_grammar(unique, grammar_type)
+    s = :unknown
+    if grammar_type == :DNF
+        s = :dnf_grammar
+    elseif grammar_type == :QN
+        s = :qn_grammar
+    end
+
+    return only(grammars_df[grammars_df.ID.==unique.ID, s])
+end
+
+function select_trajectories(df, N, id, vertex, seed)
+    Random.seed!(seed)
+    selected_trajectories = rand(only(df[df.ID.==id, :split_traj]), N)
+    filtered_on_vertex =
+        reduce(union, map(x -> get(x, vertex, Set()), selected_trajectories))
+
+    return filtered_on_vertex
+end
 
 synth_params = Dict(
     "seed" => 42,
     "max_depth" => 6,
-    "id" => res.ID,
+    "unique" => collect(eachrow(per_vertex_df[!, [:ID, :vertex, :vertices]])),
+    "id" => Derived("unique", x -> x.ID),
+    "vertex_names" => Derived("unique", x -> getfield.(x.vertices, :value)),
+    "index_of_vertex" => Derived("unique", x -> findfirst(==(x.vertex), x.vertices)),
+    "vertex" => Derived("unique", x -> string(x.vertex.value)),
     "n_trajectories" => collect(10:45:110),
+    "selected_trajectories" => Derived(
+        ["n_trajectories", "unique", "index_of_vertex", "seed"],
+        (N, unique, index_of_vertex, seed) ->
+            select_trajectories(traj_df, N, unique.ID, index_of_vertex, seed),
+    ),
     "iterator_type" => [BFSIterator],
-    "grammar_builder" => [build_dnf_grammar, build_qn_grammar],
+    "iter_name" => Derived("iterator_type", string),
+    "grammar_type" => [:DNF, :QN],
+    "grammar" => Derived(["unique", "grammar_type"], get_grammar),
+    "evaluator" => Derived("grammar_type", get_evaluator),
     "max_iterations" => 1_000_000,
 )
 
 @showprogress pmap(dict_list(synth_params)) do params
-    synth_one_biodivine(params, res)
+    @produce_or_load(synth_one_vertex, params, datadir("exp_raw", "biodivine_search"))
 end

experiments/Synth/src/Synth.jl

@@ -27,16 +27,20 @@ include("gather_bn_data.jl")
 
 export gather_bn_data, split_state_space, get_split_state_space
 
-include("create_problem.jl")
+include("synth_process.jl")
 
-export examples_to_problem
+export synth, synth_biodivine
+
+include("undirected_specification.jl")
+
+export UndirectedExample, UndirectedProblem
 
 include("evaluator.jl")
 
-export evaluate_bn, interpret
+export evaluate_bn, evaluate_qn, interpret
 
-include("synth_process.jl")
+include("create_problem.jl")
 
-export synth, synth_biodivine
+export examples_to_problem
 
 end

experiments/Synth/src/biodivine_benchmark.jl

@@ -146,49 +146,17 @@ function convert_aeon_models_to_metagraphs(excluded_files = Regex[])
     end
 end
 
-function synth_one_biodivine(outer_params::AbstractDict{String,Any}, res::DataFrame)
-    params = deepcopy(outer_params)
-    @unpack seed = params
-    Random.seed!(seed)
-
-    @unpack n_trajectories, id = params
-    selected_trajs = rand(only(res[res.ID.==id, :split_traj]), n_trajectories)
-
-    merged_selected_trajs = reduce(mergewith(union), selected_trajs)
-
-    @unpack id, grammar_builder = params
-    @info "Synthsizing for model $id with $n_trajectories traj."
-
-    model = only(res[res.ID.==id, :metagraph_model])
-    grammar = grammar_builder(nv(model))
-
-    @showprogress map(collect(merged_selected_trajs)) do (vertex, examples)
-        @info "Synthesizing model $id, node $vertex, $n_trajectories traj."
-        save_data = deepcopy(params)
-        delete!(save_data, "specifications")
-        save_data["grammar"] = grammar
-        save_data["vertex"] = vertex
-        save_data["examples"] = examples
-        file_name = savename(save_data)
-        @produce_or_load(
-            synth_one_vertex,
-            save_data,
-            datadir("exp_raw", "biodivine_search");
-            filename = file_name
-        )
-        @info "Completed synthesis for model $id, node $vertex, $n_trajectories traj."
-    end
-end
-
-function synth_one_vertex(save_data)
-    @unpack vertex, examples = save_data
-    problem = examples_to_problem(vertex, examples)
+function synth_one_vertex(params::AbstractDict{String,Any})
+    @unpack vertex, selected_trajectories = params
+    problem = examples_to_problem(vertex, selected_trajectories)
 
-    @unpack max_depth, iterator_type, max_iterations, grammar = save_data
+    @unpack max_depth, iterator_type, max_iterations, grammar, evaluator, vertex_names =
+        params
     iterator = iterator_type(grammar, :Start, max_depth = max_depth)
-    exprs_and_scores = synth_biodivine(problem, iterator, grammar, max_iterations)
+    exprs_and_scores =
+        synth_biodivine(problem, iterator, grammar, max_iterations, evaluator, vertex_names)
 
     # Save output
-    save_data["exprs_and_scores"] = exprs_and_scores
-    return save_data
+    params["exprs_and_scores"] = exprs_and_scores
+    return params
 end

experiments/Synth/src/create_problem.jl

@@ -1,7 +1,9 @@
-function examples_to_problem(node, examples)
-    io_examples =
-        map(((in, out),) -> IOExample(Dict([:state => in]), out), collect(examples))
-    problem = Problem("$node", io_examples)
+function _e2p(n, e)
+    _pair_to_undirected(p) = UndirectedExample(Dict(:state => p[1]), Dict(:state => p[2]))
 
-    return problem
+    return UndirectedProblem(n, _pair_to_undirected.(e))
 end
+
+examples_to_problem(node::Integer, examples::AbstractSet) = _e2p(string(node), examples)
+examples_to_problem(node::Atom, examples) = _e2p(node.value, examples)
+examples_to_problem(node::AbstractString, examples) = _e2p(node, examples)

experiments/Synth/src/evaluator.jl

@@ -29,14 +29,73 @@ function interpret(φ::Expr, i::SoleLogics.AbstractInterpretation, args...; kwar
     return interpret(syntax_branch, i, args...; kwargs...)
 end
 
-function evaluate_bn(problem, expr)
-    sat_examples = 0
+function interpret(
+    e::Union{AbstractString,Integer,Expr},
+    qn_state::AbstractVector{<:Integer},
+    vertex_names::AbstractVector{<:AbstractString},
+)
+    state_map = Dict(zip(vertex_names, deepcopy(qn_state)))
 
-    for example ∈ problem.spec
-        truth = TruthDict(Dict(enumerate(example.in[:state])))
+    _int(e) = @match e begin
+        ::AbstractString => state_map[e]
+        ::Integer => e
+        :($v1 + $v2) => _int(v1) + _int(v2)
+        :($v1 - $v2) => _int(v1) - _int(v2)
+        :($v1 / $v2) => _int(v1) / _int(v2)
+        :($v1 * $v2) => _int(v1) * _int(v2)
+        :(Min($v1, $v2)) => min(_int(v1), _int(v2))
+        :(Max($v1, $v2)) => max(_int(v1), _int(v2))
+        :(Ceil($v)) => ceil(_int(v))
+        :(Floor($v)) => floor(_int(v))
+        _ => error("Unhandled Expr in `interpret`: $e, $(typeof(e))")
+    end
+
+    return _int(e)
+end
+
+function evaluate_bn(problem::UndirectedProblem, expr, vertex_names)
+    sat_examples = BitVector[]
+
+    function _eval_1_dir(in, out)
+        truth = TruthDict(Dict(zip(vertex_names, in[:state])))
         res = interpret(expr, truth)
-        sat_examples += res.flag == example.out
+        expected = BooleanTruth(out[:state][findfirst(==(problem.name), vertex_names)])
+        success = expected == res
+
+        return success
+    end
+
+    for example ∈ problem.examples
+        success_direction1 = _eval_1_dir(example.data1, example.data2)
+        success_direction2 = _eval_1_dir(example.data2, example.data1)
+
+        success = BitVector([success_direction1, success_direction2])
+
+        push!(sat_examples, success)
+    end
+
+    return sat_examples
+end
+
+function evaluate_qn(problem::UndirectedProblem, expr, vertex_names)
+    sat_examples = BitVector[]
+
+    function _eval_1_dir(in, out)
+        res = interpret(expr, in[:state], vertex_names)
+        expected = out[:state][findfirst(==(problem.name), vertex_names)]
+        success = expected == res
+
+        return success
+    end
+
+    for example ∈ problem.examples
+        success_direction1 = _eval_1_dir(example.data1, example.data2)
+        success_direction2 = _eval_1_dir(example.data2, example.data1)
+
+        success = BitVector([success_direction1, success_direction2])
+
+        push!(sat_examples, success)
     end
 
-    return sat_examples / length(problem.spec)
+    return sat_examples
 end

experiments/Synth/src/gather_bn_data.jl

@@ -7,30 +7,24 @@ end
 
 function split_state_space(trajectory::StateSpaceSet)
     # split into pairs of input (all values) and output (changed value)
-    input_output_pairs_per_node = Dict{Int,Set{Tuple{Vector{Int},Int}}}()
+    #
+    input_output_pairs_per_node = Dict{Int,Set{Tuple{Vector{Int},Vector{Int}}}}()
     for i = 1:length(trajectory)-1
         changed = findfirst(trajectory[i+1] .!= trajectory[i])
         # only proceed if there was a change
         if !isnothing(changed)
 
             # in real data we don't know the direction of the transition
             # was it from i -> i+1 or i+1 -> i, we only know that two
-            # states are adjacent, so for gathering data, we add both
-            # directions as IO pairs
-            #   1. state `i` and the new value of the single variable in
-            #      the state that changed
-            #   2. state `i+1` and the previous value of the single variable
-            #      in the state that changed
+            # states are adjacent, so for synthesis, we want to add the pair
+            # of i and i+1, and test possible programs on both.
 
-            new_value = trajectory[i+1][changed]
-            old_value = trajectory[i][changed]
-            existing_pairs =
-                get(input_output_pairs_per_node, changed, Set{Tuple{Vector{Int},Int}}())
-            push!(
-                existing_pairs,
-                (trajectory[i], new_value),     # 1
-                (trajectory[i+1], old_value),   # 2
+            existing_pairs = get(
+                input_output_pairs_per_node,
+                changed,
+                Set{Tuple{Vector{Int},Vector{Int}}}(),
             )
+            push!(existing_pairs, (trajectory[i], trajectory[i+1]))
             input_output_pairs_per_node[changed] = existing_pairs
         end
     end