3 ms·

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 li

by fsndz 2y 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 https://www.lycee.ai/blog/ai-reliability-challenge) ?

boroboro4 2y ago
It does, but not necessary with LLMs, see https://news.ycombinator.com/item?id=41069829 https://news.ycombinator.com/item?id=41069829 for example - this is mixing Lean with neural network to automatically proof theorems.
agentultra 2y ago
Sel4 microkernel, compcert C compiler, https://bedrocksystems.com/ https://bedrocksystems.com/, AWS and Azure both use model checking, https://hackage.haskell.org/package/containers-verified 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.
umutisik 2y 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.
summerlight 2y 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-services-uses-formal-methods 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...

by fsndz 2y ago

boroboro4 2y ago

It does, but not necessary with LLMs, see https://news.ycombinator.com/item?id=41069829 https://news.ycombinator.com/item?id=41069829 for example - this is mixing Lean with neural network to automatically proof theorems.

agentultra 2y ago

Sel4 microkernel, compcert C compiler, https://bedrocksystems.com/ https://bedrocksystems.com/, AWS and Azure both use model checking, https://hackage.haskell.org/package/containers-verified 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.

umutisik 2y 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.

summerlight 2y 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-services-uses-formal-methods 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...