> How can it be proven correct if it's not deterministic?
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.
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.
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.
How can it be proven correct if it's not deterministic? Isn't this the halting problem?
> How can it be proven correct if it's not deterministic?
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.
You seem a bit confused?
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.
Can't the non-deterministic LLM produce deterministic software? Assuming it is not allowed to modify the theorem proving software.