4 ms·
> Code and math are similar to chess/go, where verification is (reasonably) easy Verification for code would be a formal proof, and these are hard; with a few
by cesarb 1y ago
> Code and math are similar to chess/go, where verification is (reasonably) easy
Verification for code would be a formal proof, and these are hard; with a few exceptions like seL4, most code does not have any formal proof. Games like chess and go are much easier to verify. Math is in the middle; it also needs formal proofs, but most of math is doing these formal proofs themselves, and even then there are still unproven conjectures.
- Herring 1y agoVerification for code is just running it. Maybe "verification" was the wrong word. The model just needs a sense of code X leads to outcome Y for a large number of (high-quality) XY pairs, to learn how to navigate the space better, same as with games.
- krupan 1y ago"just running it" is an enormously absurd simplification
- Herring 1y agoIf you can do better please go ahead?
- sn9 1y agoThere's an entire field of formal verification that LLMs can take advantage of. You can incorporate proofs with Coq or Dafny or use model checkers or TLA+ to actually verify your code. This will be required for any software where correctness matters.