Artifact of Distance-Guided Search in Program Synthesis with Imperfect LLM Solutions

Installation

1. Install opam, the OCaml package manager.

2. Install OCaml 4.10.0+flambda with the flambda optimizer by running opam switch create 4.10.0+flambda. OCaml versions after 4.10.0 should work fine too, but are untested.

3. Run make deps in the root directory of this project to download all the necessary opam dependencies.

4. Run make to build the Trio executable. The executable is accessible via the trio symlink in the root directory of this project.

Running the Tool

You can run Trio to solve a single benchmark as follows:

$ ./trio [trio options] [benchmark file]

For example, to solve the single benchmark in test/auto_gen/nat_mul.mls

$ ./trio test/auto_gen/nat_mul.mls

The following options are available.

  -time Print time taken
  -print_blocks Print all block expressions
  -get_size Get size of an expression
  -all Find all solutions and pick the smallest one
  -rec solution must be recursive
  -noinvmap don't use inverse maps of external functions
  -debug print info for debugging
  -help  Display this list of options
  -ai_guide AI guided synthesis. It needs AI Solution file. (At llm/llm_solutions/guide)
  -ai_comp AI guided synthesis with ai_components. If you want to top-down guide only, exclude this option.
  -convert Convert the AI_solution to ML-Like dsl.
  -pcfg Use PCFG to guide synthesis. It needs llm.sols file. (At llm/llm_solutions/pcfg)

Test : Synthesizer Only - Unguided Synthesis

Note: The default Trio configuration in this project has block-based pruning turned off. You can run Trio to solve a single benchmark without any guidance as follows:

$ ./trio test/auto_gen/list_drop.mls

Generating LLM Solutions

Using the GPT API to generate LLM-based solutions can be non-deterministic and costly. Therefore, we recommend leveraging pre-generated data whenever possible. Pre-generated LLM solution data is available in the llm/llm_solutions directory. The llm/llm_solutions/guide directory contains the final solutions generated for each model. The llm/llm_solutions/pcfg directory contains 100 generated solution samples for pcfg testing.

Test : Guided Synthesis with LLM solutions

You can run Guided synthesis to solve a single benchmark with LLM data as follows. If LLM solution is correct, it will be done without any synthesis.

$ ./trio -convert -ai_comp -ai_guide [llm solution.sol] [benchmark.mls]

For example,

./trio -convert -ai_comp -ai_guide llm/llm_solutions/guide/gpt-4o-mini/list_sum_larger.sol test/auto_gen/list_sum_larger.mls

Then you will get the following result:

let rec (f : ((list * list) -> nat)) =
  fun (x:(list * list)) ->
    match (x).0 with
    | Nil(_) ->
      O([])
    | Cons(_) ->
      match (x).1 with
      | Nil(_) ->
        (Un_Cons((x).0)).0
      | Cons(_) ->
        match ((compare (Un_Cons((x).0)).0) (Un_Cons((x).1)).0) with
        | EQ(_) ->
          (f [(x).0, (Un_Cons((x).1)).1])
        | GT(_) ->
          ((add (Un_Cons((x).0)).0) (f [(Un_Cons((x).0)).1, (x).1]))
        | LT(_) ->
          ((add (Un_Cons((x).1)).0) (f [(Un_Cons((x).0)).1, (Un_Cons((x).1)).1]))

LLM solutions are located in the following directory:

llm/llm_solutions/guide/[ gpt-4o-mini | gpt-4o | o3-mini ]/[PROBLEM].sol

Test : Topdown guide only synthesis

If you do it without the ai_comp option, you can run topdown guide only synthesis as follows:

$ ./trio -convert -ai_guide [llm solution.sol] [benchmark.mls]

For example,

./trio -convert -ai_guide llm/llm_solutions/guide/gpt-4o-mini/tree_bonus.sol test/auto_gen/tree_bonus.mls

Then you will get the following result:

let rec (f : (tree -> nat)) =
  fun (x:tree) ->
    match x with
    | Leaf(_) ->
      Un_Leaf(x)
    | Node(_) ->
      ((div (f (Un_Node(x)).2)) S(((sub S(O([]))) (Un_Node(x)).0)))

Test : Guided Synthesis with PCFG

You can run Guided synthesis to solve a single benchmark with PCFG data as follows:

$ ./trio -convert -pcfg [llm solution.sols] [benchmark.mls]

For example,

./trio -convert -pcfg llm/llm_solutions/pcfg/pcfg_gpt-4o-mini_data/list_append.sols test/auto_gen/list_append.mls

Then you will get the following result:

let rec (f : ((list * list) -> list)) =
  fun (x:(list * list)) ->
    match (x).0 with
    | Nil(_) ->
      (x).0
    | Cons(_) ->
      match (Un_Cons((x).0)).0 with
      | O(_) ->
        Cons([(Un_Cons((x).0)).0, (x).0])
      | S(_) ->
        Cons([(Un_Cons((x).0)).0, Cons([O([]), (x).1])])