Zulip Chat Archive

Stream: lean-gptf

Topic: Custom prefixes


view this post on Zulip Jesse Michael Han (Jan 29 2021 at 05:48):

New feature: you can now call gptf {pfx := $TAC} to force gptf to create a prediction using a certain tactic! For example, you can do gptf {pfx := "rw"} (resp. apply, exact, simp...). It's really interesting seeing what it thinks are good simp lemmas and what is a good idea to try for exact.

view this post on Zulip Jesse Michael Han (Jan 29 2021 at 21:38):

You can now also pass an arbitrary postprocessing function, which lets you e.g. ask the model to predict rw hypotheses, then use them for [smt] eblast_using .... This example is now available as neuro_eblast.


Last updated: May 18 2021 at 10:14 UTC