Higher-Order Theorem Proving on Complex corpus (val)
38.9Proof SuccessLoop tactic dependent
Evaluation results
| Method | Links | |
|---|---|---|
| Loop tactic dependentTraining=Reinforcement Learning, Argument selection=Tactic dependent2019.04 | 38.9 | |
| Trained on loop outputTraining=Supervised on reinforcement learning loop output2019.04 | 36.8 | |
| LoopTraining=Reinforcement Learning, Argument selection=Tactic independent2019.04 | 36.3 | |
| Deeper WaveNetTraining=Supervised on human proofs, Blocks=4, Layers per block=52019.04 | 32.65 | |
| WaveNetTraining=Supervised on human proofs, Filters=128, Blocks=22019.04 | 31.72 | |
| Wider WaveNetTraining=Supervised on human proofs, Filters=2562019.04 | 27.6 | |
| ASM_MESON_TAC + argument selectionDescription=Baseline prover with argument list predicted by WaveNet2019.04 | 9.2 | |
| ASM_MESON_TACDescription=HOL Light built-in first order theorem prover baseline2019.04 | 6.1 |