Theorem Proving (Substitution Network) on set.mm (val)
0.6847ProbMetaGen-IL
Evaluation Results
| Method | Links | ||
|---|---|---|---|
| MetaGen-ILHuman proofs=21786 (100%), Synthetic proofs=10M, Model=SUBSTITUTION2020.02 | 0.6847 | 83.9 | |
| MetaGen-RandHuman proofs=21786 (100%), Synthetic proofs=10M, Model=SUBSTITUTION2020.02 | 0.6439 | 81.85 | |
| SUBSTITUTIONHuman proofs=21786 (100%), Synthetic proofs=0, Generator=-2020.02 | 0.6142 | 81.57 | |
| SUBSTITUTIONHuman proofs=4358 (20%), Synthetic proofs=0, Generator=-2020.02 | 0.3765 | 67.07 | |
| MetaGen-ILHuman proofs=2179 (10%), Synthetic proofs=1M, Model=SUBSTITUTION2020.02 | 0.371 | 66.56 | |
| MetaGen-RandHuman proofs=2179 (10%), Synthetic proofs=1M, Model=SUBSTITUTION2020.02 | 0.3203 | 61.78 | |
| SUBSTITUTIONHuman proofs=2179 (10%), Synthetic proofs=0, Generator=-2020.02 | 0.2738 | 58.91 | |
| MetaGen-RL-AdvHuman proofs=0, Synthetic proofs=300K, Model=SUBSTITUTION2020.02 | 0.0186 | 31.38 | |
| MetaGen-RL-LMHuman proofs=0, Synthetic proofs=300K, Model=SUBSTITUTION2020.02 | 0.0181 | 24.33 | |
| MetaGen-RandHuman proofs=0, Synthetic proofs=300K, Model=SUBSTITUTION2020.02 | 0.0103 | 29.68 | |
| LANGUAGE MODELHuman proofs=0, Synthetic proofs=0, Generator=-2020.02 | 0.0032 | 9.06 | |
| SUBSTITUTIONHuman proofs=0, Synthetic proofs=0, Generator=-2020.02 | 0.0008 | 0.01 |