Post #1506825
2026-04-20 22:16 UTC
I just published a new blog post!
Types and Neural Networks
(https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html)
It's about what comes into view once dependent type systems become a part of neural network training.
Replies (2)
-
@bgavran@mathstodon.xyz 2026-04-20 22:28
This has been on my mind for a while, and its something we've been getting quite excited about at GLAIVE. It started as narrow question: > How can we train a network to generate a dependent pair in a way that is *correct-by-construction*? and it ended up morphing into a novel perspective on what it means to integrate dependent types into training.
-
@benediktpeterseim@mathstodon.xyz 2026-04-21 13:52
@bgavran@mathstodon.xyz “The system AlphaZero utilises the game structure during training and reaches superhuman ELO (>3400) with ~30x fewer parameters than GPT-4 (<60 million vs 1.8 trillion).” — I guess that’s supposed to be a “30.000x fewer”? (Which is quite immense.)