Mmm yeah interesting, I agree $2600 and then more for inference is quite a
lot. I think your original plan might be quite a good one as if multiple
groups are going to scrape the web for training data then we might be able
to get into a bunch of different models.
This is an interesting conversation with chatGPT. Seems it already knows
quite a lot.
*Me: *
Tell me what you think this is
Metamath proof of pm5.74 in database set.mm
pm5.74 $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> ch )
) ) $= ... $.
PROOF:
1 biimp $p |- ( ( ps <-> ch ) -> ( ps -> ch ) )
[I pasted in the whole proof but omit it here for brevity]
*ChatGPT:*
This is a formal proof in the Metamath language for the statement pm5.74,
which asserts that the formula
((ph -> (ps <-> ch)) <-> ((ph -> ps) <-> (ph -> ch)))
is a theorem, where ph, ps, and ch are propositional variables.
The proof appears to be a sequence of logical deductions using various
rules of inference, including bi-implication introduction (biimp),
implication introduction (imim3i), bidirectional implication elimination
(impbid), and the modus ponens rule (pm). The proof involves manipulating
the logical connectives and truth tables of the involved propositions until
the desired statement is proven.
The proof is based on the set.mm database, which is a large collection of
mathematical theorems and their formal proofs in the Metamath language.
*Me: *
is this database part of your training data?
*ChatGPT:*
As an AI language model, I do not have access to information about the
specific training data used to train me. However, I am aware that the
set.mm database is a public database of formal mathematical proofs in the
Metamath language, and it is often used as a benchmark for automated
theorem proving systems. Some researchers have used the set.mm database as
part of their training data for developing automated theorem provers or
natural language understanding systems, but I cannot say for certain
whether it was used as part of my own training data.
*Me: *
Please take the following partial proof and continue it for another line
Metamath proof of axtgcgrrflx in database set.mm
axtrkg.p $e |- P = ( Base ` G ) $.
axtrkg.d $e |- .- = ( dist ` G ) $.
axtrkg.i $e |- I = ( Itv ` G ) $.
axtrkg.g $e |- ( ph -> G e. TarskiG ) $.
axtgcgrrflx.1 $e |- ( ph -> X e. P ) $.
axtgcgrrflx.2 $e |- ( ph -> Y e. P ) $.
axtgcgrrflx $p |- ( ph -> ( X .- Y ) = ( Y .- X ) ) $= ... $.
PROOF:
1 df-trkg $a |- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i {
f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p ,
y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y
e. ( x i z ) ) } ) } ) )
2 inss1 $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. (
Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p
\ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z
) ) } ) } ) ) C_ ( TarskiGC i^i TarskiGB )
3 inss1 $p |- ( TarskiGC i^i TarskiGB ) C_ TarskiGC
4 2,3 sstri $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [.
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. (
p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i
z ) ) } ) } ) ) C_ TarskiGC
5 1,4 eqsstri $p |- TarskiG C_ TarskiGC
*ChatGPT:*
6 1,5 eqtrans $p |- TarskiG = TarskiGC $
7 subst $e |- ( ( ph -> G e. TarskiGC ) -> ( ph -> G e. TarskiG ) ) $
8 hyp $e, ph |- ph $
9, 10 mp $e |- ( ph -> G e. TarskiG ) $
11 7, 9 mp $e |- ( ph -> G e. TarskiGC ) $
12 eqtrans $p |- ( ph -> G e. TarskiGC ) = ( ph -> G e. ( ( TarskiGC i^i
TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base f ) / p ]. [. ( Itv f ) / i
]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x
i y ) / x e. ( z i y ) / y e. ( x i z ) ) } ) } ) ) ) $
13 6, 11, 12 impbii $p |- ( ph -> ( X .- Y ) = ( Y .- X ) ) $
*Me:*
how many theorems are proven in the metamath database
*ChatGPT:*
As of the latest update to the Metamath database on January 24, 2022, there
are a total of 272,443 theorems that have been proven. However, it's worth
noting that this number may change as new theorems are added to the
database over time.
----------------
So yeah I haven't tried it on any partial proofs and then like tried to run
it in MMJ2 or something but that might be interesting to see if it can
already do any more steps. It already has the structure pretty well
organised.
It also gives a clue of when it scanned the database, though that number of
theorems is wildly wrong.
On Thursday, February 16, 2023 at 3:05:01 PM UTC David A. Wheeler wrote:
>
> > On Feb 14, 2023, at 1:46 PM, Jon P <[email protected]> wrote:
> >
> > I think that's a great idea David! Seems like very low downside and it
> would be interesting to see if language models could train on the datasets.
> >
> > There's already an option to Customise GPT3 with additional datasets so
> once this is ready it could be an interesting experiment to try.
> >
> > https://openai.com/blog/customized-gpt-3/
>
> Thanks so much for that link. So I looked into creating a
> specially-trained model
> to create metamath proofs. that page points to this pricing model for
> GPT-3:
> https://openai.com/api/pricing/#faq-token
>
> I did a quick estimate of training costs for the top GPT-3 model on
> all of set.mm. It comes out to about $2600.
> That's less than I expected, and that's easily affordable in a grant (you
> could train multiple times),
> but it's not an amount I have pocket change for :-(.
> Inference isn't expensive; trying to generate axtgcgrrflx is $0.15 (15
> cents).
> See below for how I created the quick estimate.
> We could do a subset of set.mm (e.g., skip mathboxes, etc.), though fewer
> training examples
> would typically produce less-good results.
>
> I can't possibly afford that myself. That said, there are alternatives.
> There are many other
> Generative Pre-trained Transformer (GPT) models that are less capable but
> also less expensive. My current personal computer is useless
> for ML training, but Kaggle.com provides a nice Jupyter notebook interface
> for AI/ML
> work that's free to use. Here are some pages that discuss using GPT-2 and
> Kaggle:
> https://www.kaggle.com/code/changyeop/how-to-fine-tune-gpt-2-for-beginners
>
> https://www.kaggle.com/code/nulldata/fine-tuning-gpt-2-to-generate-netlfix-descriptions/notebook
> https://www.kaggle.com/general/116387
>
> I had also been looking at adding definition checks to metamath-knife, and
> maybe trying to
> help this new JavaScript metamath proof assistant. Sigh, not enough time
> in the day :-).
>
> --- David A. Wheeler
>
>
>
> === Cost estimate ===
>
> Here's. cost estimate using https://openai.com/api/pricing/
>
> OpenAI's most powerful GPT-3 model is Davinci. Their charges are:
> * Fine-tuned training: $0.0300 / 1K tokens,
> * Usage: $0.1200 / 1K tokens.
>
> I did a quick estimate of tokens in the entirety of set.mm using:
> metamath 'set scroll continuous' 'set width 9999' 'read set.mm' 'show
> statement *' 'show proof * /lemmon /renumber' 'quit' | grep -v -- '-------'
> | wc
> That yielded 64218080 words. A token is about 4 characters or 0.75 words,
> so for a quick estimate, tokens = 64218080/0.75 = 85624107 tokens.
> Fine-tuned training of this entire set = (85624106/1000)*$0.03 = $2569.
>
> Theorem axtgcgrrflx : 942 words, tokens = 942/0.75 = 1256, cost =
> (1256/1000)*$0.12 = $0.15
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/c8ef9a81-0782-4d90-9ffc-60d89aba36ffn%40googlegroups.com.
