HumanEval160

[marcusrossel]

Any ideas for interesting theorems?

[jt0202]

I think that evaluation is simple enough that there is no theorem needed. The most interesting part is the parser, but formalizing the correctness seems like a very big task. I am not sure in general if the parser based tasks are a good fit to verify.

[marcusrossel]

@jt0202 Would you have any ideas for theorems about the parser? I simply don't know which kinds of properties would be interesting.

[jt0202]

I have never done this so far and always assumed that the parsing was correct and only proved the actual algorithm to be correct. I guess one might define a grammar of the language and then show that the parser accepts exactly those words of the grammar. But this is more in the case of strings. Don't know yet what is best here.

An "interesting" theorem I could think of is that we only accept inputs that are well-formed i.e. the length of the operator list is one less the length of the number list, but you would need to rewrite the algorithm.

[marcusrossel]

I actually found a bug in the parser implementation while trying to verify its correctness!