Zulip Chat Archive

Stream: lean-gptf

Topic: Automatic lemma name suggestion


view this post on Zulip Jesse Michael Han (Feb 08 2021 at 21:40):

New feature: the autoname tactic will ask GPT-f to suggest a name for the main goal. You can use it by importing tactic.autoname. It seems to suggest sensible names for even nonexistent lemmas. Please try it out and let us know if it makes interesting suggestions!

Please note, autonameonly works with the current model formal-lean-wm-to-tt-m1-m2-v4-c4.

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:31):

It seems to suggest sensible names for even nonexistent lemmas.

On a completely unseen test set of ~2800 theorems from future (relative to the training data) commits of mathlib, it correctly guesses the names of 20% of them on the first try, 27% within 10 tries, and 30% within 16 tries.

view this post on Zulip Mario Carneiro (Feb 09 2021 at 04:32):

that actually seems a bit low

view this post on Zulip Mario Carneiro (Feb 09 2021 at 04:33):

what kind of errors is it making?

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:35):

it seems to have overfitted a bit to the existing theorem names, which makes sense because there are so few datapoints compared to even tactic proof steps

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:36):

for example, it is confused by ordnode-related stuff because it never saw anything related to it:

-- failed example
{"name": "ordnode.raised_iff", "predictions": [["ordinal.raise_le", -2.33270406723022], ["ordinal.9", -3.3633086681366], ["ordinal.raise_iff", -4.30675172805786], ["ordinal.raise_eq", -5.1791844367981], ["ordinal.out_id", -6.36061859130859], ["ordinal.raise_eq_nat_iff", -7.46061277389526], ["ordinal.lt_omega", -9.32905387878418], ["ordinal.raise_is_le", -9.94356060028076], ["ordinal. Yu", -10.3971786499023], ["ordinal. decorated_lt", -10.8216419219971], ["ordinal. isolated_def", -10.8895788192749], ["ordinal. amplitude_lt", -11.2980804443359], ["ordinal. Claim_le", -12.0608367919922], ["ordinal.tropate_eq_out", -14.9426021575928], ["ordinal. Soften_open", -20.6884441375732], ["ordinal.Ju Frequency_λ", -22.9329662322998]], "type": "∀ {n m : ℕ}, ordnode.raised n m ↔ n ≤ m ∧ m ≤ n + 1"}

view this post on Zulip Mario Carneiro (Feb 09 2021 at 04:37):

It did get the raise_iff part right, but it seems to have trouble guessing the namespace

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:38):

indeed, it was trained on and, in the evaluation above, was required to guess fully qualified names --- the numbers will probably go up if we relax this and open the namespaces

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:39):

random sample of top1 successful guesses:

