Synthetic dataset generation

Stream: Machine Learning for Theorem Proving

[Soonho Kong]

Hi All, I'm wondering if you can share ideas and/or existing prototypes on synthesizing diverse Lean datasets (theorems & proofs) across various mathematical domains, including number theory, algebra, and combinatorics. The goal would be to create a comprehensive dataset that could potentially serve educational purposes, such as automatically generating exercises for platforms like Lean Games, as well as training AI agents in these mathematical domains.

[Kevin Buzzard]

I would get humans to synthesize them. Presumably this isn't what you want to hear?

[Kim Morrison]

Without a very robust feedback loop between:

• generating statements
• deciding that they are valuable because they are both
  • true (via generating proofs) and
  • useful (via noticing that they help prove later things)

synthetic data in maths is really hard. I think people are working on such feedback loops, but there's not a lot public to point to.

[Abhishek Anand]

1. following AlphaGeometry, one could directly generate/sample in the valid-proof space and compute the theorem from the proof.
2. It is not obvious that the theorems need to be "useful". I dont think AlphaGeometry tried to select only useful theorems for training. The author said that most of the theorems in the synthetic dataset are uninteresting. It seems they did deduplicate the theorems.

The synthetic proof dataset generation phase of AlphaGeometry is discussed starting 21:00 in this video https://www.youtube.com/watch?v=eZbYSOpga2U

[Kim Morrison]

Yes, it is surprising that AlphaGeometry in the end could solve interesting problems, when so much of its training was "not useful" examples. But still, they were in a vastly smaller domain than just writing proofs.

[Huajian Xin]

(deleted)

[Notification Bot]

Huajian Xin has marked this topic as resolved.

[Notification Bot]

Huajian Xin has marked this topic as unresolved.

[Huajian Xin]

Hi! We submitted a new paper on arxiv and successfully achieved large-scale synthesis of formal proof data for Lean4. The trained model successfully proved 52% of theorems using the Lean4 language on the miniF2F benchmark. http://arxiv.org/abs/2405.14333

[Notification Bot]

26 messages were moved from this topic to #Machine Learning for Theorem Proving > DeepSeek-Prover by Eric Wieser.