News for hackers. Stuff that matters.

A comment on Some notes on Rust, mutable aliasing and formal verification. Parent comment

Re:Some notes on Rust, mutable aliasing and formal verification by eru on Thursday May 16, 2024 @07:45AM (#40377185)
> (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property.

Don't basically all applications of any heuristic solver to NP problems have this property? (Including problems that are only in NP, because they are also already in P.)

[ Parent | on HN ]
Re:Some notes on Rust, mutable aliasing and formal verification by MaxBarraclough on Thursday May 16, 2024 @09:24AM (#40378140)
Yes, sure, I could have phrased that better. There are no doubt many possible applications of the idea. The recent headline-grabbing applications of machine learning tend not to be like this.
[ Parent | on HN ]
Re:Some notes on Rust, mutable aliasing and formal verification by eru on Friday May 17, 2024 @04:05AM (#40387560)
Yes, agreed.

Though even amongst the recent-headline-grabbing stuff there are some areas that you can improve at by the equivalent of AlphaGo's self-play. Basically, when you have a slow and expensive option to use a weaker version of your system to produce better decisions / smarter data, and then use those to train the system.

[ Parent | on HN ]