Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Types and Neural Networks

brunogavranovic.com

Post reply on HN
Print view View original

21–29 of 29 posts

Re: Types and Neural Networks

#21

Post by bgavran »

ogogmad wrote: post #14

"Even more, this coproduct can be thought of as an instance of a dependent pair indexed by a finite set" - I know what the individual terms mean, but I don't get what this is saying.

A coproduct in the category Set is a disjoint union of sets, i.e. A + B + C where A, B, C are sets.

We can think of this coproduct as involving two choices:

1) a choice of which component of the coproduct we're interested in (first, second, or third)

2) a choice of an element of that component

That is, `A + B + C` is isomorphic to `(i : Fin 3 * D i)` where `Fin 3` is a set with three elements, and `D : Fin 3 - > Type` and `D(0)=A`, `D(1)=B`, `D(2)=C`.

Then, the idea is: why index by a finite set? If you replace `Fin 3` by some arbitrary set, you start to be able to model a very general notion of a dependent type.

Re: Types and Neural Networks

#22

Post by toolslive »

jnpnj wrote: post #10
toolslive wrote: post #7

> This is what most programmers do. They type raw text into the editor; the compiler either processes it into structured data, or returns an error the programmer has to internalise before resubmitting. In the 1980s structural editors were quite popular (fe the basic editor in the ZX81). Using these, it is impossible for the programmer to create text that is not a valid program.

I never saw any structured editor on these machines, how did they operate ? grammar guided insertion ?

ha! I found an online simulator. Just try to do a

    10 print "hello world!"
to get a feel for it.

https://www.zx81stuff.org.uk/zx81/jtyone.html

Re: Types and Neural Networks

#23

Post by pron »

woolion wrote: post #20
pron wrote: post #13

