Sorry for the stupid question, and I liked the talk and agree it’s a really neat project, but why is it so important? Do you mean important for math, or important for humanity / the future / whatever?
Mostly it just seems significant in the grand scheme of things. Our mathematics is going to become formally verified.
In terms of actual consequences, it’s maybe not so important on its own. But putting a couple pieces together (this, Dan Selsam’s work, GPT), it seems like we’re going to get much better AI-driven automated theorem proving, formal verification, code generation, etc relatively soon.
I’d expect these things to start meaningfully changing how we do programming sometime in the next decade.
Yeah, I get some aesthetic satisfaction from math results being formally verified to be correct. But we could just wait until the AGIs can do it for us… :-P
Yeah, it would be cool and practically important if you could write an English-language specification for a function, then the AI turns it into a complete human-readable formal input-output specification, and then the AI also writes code that provably meets that specification.
I don’t have a good sense for how plausible that is—I’ve never been part of a formally-verified software creation project. Just guessing, but the second part (specification → code) seems like the kind of problem that AIs will solve in the next decade. Whereas the first part (creating a complete formal specification) seems like it would be the kind of thing where maybe the AI proposes something but then the human needs to go back and edit it, because you can’t get every detail right unless you understand the whole system that this function is going to be part of. I dunno though, just guessing.
AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
Sorry for the stupid question, and I liked the talk and agree it’s a really neat project, but why is it so important? Do you mean important for math, or important for humanity / the future / whatever?
Mostly it just seems significant in the grand scheme of things. Our mathematics is going to become formally verified.
In terms of actual consequences, it’s maybe not so important on its own. But putting a couple pieces together (this, Dan Selsam’s work, GPT), it seems like we’re going to get much better AI-driven automated theorem proving, formal verification, code generation, etc relatively soon.
I’d expect these things to start meaningfully changing how we do programming sometime in the next decade.
Yeah, I get some aesthetic satisfaction from math results being formally verified to be correct. But we could just wait until the AGIs can do it for us… :-P
Yeah, it would be cool and practically important if you could write an English-language specification for a function, then the AI turns it into a complete human-readable formal input-output specification, and then the AI also writes code that provably meets that specification.
I don’t have a good sense for how plausible that is—I’ve never been part of a formally-verified software creation project. Just guessing, but the second part (specification → code) seems like the kind of problem that AIs will solve in the next decade. Whereas the first part (creating a complete formal specification) seems like it would be the kind of thing where maybe the AI proposes something but then the human needs to go back and edit it, because you can’t get every detail right unless you understand the whole system that this function is going to be part of. I dunno though, just guessing.
The workflow I’ve imagined is something like:
human specifies function in English
AI generates several candidate code functions
AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
Seems reasonable.