4 ms·
I imagine a system like this to be vastly more useful outside the realm of mathematics research. You don't need to be able to prove very hard problems to do us
by geysersam 2y ago
I imagine a system like this to be vastly more useful outside the realm of mathematics research.
You don't need to be able to prove very hard problems to do useful work. Proving just simple things is often enough. If I ask a language model to complete a task, organize some entries in a certain way, or schedule this or that, write a code that accomplishes X, the result is typically not trustworthy directly. But if the system is able to translate parts of the problem to logic and find a solution, that might make the system much more reliable.
- creata 2y agoBut for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.
- lanstin 2y agoAnd most applied maths doesn't seem to worry about proofs much. They have techniques that either work pretty well or blow up.
- optimalsolver 2y agoBridge collapses are a form of proof validation.
- geysersam 2y agoMy intuition is that a regular LLM is better att coming up with a correct task description from a fuzzy description than it is at actually solving tasks.
- humansareok1 2y agoThere's a lot of automated proof checkers out there. Presumably you would just run any solution from an AI through those.