search

runtimeverification / proof-generation

University of Illinois/NCSA Open Source License
10 stars 4 forks source link

Try the Metamath circuit on one of our benchmark proofs #56

Open fiedlr opened 1 year ago

fiedlr commented 1 year ago

By proof I mean the Metamath proof.

fiedlr commented 1 year ago

With @xc93 we plan to take benchmarks from https://github.com/oopsla23-paper-23/k-proof-generation , until the LLVM backend is ready to generate proof hints. Will send a link here to the benchmarks once some first ones are ready.

mariaKt commented 1 year ago

I have taken the input wff.mm, converted it to the format required for the proof generation step (.json, attached here), and attempted the local proof generation for the metamath circuit we generated earlier.

After running for ~6 min and consuming 80% of the available memory (total = 135G), the proof generator failed with

terminate called after throwing an instance of 'std::bad_alloc'
what():  std::bad_alloc

@Robertorosmaninho is getting a similar behavior, after using the same .json input file. We have posted a question to the Nil Foundation's Telegram channel.

Note that currently we are unable to publish our circuit and use the 'online' proof process, due to the circuit size (it seemed that there is a size limit to push the circuit to proof market in order to then request a proof on proof market).

metamath_input_wff_mm.json.txt