Lemma Discovery on HOL (test)
58.6Success RateCombined
Evaluation Results
| Method | Links | |
|---|---|---|
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 58.6 | |
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 57.2 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 55.1 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 53.3 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 53.1 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 52.2 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 50.2 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 49.8 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 48 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 46.8 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 46.5 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 44.5 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 44.1 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 43.3 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 42.9 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 42.6 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 42.3 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 41.8 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 41.2 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 39.5 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 39.4 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 39.3 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 38.6 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 38.5 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 38.5 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 37.6 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 35.7 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 35.6 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 35 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 34.1 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 33.4 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 33.2 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 31.7 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 30.9 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 30.5 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 30.5 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 30.1 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 29.7 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 28.9 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 28.6 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 26.1 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 24.7 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 23.1 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 22.8 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 19.2 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 17.7 |