New Proofs Generated by Machines by yangky11 · Pull Request #14 · zhangir-azerbayev/ProofNet

yangky11 · 2023-05-28T05:42:42Z

Hi Zhangir,

We evaluated our machine learning prover on ProofNet and found some new proofs.

zhangir-azerbayev · 2023-05-28T18:56:29Z

One thing I am concerned about is that including proofs in this Github repo will result in lots of models being trained on them. Would it be possible to instead add these machine proofs as an extra column to the huggingface dataset and add a line in this repo's README pointing to huggingface?

I already regret hosting any part of this benchmark on Github, but at least the formal proofs can be saved from data contamination.

alreadydone

It turns out many of the "solutions" are due to erroneous formalization.

Personally, I'd like to see techniques like reflection, self-consistency, and refinement/debate/critique etc. be used together with autoformalization to automatically catch dubious formalizations and generate reasoning traces / CoT (ToT?) data that could be used to fine-tune the model.

It does not seem outlandish to hope LLMs could become sample efficient enough to master a subject just by reading a book on it, doing all exercises, and fine-tuning on all thoughts generated in the process. It seems people are having success building customer service bots etc. by embedding and retrieving from documentation and historical Q&A data and prompting with retrieved entries, without the need of fine-tuning; nowadays there are even long context models like MPT-65k and Claude-100k that can fit a whole book into their working memory. However, for hard tasks like mathematics, I think fine-tuning on synthetic reasoning data would definitely be beneficial, given unsatisfactory reasoning capabilities of current (especially open source) models.

alreadydone · 2023-05-28T20:03:24Z

 theorem exercise_2_1_26 {G : Type*} [group G] 
  [fintype G] (a : G) : ∃ (n : ℕ), a ^ n = 1 :=
-sorry
+begin
+  exact ⟨0, pow_zero a⟩,
+end


The exercise states "positive integer".

alreadydone · 2023-05-28T20:05:33Z

 theorem exercise_7_1_12 {F : Type*} [field F] {K : subring F}
  (hK : (1 : F) ∈ K) : is_domain K :=


hK is redundant by definition of subring in mathlib (see subring.one_mem).

alreadydone · 2023-05-28T20:15:04Z


 theorem exercise_4_5_17 {G : Type*} [fintype G] [group G] 
  (hG : card G = 105) : 
  nonempty(sylow 5 G) ∧ nonempty(sylow 7 G) :=


Both exercises require the Sylow subgroups to be normal, which is omitted in both formalizations.

alreadydone · 2023-05-28T20:17:31Z

 theorem exercise_3_1_22b {G : Type*} [group G] (I : Type*)
  (H : I → subgroup G) (hH : ∀ i : I, subgroup.normal (H i)) : 
  subgroup.normal (⨅ (i : I), H i):=


This should probably be added to mathlib ...

alreadydone · 2023-05-28T20:20:15Z

  [module F V] (v : V) (a : F): a • v = 0 ↔ a = 0 ∨ v = 0 :=
-sorry
+begin
+  simp [smul_eq_mul],


smul_eq_mul isn't actually used, I guess.

Yep, smul_eq_mul is indeed redundant here, but that's what the prover generated.

alreadydone · 2023-05-28T20:29:23Z

 theorem exercise_2_1_27 {G : Type*} [group G] 
  [fintype G] : ∃ (m : ℕ), ∀ (a : G), a ^ m = 1 :=


This exercise states "integer m > 0" too, but fintype.card G does satisfy the condition.

alreadydone · 2023-05-28T20:56:24Z

 theorem exercise_2018_a5 (f : ℝ → ℝ) (hf : cont_diff ℝ ⊤ f)
  (hf0 : f 0 = 0) (hf1 : f 1 = 1) (hf2 : ∀ x, f x ≥ 0) :
  ∃ (n : ℕ) (x : ℝ), iterated_deriv n f x = 0 := 
-sorry 
+begin
+  use (1/2),
+  use 0,
+  norm_num [hf0],
+end 


How could there be such an easy Putnam problem? Turns out the statement should say iterated_deriv n f x < 0, see https://kskedlaya.org/putnam-archive/2018.pdf

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

zhangir-azerbayev · 2023-05-28T22:08:19Z

