Lemma Discovery on Octonions
84.9Success RateCombined
Evaluation Results
| Method | Links | |
|---|---|---|
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 84.9 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 83.1 | |
| CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 79.7 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 79.4 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 78.9 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 76.6 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 76 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 75.7 | |
| CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 70.9 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 68.6 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 68 | |
| LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 67.7 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 67.4 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 67.1 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 66.9 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 65.7 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 65.1 | |
| CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 64 | |
| LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 62.6 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 62.3 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 61.4 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 60.6 | |
| LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 59.7 | |
| Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 59.4 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 59.1 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 58.3 | |
| LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 57.4 | |
| LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 57.4 | |
| LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 56 | |
| LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 54.6 | |
| Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 53.1 | |
| Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 53.1 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.04 | 53.1 | |
| Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.04 | 51.4 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 48.6 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 48 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 46 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.04 | 45.1 | |
| Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 45.1 | |
| Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 42.9 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 42.3 | |
| Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 41.4 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.04 | 40.6 | |
| Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.04 | 34 | |
| Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 32.6 | |
| Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.04 | 32.3 | |
| QuickSpecType=Symbolic tool2025.04 | 22.8 |