Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> 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.



Verification 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.


"just running it" is an enormously absurd simplification


If you can do better please go ahead?


There'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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: