It seems you've summarized my problem properly. Haha.

What I meant in my comment is that when you use formal verification to verify AI, it passes formal verification, but even if it passes that formal verification, the AI still can’t complete the task. The original article also talks about the importance of specifications in the AI era, but my point is that even if it passes formal verification, the AI still has problems. I’m not sure whether I misunderstood the original.

The problem I often run into is this. It’s not formal verification, but I create a UML diagram to lay out the whole skeleton first. There are usually open-source architecture books, so I take it from there.

Then it should implement the whole UML skeleton, right? But it goes like this: halfway through, at some point, it says, “This algorithm is too slow? Hmm... I need to make it faster,” and tries local optimization, so sometimes I don’t get the result I want—that is, an MVP that at least runs.

I know the overall goal clearly, but there’s a problem where it gets obsessed with a specific subgoal or keeps expanding that subgoal.

I think my English is a bit lacking, so I didn't explain my situation well enough.

The main point is not that everything is solved if you specify all the conjunction conditions and prove that those conjunction conditions are correct. Rather, the key point is that in that process, the agent keeps expanding subgoals.

For example, two proofs, P1 and P2, are carried out, but they proceed in a way that diverges from the actual progress of the work. That is, you can prove things like "P1: the chicken is safe" and "P2: the origin of this sauce is trustworthy," but combining these does not make a chicken dish.

In other words, the proof logic holds, but my actual task doesn't get solved. I'm questioning how to solve this problem. It's frustrating that I'm not a native English speaker at times like this. I'm sorry for causing a misunderstanding.

For example, it goes like this.

I proved P1 and P2. But then it creates P1.1. It goes and finds information from an agency certifying that this chicken is safe, and puts that in. Then it starts creating P2.1 as well. The origin of this sauce is trustworthy, but maybe there’s a better one somewhere?

It goes on like that.