List your company
ResearchFormerly WizWand

Lemma Discovery on Octonions

84.9Success RateCombined
20.31637.08353.8570.617Apr 7, 2025
Updated 5mo ago

Evaluation results

MethodLinks
CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0484.9
LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0483.1
CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0479.7
CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0479.4
LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0478.9
LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0476.6
LEMMANAID CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0476
LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0475.7
CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0470.9
CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0468.6
LEMMANAID (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0468
LEMMANAID CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0467.7
LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0467.4
LEMMANAID (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0467.1
LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0466.9
Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0465.7
LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0465.1
CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0464
LEMMANAID CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0462.6
Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0462.3
LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0461.4
LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0460.6
LEMMANAID (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0459.7
Neural CombinedBackbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0459.4
Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0459.1
LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0458.3
LEMMANAID (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0457.4
LEMMANAID (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0457.4
LEMMANAID (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0456
LEMMANAID (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0454.6
Neural CombinedBackbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0453.1
Neural (types + defs)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0453.1
Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL+AFP-train2025.0453.1
Neural (types)Backbone=DeepSeek-coder-6.7B, Training Set=HOL-train2025.0451.4
Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL-train2025.0448.6
Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0448
Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0446
Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL+AFP-train2025.0445.1
Neural CombinedBackbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0445.1
Neural (types)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0442.9
Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0442.3
Neural (defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0441.4
Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL-train2025.0440.6
Neural (types + defs)Backbone=DeepSeek-coder-1.3B, Training Set=HOL-train2025.0434
Neural (types)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0432.6
Neural (types + defs)Backbone=Llama-3.2-1B, Training Set=HOL+AFP-train2025.0432.3
QuickSpecType=Symbolic tool2025.0422.8