As long as the software is proven correct, who cares how it achieves that?
First, the halting problem is only undecidable on arbitrary programs. Here we would be writing programs specifically to be easy to prove correct. In fact, we would be developing programs and proof at the same time.
Second, determinism is a nice property, but it's independent of whether you can proof software correct.
Have a look at eg randomised quicksort or the 'expected linear time minimum-spanning-tree algorithm' https://en.wikipedia.org/wiki/Expected_linear_time_MST_algor...
Or have a look at HyperLogLog. https://en.wikipedia.org/wiki/HyperLogLog
HyperLogLog only gives you a probabilistic approximation of the true number of distinct items. Here the proof would be about the probability that you are within some acceptable window around the true answer.
Depends on domain, but basically all the same lessons we have for software written the old way by humans.
Which, ah, admittedly isn't great.
> Isn't this the halting problem?
No.
1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
Making your Turing machine non-deterministic doesn't add any power to it in the sense that the halting problem cares about.
> 2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.
> 3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
Proven correct is a much stronger statement than proven to halt eventually. The form usually has to include the latter.
But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
Proof can be done on the program the AI outputs, and doesn't need to be done by the AI.
> But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
We can just tell the AI to do that, at this point. Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
In principle, yes. In practice, people have found it extremely challenging to prove anything about programs that weren't explicitly written to be easy to prove things about.
And AIs are better at writing Lean proofs than just about 99.9% or so of people (exact number is made up). So we might as well have the AI write the proof.
> > But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
> We can just tell the AI to do that, at this point.
Yes, of course. That's my point. And the AI can co-write both proofs and programs.
> Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
You can only realise that subset, by actually writing the proof.
You can think of these automated proofs like a souped up version of eg Rust's or Haskell's type system. You generally don't write a big chunk of Rust code first, and try to work out how to fit it into the type system afterwards. You co-write both.
People sometimes try to retrofit old Python or JavaScript code with types, and that usually has a lot of problems; and these gradual type systems are not nearly as stringent as you need to be for proper proofs.
Absolutely. And then trivially reject programs that have too-long (for whatever value you want) proofs, and train (/fine tune) the models with this as a condition.
If a program is safe, but the smallest proof of it being so is 137 million pages, you can likely already reject it as "too hard" after a million pages even if the program in question is a potential replacement for the Linux kernel.