The problem is that the search space is so large that correcting errors via guardrails is only effective if the original error rate is low (how many Integer -> Integer functions are there? There's ~1 way to get it right and ~∞ ways to get it wrong). Sure, we can help the easy cases, but that's because they're easy to begin with. In general, we know (or at least assume) that being able to check a solution tractably do…

>As Philippe Schnoebelen discovered in 2002 [1], languages cannot reduce the difficulty of program construction or comprehension. From a model-checking point of view. This is about taking a proof-theoretic approach... Your last paragraph is also quite wrong: a machine learning could very well easily learn and solve an NP-complete problem, because this property does not say anything about average case complexity (and…

> From a model-checking point of view. This is about taking a proof-theoretic approach...

No. In complexity theory we deal with problems, and the model-checking problem is that of determining whether a program satisfies some property or not. If your logic is sound, you can certainly use an algorithm based on the logic's deductive theory (which could be type theory, but that's an unimportant detail) to decide the problem, but that can have no impact whatsoever on the complexity of the problem. The result applies to all decision procedures, be they model-theoretic or deductive (logic-theoretic).

> Your last paragraph is also quite wrong: a machine learning could very well easily learn and solve an NP-complete problem, because this property does not say anything about average case complexity

No. First, it's unclear what "average complexity" means here, but for any reasonable definition, the "average complexity" of NP-hard problems is not known to be tractable. Second, complexity theory approaches this issue (of "some instances may be easier") using parameterised complexity [1], and I'm afraid that the results for the model-checking problem - which, again, is the inherent difficulty of knowing what a program does regardless of how you do it - are not very good. I mentioned such a result in an old blog post of mine here [2]. (Parameterised complexity is more applicable than probabilistic complexity here because even if there were some reasonable distribution of random instances, it's probably not the distribution we'd care about.)

There is no escape from complexity limits, and the best we hope for is to find out that problems we're interested in have actually been easier than we thought all along. Of course, some people believe that the programs people actually write are somehow in a tractable complexity class that we've not been able to define - and maybe one day we'll discover that that's the case - but what we've seen so far suggests it isn't: If programs that people write are somehow easier to analyse, then we'd expect to see the size of programs we can soundly analyse grow at the same pace as the size of programs people write, and nothing can be further from what we've observed. The size of programs that can be "proven correct" (especially using deductive methods!) has remained largely the same for decades, while the size of programs people write has grown considerably over that period of time.

[1]: https://en.wikipedia.org/wiki/Parameterized_complexity

[2]: https://pron.github.io/posts/correctness-and-complexity#corr...

Re: Types and Neural Networks

#24

Post by bgavran »

aesthesia wrote: post #16

I'm not totally convinced by this: > It might appear that this is an argument against scale, and the Bitter Lesson. That is not the case. I see this as a move that lets scale do its work on the right object. As with chess, where encoding the game rules into training produces a leap that no amount of inference-time search can today match, the move here is to encode the programming language itself into the training, an…

Author here - thanks for engaging.

> One way to think of the bitter lesson as it applies to generative models is that ~all data carries some information about the structure of reality

Completely agree. It might have not come across, but what I'm pointing out in the post is that the data as it is currently encoded in the models is needlessly lossy. Tokens do not reveal all the information we have at our disposal. In natural language, that's fine, because it's quite loose in structure.

But if our domain is heavily structured (like modern programming languages are), why reveal only snippets of linearised syntax of that structure to the model? Why not reveal the full structure we have at our disposal?

> and architectures that let you train on more data are better because they learn better underlying world models.

By this argument, wouldn't we conclude that training on chess using the game structure wouldn't work either, since that'd be a model that uses less data?

Less data is the point, isn't it?

Re: Types and Neural Networks

#25

Post by bgavran »

Daffrin wrote: post #9

The connection between type systems and neural net structure is underexplored in practice. One thing I'd add: when you're dealing with multi-modal inputs in production — say, mixed structured and unstructured content — the type-safety problem compounds. You end up with implicit contracts at inference boundaries that are very hard to enforce. Has the author written anything on how this applies to transformer architect…

There's been some exciting work generalising transformers to data structures that aren't just pure arrays: https://glaive-research.org/2025/02/11/Generalized-Transform...

I've implemented these in Idris 2: https://github.com/bgavran/TensorType/blob/main/src/NN/Archi...

Re: Types and Neural Networks

#26

Post by bgavran »

woolion wrote: post #11
bgavran wrote: post #6

Earlier quoted context omitted.

Author here - thanks for engaging. On existing techniques - Type-Constrained Generation paper is discussed in the blog post (under Constrained Decoding), and I'd group typed holes in the same bucket. The problem with those methods is that they're inference time: they don't update the weights. In this case, constrained decoding prevents the model from saying certain things, without changing what the model wants to say…

Thank you for your reply. FTR, I find the subject very interesting and I hope there will be more work on this line of approach. >The problem with those methods is that they're inference time I agree, I just thought it was missing some prior art (not affiliated with these papers :-P) What is not clear to me at all is, is this the draft of a research idea? Or is there already some implementation coming in a later post?…

There is an existing implementation validating this idea, and the plan is to make it publicly available at some point.

> It seems to me that such an idea would be workable on a given language with a given type system, but it seems to me there would be a black magic step to train a model that would work in a language-agnostic manner.

That's correct. The blog post alludes to infrastructure building as a necessary component of making that happen for that exact reason. I.e. while it's "easy" to generate a dependent pair in this way, generating an entire dependently typed AST is much more difficult. On the positive side, this is more of a software engineering effort rather than a research one.

Re: Types and Neural Networks

#27

Post by woolion »

bgavran wrote: post #26
woolion wrote: post #11

Earlier quoted context omitted.

Thank you for your reply. FTR, I find the subject very interesting and I hope there will be more work on this line of approach. >The problem with those methods is that they're inference time I agree, I just thought it was missing some prior art (not affiliated with these papers :-P) What is not clear to me at all is, is this the draft of a research idea? Or is there already some implementation coming in a later post?…

There is an existing implementation validating this idea, and the plan is to make it publicly available at some point. > It seems to me that such an idea would be workable on a given language with a given type system, but it seems to me there would be a black magic step to train a model that would work in a language-agnostic manner. That's correct. The blog post alludes to infrastructure building as a necessary compo…

Ok, thank you for the info. Do you have any idea when at some point might be? I'd love to check it out.

Re: Types and Neural Networks

#28

Post by jnpnj »

toolslive wrote: post #22
jnpnj wrote: post #10

Earlier quoted context omitted.

I never saw any structured editor on these machines, how did they operate ? grammar guided insertion ?

ha! I found an online simulator. Just try to do a 10 print "hello world!" to get a feel for it. https://www.zx81stuff.org.uk/zx81/jtyone.html

A bit confusing but extremely enjoyable, thanks

Re: Types and Neural Networks

#29

Post by deskamess »

jnpnj wrote: post #17
deskamess wrote: post #12

Earlier quoted context omitted.

Not a technical answer but when we started up the system (zx 16k) we were in a prompt. We would add commands with line numbers. After each line number the list of possible commands were embossed on the keyboard and you would start with that (if, peek, poke, etc). What you could complete was limited by that. Edit: BASIC programming That was not a very good description so try this: https://www.usebox.net/jjm/notes/basi…

I see. So if IIUC, it's similar to programmable pocket calculators too, and it's very enjoyable to have a physical key per language construct.

Right. That's the gist of the 'curated/guided' command entry.
Post reply on HN