Bruno Gavranović

I'm building neural networks that generate provably correct code, and the software infrastructure for training them.

Recently experimenting with TensorType: https://github.com/bgavran/TensorType

Last Notes

2026-07-06 08:40:55 GMT

- reply

@nprofile…4hp5 Yes, the parallels are stark indeed.
My favourite is this one:
https://mathstodon.xyz/@bgavran/114054413104698446

2026-04-20 22:16:02 GMT

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.
https://media.mathstodon.xyz/media_attachments/files/116/439/282/088/125/203/original/c0911f961b71aadb.png

2026-01-28 13:07:55 GMT

- reply

@nprofile…97ud Thanks for sharing this, I wasn't aware of this paper.

2026-01-27 21:04:51 GMT

- reply

@nprofile…97ud I see. I'm uneasy with making such claims about isolated objects, but I'll need to process this a bit more before being able to say mathematically why.
In general, this seems to touch upon a question I asked at some earlier point here: https://mathstodon.xyz/@bgavran/115482491243636752

2026-01-27 16:30:15 GMT

- reply

@nprofile…97ud I think there is some care that needs to be taken when upgrading the "removing element of a set" story to "removing an object of a category" one.
For instance, if there was another object `q` isomorphic to `p0` we removed, we'd end up with an equivalent category. So you likely want to remove the entire isomorphism class, but then I believe you run into further problems.
This thesis on Symmetric Containers (Section 2.3) goes into some detail: https://staff.math.su.se/gylterud/thesis_gylterud.pdf

2025-11-10 12:11:44 GMT

- reply

@nprofile…p3nn @nprofile…4x5t It did - the Appendix B of my thesis contains an intro and relevant constuctions of locally graded (and indexed) categories, and unpacks how one obtains Para as a change of base along the category of elements
https://arxiv.org/abs/2403.13001

2025-04-20 19:07:40 GMT

She said yes!!!! 💍
There are moments I feel like the luckiest man on Earth - now is one of them. @nprofile…f2xj
https://media.mathstodon.xyz/media_attachments/files/114/371/826/591/694/566/original/a1230fc04554847d.jpg
https://media.mathstodon.xyz/media_attachments/files/114/371/826/739/053/919/original/003027344d56fcf9.jpg

2025-02-23 18:06:01 GMT

- reply

@nprofile…fa4k Both alchemy and deep learning:
* operated without an understanding of fundamental principles of what they were studying
* made many experimental advances, often by accident
* lacked any predictive power
* sought to create mystical machinations
* were not reliable methods of producing outputs
Makes me wonder what the chemistry of deep learning is.

2025-02-23 18:02:44 GMT

- reply

@nprofile…fa4k Indeed, I found this because I'm trying to establish a clearer relationship between alchemy then and deep learning today.

2025-02-23 17:37:11 GMT

Fun fact I just learned: gunpowder was created by alchemists as a byproduct of trying to create the elixir of life.
https://en.wikipedia.org/wiki/Gunpowder

2024-06-24 12:58:13 GMT

It's well known that we can freely cocomplete or complete a category, i.e. add all colimits and limits via Yoneda embedding or its opposite.
Can we freely add (cartesian) closed structure to a category?

2024-03-14 01:57:40 GMT

My PhD Thesis is now available to read!
It presents a mathematical foundation for neural networks that is end-to-end, uniform, and prescriptive.
I'm incredibly excited about it.
You can find it at https://brunogavranovic.com/assets/FundamentalComponentsOfDeepLearning.pdf
and summarised at the following blog post
https://brunogavranovic.com/posts/2024-03-13-my-thesis-is-out.html
https://media.mathstodon.xyz/media_attachments/files/112/091/558/963/761/088/original/72c0a84b7b7a4ef8.png

2023-10-07 20:31:15 GMT

- reply

@npub1knz…c73p @npub1vsd…cfz9 You might like this description