Thank you for the corrections @alreadydone ! I've added commits that fix 6 wrong formalization and improve two formalizations.

@yangky11 It would be great if you could rerun your model on the statements that were modified.

I still would like to avoid having solutions to the benchmark on Github. I still would suggest adding a reference_formal_proof column to the huggingface dataset.

zhangir-azerbayev

Rerun model on modified statements.
Delete solutions from Github and move to huggingface.

yangky11 · 2023-05-31T06:11:51Z

Hi Zhangir and Junyan,

Thank you for your feedback on these proofs! That's really helpful, because, TBH, I cannot make sense of most of these theorems/proofs. I agree with Zhangir's worry about data contamination and potentially moving all proofs to another place. Do we know Hugging Face is not included in the training data of LLMs? Also, if all proofs are removed from the repo, we need a convenient way to track which theorems have proofs (maybe using comments next to sorry?). In any case, I just wanted to share the proofs, and it's totally up to you what you want to do with them.

It's quite surprising to me many of these proofs uncover issues of the original formalization. Now I'm a bit short of compute due to an incoming deadline, but I'm happy to run the prover on the updated proofs later.

yangky11 · 2023-06-08T17:05:41Z

Hi,

I have finished re-running a new version of the model. It proved 1 out of the 7 modified theorems (f63ea51). In addition, it also proved 10 theorems that weren't in the first batch (5854981, 19b1112). @alreadydone It would be great if you can take a look and see if any of them has incorrect theorem statement. Thank you!

alreadydone · 2023-06-09T04:45:17Z

Thanks! There are some nice proofs, but I also spotted some problems in formalization, which @zhangir-azerbayev can take a look at 19b1112. I also find strange numberings inconsistent with Pugh's book, see 060d4b1#r117194793

eric-wieser · 2023-06-09T09:20:29Z

I already regret hosting any part of this benchmark on Github

Can you elaborate on why?

BartoszPiotrowski · 2023-06-09T10:03:08Z

I already regret hosting any part of this benchmark on Github

Can you elaborate on why?

Zhangir may elaborate more, but the issue simply is that the benchmark is meant for evaluating LLMs, and because they are typically pretrained on multiple internet resources -- including Github -- it means that these models may memorize the examples from the benchmark. Then good performance achieved on the tasks based on the benchmark cannot be fully attributed to generalization achieved by the model but at least partially to memorization.

zhangir-azerbayev · 2023-06-09T15:22:54Z

Thanks @yangky11 for the proofs and @alreadydone for catching errors. Here's my plan for how to proceed with this PR.

Fix all the remaining incorrect formalizations identified by @alreadydone
Delete machine-generated solutions from this PR. Instead, I will add a new dict-valued column to the huggingface dataset titled "machine-solutions", whose values will have scheme {system-name: formal-proof}. This way we can keep track of machine solutions from multiple models without risk training set contamination (I expect people will have the good sense to not download huggingface when training their models).

yangky11 · 2023-06-09T17:38:40Z

@alreadydone Thank you for checking the proofs! @zhangir-azerbayev That sounds good to me! It would also be great to keep track of which theorems have proofs in the comments in this repo.

Our system name is ReProver. We're wrapping up the project and will release the paper and code soon.

alreadydone

In response to an email from @yangky11 I'm adding more comments.

alreadydone · 2023-06-15T14:43:01Z

 theorem exercise_11_2_13 (a b : ℤ) :
  (of_int a : gaussian_int) ∣ of_int b → a ∣ b :=
-sorry
+begin
+  contrapose, 
+  simp,
+end


squeeze_simp gives simp only [of_int_eq_coe, coe_int_dvd_coe_int, imp_self] but exact (coe_int_dvd_coe_int a b).1 is sufficient.

alreadydone · 2023-06-15T16:15:39Z

+  rintros ⟨a⟩ ⟨b⟩,
+  exact congr_arg coe (mul_comm a b)


exact mul_comm works.

alreadydone · 2023-06-15T16:21:53Z

+  rw infi,
+  rw ←set.image_univ,
+  rw Inf_image,
+  simp [hH],
+  haveI := λ i, (H i).normal,
+  split,
+  intros x hx g, 
+  rw subgroup.mem_infi at hx ⊢,
+  intro i,
+  apply (hH i).conj_mem _ (hx i),


