4 ms·
To generate new, generally useful algorithms, we need a different type of "AI", i.e. one that combines learning and formal verification. Because algorithm desig
by timkam 5y ago
To generate new, generally useful algorithms, we need a different type of "AI", i.e. one that combines learning and formal verification. Because algorithm design is a cycle: come up with an algorithm, prove what it can or can't do, and repeat until you are happy with the formal properties. Software can help, but we can't automate the math, yet.
- dharmaturtle 5y ago> we can't automate the math, yet This exists: https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving
- bccdee 5y agoThis is moreso automation-assisted theorem proving. It takes a lot of human work to get a problem to the point where automation can be useful. It's like saying that calculators can solve complex math problems; it's true in a sense, but it's not not strictly true. We solve the complex math problems using calculators.
- sterlind 5y agoand there's already GPT-f [0], which is a GPT-based automated theorem prover for the Metamath language, which apparently submitted novel short proofs which were accepted into Metamath's archive. I would very much like GPT-f for something like SMT, then it could actually make Dafny efficient to check (and probably avoid needing to help it out when it gets stuck!) 0. https://analyticsindiamag.com/what-is-gpt-f/ https://analyticsindiamag.com/what-is-gpt-f/
- IAmLiterallyAB 5y agoSomeone tell Gödel
- jostmey 5y agoI see a different path forward based on the success of AlphaGo. This looks like a clever example of supervised learning. But supervised learning doesn't get you cause and effect, it is just pattern matching. To get at cause and effect, you need reinforcement learning, like AlphaGo. You can imagine an AI writing code that is then scored for performing correctly. Overtime the AI will learn to write code that performs as intended. I think coding can be used as a "playground" for AI to rapidly improve itself, like how AlphaGo could play Go over and over again
- deleted 5y ago[deleted]
- Jeff_Brown 5y agoImparting a sense of objective to the AI is surely important, and an architecture like AlphaGo might be useful for the general problem of helping a coder. I'm not seeing it, however, for this particular autocomplete-flavored idiom. AlphaGo learns a game with fixed, well-defined, measurable objectives, by trying it a bazillion times. In this autocomplete idiom the AI's objective is constantly shifting, and conveyed by extremely partial information. But you could imagine a different arrangement, where the coder expresses the problem in a more structured way -- hopefully involving dependent types, probably involving tests. That deeper encoding would enable a deeper AI understanding (if I can responsibly use that word). The human-provided spec would have to be extremely good, because AlphaGo needs to run a bazillion times, so you can't go the autocomplete route of expecting the human to actually read the code and determine what works.
- visarga 5y agoYou mean like AlphaGo where the neural net is combined with MCTS?