Hacker News new | ask | show | jobs
by fsndz 693 days ago
What's a real-life use case of theorem proving ? I really want to learn more about that but it always feel like an abstract thing that people do because they like solving puzzles. Does it help in solving the reliability challenge of current LLMs (https://www.lycee.ai/blog/ai-reliability-challenge) ?
4 comments
boroboro4 693 days ago
It does, but not necessary with LLMs, see https://news.ycombinator.com/item?id=41069829 for example - this is mixing Lean with neural network to automatically proof theorems.
link
umutisik 693 days ago
Real life use cases for theorem proving I am aware of: - Formal verification of implementations for applications that require extreme security and reliability. (banking, aerospace, ...) - Automated theorem proving would increase the pace of theoretical work. In some cases, that helps guide useful work. There are better examples, but a simple one: nobody is looking for faster (worst-case) sorting algorithms because there is a proven theoretical limit. Don't believe in theory, but don't be without theory! It definitely won't hurt if theory-building is cheaper and faster.

Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.

link
summerlight 692 days ago
When you want near 100% confidence on your design, you're gonna need formal method or something similar. Usually this is meant for critical, complex infrastructures and AWS has been one of such organization. https://www.amazon.science/publications/how-amazon-web-servi...

This can be applied on something like: Is your extension on distributed system protocol (like Paxos) correct? Does my novel security system hold certain properties? etc etc...

link
agentultra 693 days ago
Sel4 microkernel, compcert C compiler, https://bedrocksystems.com/, AWS and Azure both use model checking, https://hackage.haskell.org/package/containers-verified

... basically when you need to be sure certain properties of your system hold.

You can verify only the critical parts, as in a data structure or algorithm, or you can verify higher-level parts of a system. All you're doing with math is thinking (out loud) and writing a proof is constructing a convincing argument. If you need to be certain that a thread doesn't leak addresses in shared memory to other threads then you ought to take the time to think through how you're going to achieve that and prove that your solution works.

link