Comment by measurablefunc
3 days ago
Not really. If you find someone who claims that non-trivial properties of neural networks can be verified by some kind of formal system like Lean then you should post the link because that would be very impressive.
Trivially, all finite neural networks can be represented to arbitrary precision by implementing them with digital logic. All digital logic can be represented by computer programs, so at this point we can pull in the entire apparatus of abstract interpretation, program proving and so on.
Try it & see how that goes.
Nothing in this thread was about Lean.
Nothing you said responds to anything I said.
Rice's theorem (which you are clearly citing, but won't clearly mention, for some reason) has almost zero actual practical relevance to AI explainability.
You make low-quality and low-effort AI-denialism posts whenever you pattern match "all non-trivial semantic properties of programs are undecidable" to... anything you think matches the folk/common understanding of those terms, without considering how irrelevant these statements are to actual real-world applications and engineering.
You ask for links, but post nothing of substance and post no references or even mention relevant details for your own claims.
Stop responding to my comments & save yourself the time & keystrokes. It's better that way for everyone involved since you haven't addressed anything of substance in anything I have written & have opted for nonsensical psychoanalysis.
You haven't said anything of substance, because as I and other commenters here have pointed out, you clearly don't even understand Rice's theorem and why it isn't applicable here. You bring up formal verification with Lean on a thread and topic which is about model explainability. You should just stop posting entirely, you are polluting HN with irrelevant nonsense.
1 reply →