Automatic lemma name suggestion

Stream: lean-gptf

[Jesse Michael Han]

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.

[Jesse Michael Han]

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.

[Mario Carneiro]

that actually seems a bit low

[Mario Carneiro]

what kind of errors is it making?

[Jesse Michael Han]

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

[Jesse Michael Han]

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"}

[Mario Carneiro]

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

[Jesse Michael Han]

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

[Jesse Michael Han]

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₁"}

[Mario Carneiro]

has_continuous_arccos.measurable_arccos :grinning:

[Mario Carneiro]

a trailblazer

[Bryan Gin-ge Chen]

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?

[Jesse Michael Han]

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

[Jesse Michael Han]

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: