Post #2995266

2026-04-20 22:28 UTC

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.

Replies (1)

@bgavran@mathstodon.xyz 2026-04-20 22:42

For me, this answered a long-standing question about works like CHAD (https://arxiv.org/abs/2103.15776) or The Differentiable Curry (https://dimitriv.github.io/papers/hoad-workshop.pdf) which allow us to differentiate through structured objects such as (co)inductive types of function objects. I had always wondered: since we now have at our disposal such sophisticated maps which we can differentiate through (instead of just first-order programs), does this expand in any way the design space of neural networks? If our output is now a coinductive type, does this mean we can dynamically learn it from data? Perhaps surprisingly, the answer is no. While your output *can* be a coinductive type, using these methods requires you to statically fix the constructor choices, preventing the neural network from doing the learning itself. While this now feels "obvious", this distinction of "differentiating through a fixed program" versus "learning which program we generate" is one I've never seen acknowledged before

Open ##2995267