{"name": "finset.product_eq_bUnion", "predictions": [["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_eq_bUnion", -0.29872065782547], ["finset.product_def", -1.84102940559387], ["finset.product_def", -1.84102940559387], ["finset.product_def", -1.84102940559387], ["finset.product_def", -1.84102940559387], ["finset.product_def", -1.84102940559387], ["finset.product_def", -1.84102940559387], ["finset.product_eq_bUnion'", -4.21205139160156]], "type": "∀ {α : Type u_1} {β : Type u_2} [_inst_1 : decidable_eq α] [_inst_2 : decidable_eq β] (s : finset α) (t : finset β), s.product t = s.bUnion (λ (a : α), finset.image (λ (b : β), (a, b)) t)"}
{"name": "quotient_map.surjective", "predictions": [["quotient_map.surjective", -1.01991152763367], ["quotient_map.surjective", -1.01991152763367], ["quotient_map.surjective", -1.01991152763367], ["quotient_map.surjective", -1.01991152763367], ["quotient_map.surjective", -1.01991152763367], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.function_surjective", -1.22668278217316], ["quotient_map.right_surjective", -2.3489830493927], ["quotient_map.to_surjective", -2.60883545875549], ["quotient_map. function_surjective", -5.94958400726318], ["surjective_of_quotient_uniform", -14.6107892990112]], "type": "∀ {α : Type u_1} {β : Type u_2} [_inst_1 : topological_space α] [_inst_2 : topological_space β] {f : α → β}, quotient_map f → function.surjective f"}
{"name": "option.pbind_eq_bind", "predictions": [["option.pbind_eq_bind", -1.11646616458893], ["option.pbind_eq_bind", -1.11646616458893], ["option.pbind_eq_bind", -1.11646616458893], ["option.pbind_eq_bind", -1.11646616458893], ["option.pbind_eq_bind'", -2.84433674812317], ["option.bind_punit", -4.84474229812622], ["option.bind_pf", -5.29447889328003], ["option.bind_pindex", -5.44013738632202], ["option.bind_idem", -6.99253129959106], ["option.seq_bind'", -7.45541572570801], ["option.bind_pbind", -7.45678329467773], ["option.bind_ only", -9.34739589691162], ["option.bind_pcont", -9.50272941589355], ["option.bind_pSong_eq_filter", -17.9352874755859], ["option.bind_is_filter_ mid", -21.887788772583], ["option.dense_NF_preserves", -30.1571636199951]], "type": "∀ {α : Type u_1} {β : Type u_2} (f : α → option β) (x : option α), x.pbind (λ (a : α) (_x : a ∈ x), f a) = x.bind f"}
{"name": "mv_polynomial.C_surjective", "predictions": [["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C_surjective", -0.445991665124893], ["mv_polynomial.C.surjective", -2.33550643920898], ["mv_polynomial.C.surjective", -2.33550643920898], ["mv_polynomial.C.surjective", -2.33550643920898], ["mv_polynomial.iter_to_sum._proof_1", -11.8020257949829], ["mv_polynomial.Exists_C_surjective", -12.5675983428955], ["mv_polynomial.C.surjective_ Type", -13.9191789627075], ["ring_hom.Sup_of_empty", -15.2716293334961]], "type": "∀ {R : Type u_1} [_inst_2 : comm_semiring R] (σ : Type u_2), ¬nonempty σ → function.surjective ⇑mv_polynomial.C"}
{"name": "real.measurable_arccos", "predictions": [["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["real.measurable_arccos", -0.101719327270985], ["has_continuous_arccos.measurable_arccos", -11.9590692520142]], "type": "measurable real.arccos"}
{"name": "homeomorph.preimage_closure", "predictions": [["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure", -0.249808266758919], ["homeomorph.preimage_closure_eq", -4.19137573242188], ["homeomorph.preimage_closed_of_closure", -4.7142653465271], ["homeomorph.preimage_dense_of_dense", -9.04643535614014]], "type": "∀ {α : Type u_1} {β : Type u_2} [_inst_1 : topological_space α] [_inst_2 : topological_space β] (h : α ≃ₜ β) (s : set β), ⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)"}
{"name": "set.pi_inter_compl", "predictions": [["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl", -0.726515233516693], ["set.pi_inter_compl_pi", -1.7950279712677], ["set.pi_inter_compl_pi", -1.7950279712677], ["set.pi_compl_inter_compl", -5.31532955169678], ["set.pi_compl_inter_compl", -5.31532955169678], ["set.pi_rest", -7.69228172302246], ["set.pi_inter_pi_compl_eq_univ", -10.8894968032837], ["set.pi_univ_inter_symm_pi", -11.4858512878418]], "type": "∀ {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} (s : set ι), s.pi t ∩ sᶜ.pi t = set.univ.pi t"}
{"name": "measurable.ennreal_inv", "predictions": [["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.ennreal_inv", -0.139067500829697], ["measurable.inv", -2.66454648971558], ["measurable.inv", -2.66454648971558], ["measurable.inv", -2.66454648971558], ["measurable.ennreal_inv_nnreal", -7.25561428070068], ["measurable.inv_upper_measurable", -12.270655632019]], "type": "∀ {α : Type u_1} [_inst_1 : measurable_space α] {f : α → ennreal}, measurable f → measurable (λ (a : α), (f a)⁻¹)"}
{"name": "set.pi_congr", "predictions": [["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr", -0.169505730271339], ["set.pi_congr_left", -3.86984658241272], ["set.pi_eq_pi", -6.06816530227661], ["set.pi_congr_pos", -8.94440460205078]], "type": "∀ {ι : Type u_1} {α : ι → Type u_2} {s s₁ : set ι} {t t₁ : Π (i : ι), set (α i)}, s = s₁ → (∀ (i : ι), i ∈ s → t i = t₁ i) → s.pi t = s₁.pi t₁"}

view this post on Zulip Mario Carneiro (Feb 09 2021 at 04:42):

has_continuous_arccos.measurable_arccos :grinning:

view this post on Zulip Mario Carneiro (Feb 09 2021 at 04:43):

a trailblazer

view this post on Zulip Bryan Gin-ge Chen (Feb 09 2021 at 04:45):

Could the Yu in ["ordinal. Yu", -10.3971786499023] be coming from Yury's name in copyright headers or is that not included in the training data?

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:46):

copyright headers are definitely not in the training data, however, these models were pretrained on the WebMath corpus, so it has seen a fair bit of non-Lean English

view this post on Zulip Jesse Michael Han (Feb 09 2021 at 04:50):

Mario Carneiro said:

has_continuous_arccos.measurable_arccos :grinning:

it evidently got bored of predicting real.measurable_arccos and decided to have fun instead :upside_down:


Last updated: May 18 2021 at 10:14 UTC