[Art competition] Undecidability in Program Verification

[08kmc09]

Name

Mincheol Kwon

Tool You Used

Adobe Firefly

Short Description

For me, undecidability in program verification means "Generate an image of a machine powered by cogs, with enough room inside for two empty cogwheels of the same size. Ensure that the other cogwheels inside the machine are smaller than the two empty cogwheels. Place this machine on a desk with three equally sized cogs in front of it."

Long Description (up to 3 sentences)

Undecidability must give up one of automatic, terminating, exact verification of the program. So, I described the verification as a machine, with only two gears can be fitted. One of three concepts will remain on the desk.

[KihongHeo]

I find several interesting points here:

• Quality of image is much better than last year. This shows the improvement of AI models.
• Still this AI model cannot understand logical constraints such as "three equally sized", "smaller than", etc. This problem should be solved by logic-based system. I hope you folks tackle such problems later on.
• Short description is longer than long description. 👍

[08kmc09]

I tried to tune my prompt with other LLMs (GPT-3.5, bard), but that prompt was my best effort 😭

[cwlo2F]

Those three gears on the table must be the automatic gear, the terminating gear, and the exact gear. It is fun to imagine what each of the gears actually looks like according to its function, and how they work together. 🙂