List your company
ResearchFormerly WizWand

Lemma Discovery on HOL (test)

58.6Success RateCombined
16.06427.10738.1549.193Apr 7, 2025
Updated 5mo ago

Evaluation results

MethodLinks
CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0458.6
CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0457.2
LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0455.1
CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0453.3
CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0453.1
LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0452.2
LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0450.2
LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0449.8
LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0448
Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0446.8
LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0446.5
LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0444.5
Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0444.1
LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0443.3
CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0442.9
Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0442.6
Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0442.3
LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0441.8
CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0441.2
LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0439.5
Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0439.4
LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0439.3
Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0438.6
Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0438.5
LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0438.5
LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0437.6
LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0435.7
LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0435.6
LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0435
LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0434.1
Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0433.4
LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0433.2
LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0431.7
Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0430.9
Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0430.5
Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0430.5
Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0430.1
Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0429.7
Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0428.9
LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0428.6
Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0426.1
Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0424.7
Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0423.1
Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0422.8
Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0419.2
Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0417.7