ML/AI/ChatGPT?

[ninehusky]

Sorin mentioned this idea in last week's meeting; is mentioned in #15 .

The ML angle is interesting here; traditional synthesis tools infer some sort of PCFG that is used to identify "likely candidates". Although, in our case, I'm not sure what that would look like. We're trying to find all (or many) programs that match a spec, not trying to find a specific solution.

The easiest thing we could do is just to ask ChatGPT what it thinks some valid rewrite rules are. We could feed it the existing handwritten rules for Halide and see if it gives us anything different than what's already there. Some things to brainstorm:

• How can we use ChatGPT alongside bottom-up enumeration?
• Does ChatGPT let us unlock domains which were previously prohibitively expensive?
• (How) Should we change Chompy's main API so that we can "fast forward" the enumeration process given ChatGPT's set of rules?

Setting up an initial experiment, and just seeing what rules it outputs would be good. This probably involves:

• Bothering someone in the lab with more ChatGPT knowledge/getting an account.
• Configuring necessary prompt engineering files
• Updating Chompy infrastructure to include a llm_generate_rule function from () -> Vec<Rule>.

[ninehusky]

A sample ruleset that GPT outputs:

Rules:
(Rules generated: 60)
(Add ?a (Const 0)) ~> ?a
(Add (Const 0) ?a) ~> ?a
(Sub ?a (Const 0)) ~> ?a
(Mul ?a (Const 1)) ~> ?a
(Mul (Const 1) ?a) ~> ?a
(Mul ?a (Const 0)) ~> (Const 0)
(Mul (Const 0) ?a) ~> (Const 0)
(Div ?a (Const 1)) ~> ?a
(Abs ?a) ~> ?a if (Gt ?a (Const 0))
(Abs ?a) ~> (Sub (Const 0) ?a) if (Lt ?a (Const 0))
(Add ?a ?b) ~> (Add ?b ?a)
(Mul ?a ?b) ~> (Mul ?b ?a)
(Sub ?a ?b) ~> (Add ?a (Sub (Const 0) ?b))
(Div ?a (Const 1)) ~> ?a
(Div (Const 0) ?a) ~> (Const 0) if (Neq ?a (Const 0))
(Add ?a (Const ?c)) ~> (Add (Const ?c) ?a)
(Sub ?a (Const ?c)) ~> (Add ?a (Mul (Const -1) (Const ?c)))
(Mul ?a (Const -1)) ~> (Sub (Const 0) ?a
(Mul (Const -1) ?a) ~> (Sub (Const 0) ?a)
(Div (Const ?c) ?a) ~> (Mul (Const (?c // 1)) (Div (Const 1) ?a)) if (Neq ?a (Const 0))
(Abs (Mul ?a (Const -1))) ~> (Abs ?a)
(Neq ?a ?a) ~> (Const 0)
(Eq ?a ?a) ~> (Const 1)
(Gt ?a ?b) ~> (Lt ?b ?a)
(Ge ?a ?b) ~> (Neq ?a ?b)
(Gt ?a ?b) ~> (Eq ?a ?b)
(Add (Mul ?a (Const 0)) ?b) ~> ?b
(Add ?a (Mul (Const 1) ?b)) ~> (Add ?a ?b)
(Gt ?a (Const 1)) ~> (Ge (Add ?a (Const -1)) (Const 0))
(Lt (Add ?a ?b) (Add ?c ?d)) ~> (Or (Lt ?a ?c) (Lt ?b ?d))
(Mul ?a (Abs ?b)) ~> (Abs (Mul ?a ?b))
(Div ?a (Abs ?b)) ~> (Div (Abs ?a) ?b) if (Neq ?b (Const 0))
(Eq (Abs ?a) (Abs ?b)) ~> (Or (Eq ?a ?b) (Eq ?a (Mul (Const -1) ?b)))
(Sub ?a ?a) ~> (Const 0)
(Add ?a (Sub ?a ?b)) ~> ?b
(Div (Sub ?a ?b) ?c) ~> (Sub (Div ?a ?c) (Div ?b ?c)) if (Neq ?c (Const 0))
(Mul ?a (Add ?b ?c)) ~> (Add (Mul ?a ?b) (Mul ?a ?c))
(Sub (Mul ?a ?b) (Mul ?a ?c)) ~> (Mul ?a (Sub ?b ?c))
(Div (Add ?a ?b) (Add ?c ?d)) ~> (Add (Div ?a ?c) (Div ?b ?d)) if (Neq ?c (Const 0))
(Gt ?a (Const 0)) ~> (Ge (Mul (Const -1) ?a) (Const 0))
(Mul ?a (Add ?b ?c)) ~> (Add (Mul ?a ?b) (Mul ?a ?c))
(Mul (Abs ?a) (Const -1)) ~> (Sub (Const 0) (Abs ?a))
(Neq (Div ?a ?b) (Div ?c ?d)) ~> (Or (Neq ?a ?c) (Neq ?b ?d)) if (Neq ?b (Const 0) and Neq ?d (Const 0))
(Abs (Div ?a ?b)) ~> (Div (Abs ?a) (Abs ?b)) if (Neq ?b (Const 0))
(Mul (Add ?a ?b) (Const ?c)) ~> (Add (Mul ?a (Const ?c)) (Mul ?b (Const ?c)))
(Div (Add ?a ?b) (Const ?c)) ~> (Add (Div ?a (Const ?c)) (Div ?b (Const ?c))) if (Neq ?c (Const 0))
(Abs (Add ?a ?b)) ~> (Add (Abs ?a) (Abs ?b)) if (Gt ?a (Const 0))
(Gt (Sub ?a ?b) (Const 0)) ~> (Gt ?a ?b)
(Div ?a (Mul ?b ?c)) ~> (Div (Div ?a ?b) ?c) if (Neq ?b (Const 0))
(Neq ?a ?b) ~> (Eq ?a (Const 0)) if (Neq ?a ?b)
(Neq ?a ?b) ~> (Neq (Abs ?a) (Abs ?b))
(Eq (Mul ?a (Const 1)) ?a) ~> (Const 1)
(Eq (Mul ?a (Const 0)) ?a) ~> (Sub (Const 0) ?a)
(Gt (Add ?a ?b) (Const 0)) ~> (Or (Gt ?a (Const 0)) (Gt ?b (Const 0)))
(Lt (Sub ?a ?b) (Const 0)) ~> (Gt ?a ?b)
(Abs ?a) ~> (Abs (Mul ?a (Const -1)))
(Mul (Const 2) ?a) ~> (Add ?a ?a)
(Mul (Const 3) ?a) ~> (Add ?a (Add ?a ?a))
(Div ?a (Const 2)) ~> (Mul ?a (Const 0.5)) if (Neq ?a (Const 0))
(Add (Div ?a ?b) (Div ?c ?b)) ~> (Div (Add ?a ?c) ?b) if (Neq ?b (Const 0))

Some good rules it gets:

• (Div (Add ?a ?b) (Const ?c)) ~> (Add (Div ?a (Const ?c)) (Div ?b (Const ?c))) if (Neq ?c (Const 0))
  ^ this is good (and big!), even though it doesn't follow what our custom division semantics are (a / b = 0 if b = 0 else a / b)
  Some problems:
• It seems to insist on putting the if blah at the end of the rule, even though I told it not to
• Ungrammatical rules (see the //) : (Div (Const ?c) ?a) ~> (Mul (Const (?c // 1)) (Div (Const 1) ?a)) if (Neq ?a (Const 0))
• Unsound rules: (Neq (Div ?a ?b) (Div ?c ?d)) ~> (Or (Neq ?a ?c) (Neq ?b ?d)) if (Neq ?b (Const 0) and Neq ?d (Const 0))<-- this would say that (1 / 2) != (2 / 4) ~> true
• (Div ?a (Const 2)) ~> (Mul ?a (Const 0.5)) if (Neq ?a (Const 0)) <-- not in the grammar of the language (and the condition is unnecessary)

[ninehusky]

this seems to indicate that GPT can't just replace chompy. (also, in the prompt we asked it for 100 rules, but only got 60). but it does seem to indicate that GPT could be used to kick-start chompy, i.e., give it some initial set of rules that we can use to explore more. (i think in the enumo paper this is called "fast forwarding"?)

something basic i'd like to whip up before friday's meeting is set up experiments where we do:

gpt_rules = gpt_rules().sort()
initial_rules = []
for r in gpt_rules():
   if not r.is_valid() and not is_derivable(initial_rules, r):
      initial_rules.add(r)

# fast forward chompy
chompy_plus_gpt_rules = run_chompy(initial_rules)
just_chompy_rules = run_chompy([])

# now, how does just_chompy_rules compare with chompy_plus_gpt?

[Riddhimaan-Senapati]

It might be better to train a RAG/finetune LLMs on valid rules/ (or docs on how to create valid rules) for better accuracy.

[ninehusky]

Yeah, I think fine tuning is definitely an option here.