Michael Färber
Home Connection Provers Premise Selection Tactics Satallax
Premise selection statistics

This page contains statistics from experiments performed on Mizar, HOL Light, and Isabelle datasets, which are all included in our premise selection tool. Historically, in many premise selection papers “100-Precision” was called “Cov”, so “Cov” in our statistics actually refers to “100-Precision”.

Mizar

Samples Cov Prec Rec AUC Rank
combineMean/rforest:combineMean=Harmonic 1689 0.880 13.860 243.74 0.9568 51.98
combineMean/rforest:combineMean=Geometric 1689 0.880 13.866 244.41 0.9567 52.01
combineMean/rforest:combineMean=Maximum 1689 0.873 13.805 280.35 0.9492 57.97
combineMean/rforest:combineMean=Quadratic 1689 0.874 13.806 257.90 0.9534 54.41
combineMean/rforest:combineMean=Arithmetic 1689 0.875 13.815 249.73 0.9549 53.16
confidence/rforest:confidenceAlg=NaiveConfidence 1689 0.784 12.385 452.11 0.8841 104.17
giniFeats/rforest:giniFeats=4 1689 0.880 13.857 243.75 0.9565 52.07
giniFeats/rforest:giniFeats=12 1689 0.880 13.871 242.98 0.9563 52.11
giniFeats/rforest:giniFeats=8 1689 0.880 13.860 243.75 0.9564 52.08
giniFeats/rforest:giniFeats=6 1689 0.880 13.860 243.70 0.9565 52.07
giniFeats/rforest:giniFeats=2 1689 0.880 13.857 243.93 0.9565 52.09
giniFeats/rforest:giniFeats=16 1689 0.880 13.862 242.89 0.9562 52.13
manyTrees/rforest:nTrees=100:sampleFreq=50 1689 0.885 13.944 243.77 0.9585 50.84
nTsF/rforest:nTrees=6:sampleFreq=8 1689 0.880 13.864 243.84 0.9569 51.72
nTsF/rforest:nTrees=2:sampleFreq=6 1689 0.880 13.854 243.44 0.9564 52.11
nTsF/rforest:nTrees=16:sampleFreq=4 1689 0.880 13.882 250.16 0.9558 52.23
nTsF/rforest:nTrees=16:sampleFreq=16 1689 0.882 13.889 243.44 0.9575 51.42
nTsF/rforest:nTrees=32:sampleFreq=12 1689 0.884 13.932 244.66 0.9583 50.99
nTsF/rforest:nTrees=12:sampleFreq=12 1689 0.881 13.893 243.72 0.9576 51.45
nTsF/rforest:nTrees=4:sampleFreq=4 1689 0.880 13.870 244.83 0.9567 51.94
nTsF/rforest:nTrees=8:sampleFreq=8 1689 0.881 13.882 244.04 0.9571 51.65
nTsF/rforest:nTrees=32:sampleFreq=24 1689 0.884 13.925 243.98 0.9580 51.18
nTsF/rforest:nTrees=12:sampleFreq=24 1689 0.881 13.873 243.38 0.9574 51.59
nTsF/rforest:nTrees=2:sampleFreq=16 1689 0.880 13.861 243.70 0.9568 52.05
nTsF/rforest:nTrees=12:sampleFreq=8 1689 0.882 13.902 245.01 0.9575 51.46
nTsF/rforest:nTrees=12:sampleFreq=4 1689 0.882 13.906 246.62 0.9573 51.58
nTsF/rforest:nTrees=6:sampleFreq=1 1689 0.873 13.729 260.94 0.9503 55.24
nTsF/rforest:nTrees=8:sampleFreq=1 1689 0.864 13.604 270.21 0.9456 58.00
nTsF/rforest:nTrees=24:sampleFreq=8 1689 0.884 13.910 246.83 0.9575 51.28
nTsF/rforest:nTrees=4:sampleFreq=8 1689 0.880 13.848 243.66 0.9568 51.85
nTsF/rforest:nTrees=2:sampleFreq=24 1689 0.880 13.869 243.35 0.9567 51.97
nTsF/rforest:nTrees=6:sampleFreq=32 1689 0.880 13.858 243.25 0.9569 51.80
nTsF/rforest:nTrees=32:sampleFreq=4 1689 0.876 13.729 255.75 0.9529 53.90
nTsF/rforest:nTrees=12:sampleFreq=32 1689 0.881 13.860 243.15 0.9571 51.79
nTsF/rforest:nTrees=16:sampleFreq=6 1689 0.883 13.906 246.24 0.9575 51.42
nTsF/rforest:nTrees=16:sampleFreq=1 1689 0.843 13.142 290.95 0.9347 64.89
nTsF/rforest:nTrees=24:sampleFreq=1 1689 0.826 12.856 310.18 0.9262 71.07
nTsF/rforest:nTrees=16:sampleFreq=12 1689 0.883 13.926 243.77 0.9577 51.39
nTsF/rforest:nTrees=24:sampleFreq=24 1689 0.882 13.890 243.43 0.9577 51.28
nTsF/rforest:nTrees=16:sampleFreq=24 1689 0.882 13.887 243.39 0.9575 51.53
nTsF/rforest:nTrees=4:sampleFreq=24 1689 0.881 13.866 243.34 0.9570 51.87
nTsF/rforest:nTrees=8:sampleFreq=2 1689 0.879 13.853 253.37 0.9544 52.76
nTsF/rforest:nTrees=8:sampleFreq=4 1689 0.882 13.915 246.72 0.9568 51.83
nTsF/rforest:nTrees=4:sampleFreq=32 1689 0.880 13.862 243.56 0.9567 52.00
nTsF/rforest:nTrees=2:sampleFreq=2 1689 0.880 13.877 246.05 0.9560 52.23
nTsF/rforest:nTrees=32:sampleFreq=16 1689 0.884 13.928 244.46 0.9583 51.10
nTsF/rforest:nTrees=24:sampleFreq=6 1689 0.882 13.888 248.75 0.9569 51.83
nTsF/rforest:nTrees=16:sampleFreq=8 1689 0.883 13.913 245.51 0.9576 51.40
nTsF/rforest:nTrees=6:sampleFreq=4 1689 0.881 13.918 244.98 0.9570 51.81
nTsF/rforest:nTrees=12:sampleFreq=16 1689 0.882 13.892 243.39 0.9575 51.59
nTsF/rforest:nTrees=4:sampleFreq=1 1689 0.874 13.794 255.51 0.9518 53.94
nTsF/rforest:nTrees=16:sampleFreq=32 1689 0.882 13.874 243.35 0.9574 51.65
nTsF/rforest:nTrees=6:sampleFreq=24 1689 0.881 13.867 243.16 0.9571 51.80
nTsF/rforest:nTrees=4:sampleFreq=12 1689 0.880 13.870 243.89 0.9569 52.01
nTsF/rforest:nTrees=24:sampleFreq=2 1689 0.867 13.557 266.63 0.9468 57.57
nTsF/rforest:nTrees=4:sampleFreq=6 1689 0.879 13.854 244.01 0.9567 51.86
nTsF/rforest:nTrees=6:sampleFreq=2 1689 0.879 13.873 251.25 0.9548 52.64
nTsF/rforest:nTrees=16:sampleFreq=2 1689 0.873 13.723 261.36 0.9503 55.20
nTsF/rforest:nTrees=2:sampleFreq=32 1689 0.880 13.858 243.60 0.9568 51.93
nTsF/rforest:nTrees=12:sampleFreq=6 1689 0.883 13.903 245.93 0.9570 51.55
nTsF/rforest:nTrees=8:sampleFreq=6 1689 0.882 13.914 244.51 0.9573 51.55
nTsF/rforest:nTrees=24:sampleFreq=16 1689 0.884 13.924 243.99 0.9579 51.20
nTsF/rforest:nTrees=12:sampleFreq=2 1689 0.875 13.776 256.18 0.9529 53.96
nTsF/rforest:nTrees=32:sampleFreq=6 1689 0.882 13.859 249.63 0.9563 51.97
nTsF/rforest:nTrees=6:sampleFreq=12 1689 0.879 13.855 243.85 0.9567 51.92
nTsF/rforest:nTrees=2:sampleFreq=4 1689 0.880 13.864 244.15 0.9562 52.36
nTsF/rforest:nTrees=12:sampleFreq=1 1689 0.857 13.454 277.63 0.9414 60.63
nTsF/rforest:nTrees=32:sampleFreq=2 1689 0.856 13.361 275.41 0.9412 60.64
nTsF/rforest:nTrees=2:sampleFreq=8 1689 0.879 13.853 243.79 0.9565 52.15
nTsF/rforest:nTrees=8:sampleFreq=12 1689 0.881 13.882 243.99 0.9569 51.86
nTsF/rforest:nTrees=24:sampleFreq=32 1689 0.882 13.888 243.28 0.9576 51.47
nTsF/rforest:nTrees=32:sampleFreq=32 1689 0.883 13.893 243.63 0.9580 51.26
nTsF/rforest:nTrees=8:sampleFreq=24 1689 0.881 13.872 243.34 0.9570 51.81
nTsF/rforest:nTrees=4:sampleFreq=16 1689 0.880 13.857 243.73 0.9568 51.99
nTsF/rforest:nTrees=24:sampleFreq=4 1689 0.880 13.853 251.43 0.9551 52.75
nTsF/rforest:nTrees=6:sampleFreq=6 1689 0.881 13.880 244.43 0.9568 51.75
nTsF/rforest:nTrees=32:sampleFreq=1 1689 0.806 12.520 320.18 0.9176 76.74
nTsF/rforest:nTrees=2:sampleFreq=12 1689 0.880 13.871 244.13 0.9564 52.17
nTsF/rforest:nTrees=2:sampleFreq=1 1689 0.881 13.883 247.87 0.9556 52.23
nTsF/rforest:nTrees=4:sampleFreq=2 1689 0.880 13.870 247.78 0.9558 52.04
nTsF/rforest:nTrees=8:sampleFreq=32 1689 0.880 13.850 243.49 0.9569 51.91
nTsF/rforest:nTrees=32:sampleFreq=8 1689 0.884 13.910 248.26 0.9570 51.57
nTsF/rforest:nTrees=6:sampleFreq=16 1689 0.881 13.873 243.60 0.9571 51.83
nTsF/rforest:nTrees=8:sampleFreq=16 1689 0.881 13.876 243.58 0.9570 51.79
nTsF/rforest:nTrees=24:sampleFreq=12 1689 0.885 13.955 244.11 0.9583 50.96
pathScore/rforest:depthWeightAlg=Constant 1689 0.881 13.891 240.56 0.9581 51.08
pathScore/rforest:depthWeightAlg=Ascending 1689 0.880 13.858 242.32 0.9572 51.72
pathScore/rforest:depthWeightAlg=Inverse 1689 0.880 13.857 243.73 0.9568 51.99
pathScore/rforest:depthWeightAlg=Descending 1689 0.881 13.880 243.14 0.9566 51.66
predAlg/rforest:predAlg=Naive 1689 0.372 7.433 745.42 0.5900 367.23
predAlg/knn 1689 0.875 13.821 250.32 0.9539 53.57
predAlg/rforest:predAlg=KNN:tfidf=True 1689 0.880 13.857 243.73 0.9568 51.99
predAlg/rforest:predAlg=KNN:tfidf=False 1689 0.778 12.626 348.11 0.9140 88.57
randFeats/rforest:randFeats=32 1689 0.880 13.864 244.19 0.9565 52.09
sampleStrat/rforest:sampleFreq=2:sampleStrat=TreesDrawSamples 1689 0.656 10.570 588.59 0.7276 183.60
sampleStrat/rforest:sampleStrat=TreesDrawSamples 1689 0.880 13.860 244.00 0.9566 52.03
sampleStrat/rforest:sampleFreq=2:sampleStrat=SamplesDrawTrees 1689 0.880 13.871 247.81 0.9559 52.03
sampleStrat/rforest:sampleStrat=SamplesDrawTrees 1689 0.880 13.857 243.73 0.9568 51.99
SPQ/rforest:depthWeightAlg=Constant:minDepthWeight=0 1689 0.537 8.834 729.62 0.6086 352.56
treeDepth/rforest:maxTreeDepth=16 1689 0.880 13.857 243.76 0.9568 51.99
treeDepth/rforest:maxTreeDepth=32 1689 0.880 13.857 243.73 0.9568 51.99
treeDepth/rforest:maxTreeDepth=2 1689 0.879 13.850 245.71 0.9561 52.50
treeDepth/rforest:maxTreeDepth=12 1689 0.880 13.856 243.70 0.9568 51.99
treeDepth/rforest:maxTreeDepth=6 1689 0.880 13.861 244.19 0.9566 52.16
treeDepth/rforest:maxTreeDepth=4 1689 0.880 13.858 244.56 0.9564 52.29
treeDepth/rforest:maxTreeDepth=8 1689 0.880 13.861 244.01 0.9567 52.06
treeDepth/rforest:maxTreeDepth=24 1689 0.880 13.857 243.73 0.9568 51.99

HOL Light

Samples Cov Prec Rec AUC Rank
HLknn 1529 0.919 3.852 115.23 0.9565 39.47
HLrfnT24sF12ConstantScore 1529 0.929 3.883 100.28 0.9629 33.60

Isabelle

Samples Cov Prec Rec AUC Rank
Isabelleknn 1650 0.834 6.075 286.90 0.9236 82.93
IsabellerfnT24sF12ConstantScore 1650 0.843 6.118 272.58 0.9293 77.40