top | item 42970607

(no title)

ogrisel | 1 year ago

Software Engineering is difficult to verify because it requires dealing with ambiguous understanding of the end-user actual needs / value and subtle trade-offs about code maintainability vs feature coverage vs computational performance.

Algorithmic puzzles, on the other hand, both require reasoning and are easy to verify.

There are other things in coding that are both useful and easy to verify: checking that the generated code follows formatting standards or generating outputs with a specific data schema and so on.

discuss

order

godelski|1 year ago

I agree with you on the first part, but no, code is not easy to verify. I think you missed part of what I wrote. I mean verify that your code is bug free. This cannot be done purely through testing. Formal verification still remains an unsolved problem.

FieryTransition|1 year ago

But if you have a large set of problems to which you already know the answer, then using that in reinforcement learning, then wouldn't the expertise transfer later to problems with no known answers, that is a feasable strategy, right?

Another issue is, how much data can you synthesize in such a way, so that you can construct both the problem and solution, so that you know the answer before using it as a sample.

Ie, some problems are easier to make knowing you can construct the problem yourself, but if you were to solve said problems, with no prior knowledge, they would be hard to solve, and could be used as a scoring signal?

Ie, you are the Oracle and whatever model is being trained doesn't know the answer, only if it is right or wrong. But I don't know if the reward function must be binary or on a scale.

Does that make sense or is it wrong?

voxic11|1 year ago

Formal verification of arbitrary programs with arbitrary specifications will remain an unsolved problem (see halting problem). But formal verification of specific programs with specific specifications definitely is a solved problem.