Lemma Discovery on AFP (test)
42.7Success RateCombined
Evaluation Results
| Method | Links | |
|---|---|---|
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 42.7 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 38.7 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 35.9 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 34.8 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 32.9 | |
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 32.1 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 31.6 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 30.4 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 29.4 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 28.6 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 28.5 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 28.2 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 27.9 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 27.4 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 27.2 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 26.4 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 26.3 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 25.2 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 25.1 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 23.7 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 23.5 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 22.6 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 22.5 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 21.1 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 20.3 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 19.7 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 19.7 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 19.3 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 19 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 18.6 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 17.8 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 17.7 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 17.7 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 15 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 15 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 13 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 12.9 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 12.9 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 12.2 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 11.9 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 11.1 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 8.8 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 7.8 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 7.3 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 6.2 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 6.2 |