We can produce a shorter proof manually, but it's certainly nice to be able to automate this.

Suggested change

rw infi,

rw ←set.image_univ,

rw Inf_image,

simp [hH],

haveI := λ i, (H i).normal,

split,

intros x hx g,

rw subgroup.mem_infi at hx ⊢,

intro i,

apply (hH i).conj_mem _ (hx i),

split,

simp_rw subgroup.mem_infi,

exact λ x hx g i, (hH i).conj_mem _ (hx i) _,

alreadydone · 2023-06-15T20:11:33Z

+  cases sq_eq_one_iff.1 hx with h h,
+  exacts [or.inl h, or.inr h],


Suggested change

cases sq_eq_one_iff.1 hx with h h,

exacts [or.inl h, or.inr h],

exact sq_eq_one_iff.1 hx

alreadydone · 2023-06-15T20:18:19Z

  is_open_map π₁ ∧ is_open_map π₂ :=
-sorry
+begin
+  simp [is_open_map_iff_nhds_le, h₁, h₂],


An occasion where appropriate lemmas aren't used but rather the proof is adapted; the following proof, albeit longer, would be preferred in mathlib for performance reasons.

Suggested change

simp [is_open_map_iff_nhds_le, h₁, h₂],

rw [h₁, h₂], exact ⟨is_open_map_fst, is_open_map_snd⟩,

alreadydone · 2023-06-15T20:21:39Z

+  rw set.diff_eq,
+  use hU.inter hA.is_open_compl,
+  rw set.diff_eq,
+  exact hA.inter hU.is_closed_compl,


Again, lemma not used but proof got adapted:

Suggested change

rw set.diff_eq,

use hU.inter hA.is_open_compl,

rw set.diff_eq,

exact hA.inter hU.is_closed_compl,

exact ⟨hU.sdiff hA, hA.sdiff hU⟩

alreadydone · 2023-06-15T20:24:20Z

  continuous (λ x, min (f x) (g x)) :=
-sorry
+begin
+  simpa only [min_def] using hf.min hg,


The simp only part may have been copied from https://github.com/leanprover-community/mathlib/blob/bf9bbbcf0c1c1ead18280b0d010e417b10abb1b6/src/topology/order/basic.lean#L562

Suggested change

simpa only [min_def] using hf.min hg,

exact hf.min hg

alreadydone · 2023-06-15T20:30:59Z

+  rw is_open_iff_nhds,
+  simp [cluster_pt],
+  simp [filter.inf_principal_eq_bot],


It took me several minutes to come up with the proof

Suggested change

rw is_open_iff_nhds,

simp [cluster_pt],

simp [filter.inf_principal_eq_bot],

simp_rw [is_open_iff_eventually, cluster_pt_principal_iff_frequently, not_frequently, not_mem_compl_iff],

so it's great that it can be automated. This proof can be condensed to

Suggested change

rw is_open_iff_nhds,

simp [cluster_pt],

simp [filter.inf_principal_eq_bot],

simp [is_open_iff_nhds, cluster_pt, filter.inf_principal_eq_bot],

to avoid a non-terminal simp.

alreadydone · 2023-06-16T05:19:16Z

+  rw [norm_add_sq_real, norm_sub_pow_two_real],
+  ring,


This proof could directly use parallelogram_law_with_norm rather than "re-proving" it, but that requires specifying an implicit argument with @. I wonder whether the model tried to use it initially but failed. It's nice that it figured out it could use lemmas that specialize to real inner product spaces.

Suggested change

rw [norm_add_sq_real, norm_sub_pow_two_real],

ring,

simp_rw [sq, @parallelogram_law_with_norm ℝ, mul_add],

alreadydone · 2023-06-16T05:39:51Z

+  cases eq_or_ne x 1,
+  all_goals { simp [h] },
+  apply order_of_eq_prime,
+  exacts [hx, h],


This proof is interesting as it takes a different approach than I would.

Suggested change

cases eq_or_ne x 1,

all_goals { simp [h] },

apply order_of_eq_prime,

exacts [hx, h],

exact (dvd_prime $ by norm_num).1 (order_of_dvd_of_pow_eq_one hx),

alreadydone · 2023-07-14T15:31:09Z

Personally, I'd like to see techniques like reflection, self-consistency, and refinement/debate/critique etc. be used together with autoformalization to automatically catch dubious formalizations and generate reasoning traces / CoT (ToT?) data that could be used to fine-tune the model.

Some Amazon guys did self-consistency for autoformalization: https://twitter.com/johnjnay/status/1679687620228530177 (Isabelle MiniF2F, not Lean though).

Add machine-generated proofs.

8eff21d

alreadydone reviewed May 28, 2023

View reviewed changes

Add space before * symbol

aa2dbf8

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

zhangir-azerbayev reviewed May 28, 2023

View reviewed changes

Comment thread benchmark/benchmark_to_publish/formal/Herstein.lean Outdated

zhangir-azerbayev added 2 commits May 28, 2023 17:44

fix Herstein 2_1_26

34e8d4a

remove 2_1_26 proof

eb57016

zhangir-azerbayev reviewed May 28, 2023

View reviewed changes

Comment thread benchmark/benchmark_to_publish/formal/Dummit-Foote.lean Outdated

zhangir-azerbayev and others added 7 commits May 28, 2023 17:50

Fix 4_5_17

cbfc22a

Fix 4_5_16 and 4_5_17

a2e5cd4

remove extraneous hypothesis

dc01d01

Fix Herstein 2_1_27

cdbb1ca

Improve formalization of 4_2_9

2ec74e8

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Fix Putnam 2018_a5

548e6b4

Update benchmark/benchmark_to_publish/formal/Putnam.lean

988af37

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

zhangir-azerbayev requested changes May 28, 2023

View reviewed changes

Kaiyu Yang added 6 commits June 7, 2023 10:28

Add additional machine-generated proofs

19b1112

Three more proofs found by retrieval

5854981

Merge branch 'zhangir-azerbayev:main' into main

b1104fb

Merge branch 'main' of https://github.com/yangky11/ProofNet into main

8366a44

Remove invalid proofs

3cc36eb

re-run the prover on fixed theorems

f63ea51

yangky11 changed the title ~~26 New Proofs Generated by Machines~~ New Proofs Generated by Machines Jun 8, 2023

alreadydone reviewed Jun 16, 2023

View reviewed changes

		theorem exercise_7_1_12 {F : Type*} [field F] {K : subring F}
		(hK : (1 : F) ∈ K) : is_domain K :=

		theorem exercise_2_1_27 {G : Type*} [group G]
		[fintype G] : ∃ (m : ℕ), ∀ (a : G), a ^ m = 1 :=

		cases sq_eq_one_iff.1 hx with h h,
		exacts [or.inl h, or.inr h],

	cases sq_eq_one_iff.1 hx with h h,
	exacts [or.inl h, or.inr h],
	exact sq_eq_one_iff.1 hx

	simp [is_open_map_iff_nhds_le, h₁, h₂],
	rw [h₁, h₂], exact ⟨is_open_map_fst, is_open_map_snd⟩,

	rw [norm_add_sq_real, norm_sub_pow_two_real],
	ring,
	simp_rw [sq, @parallelogram_law_with_norm ℝ, mul_add],

Conversation

yangky11 commented May 28, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zhangir-azerbayev commented May 28, 2023

Uh oh!

alreadydone left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhangir-azerbayev commented May 28, 2023

Uh oh!

zhangir-azerbayev left a comment

Choose a reason for hiding this comment

Uh oh!

yangky11 commented May 31, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

yangky11 commented Jun 8, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

alreadydone commented Jun 9, 2023

Uh oh!

eric-wieser commented Jun 9, 2023

Uh oh!

BartoszPiotrowski commented Jun 9, 2023

Uh oh!

zhangir-azerbayev commented Jun 9, 2023

Uh oh!

yangky11 commented Jun 9, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone commented Jul 14, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

yangky11 commented May 28, 2023 •

edited

Loading

alreadydone left a comment •

edited

Loading

yangky11 commented May 31, 2023 •

edited

Loading

yangky11 commented Jun 8, 2023 •

edited

Loading

yangky11 commented Jun 9, 2023 •

edited

Loading

alreadydone commented Jul 14, 2023 •

edited

Loading