jdw64

Thank you so much for the advice. I’m a beginner in this area, so your help has been a great help to me. When I did it myself, verification kept being satisfied, but it stayed in a state with no progress; but after working based on your comment, progress seems to have sped up.

Since I’m a freelance programmer, my workflow is far removed from other people’s (there’s no review, and I mostly deliver programs based on whether they run), and I had no place to hear advice from seniors. But rramadass always helps me. Thanks to the advice you gave me, I was able to study formal verification and also study ADTs, and explore a broader world.

Some local regressions still exist, but the big looping around has decreased compared to before. It still seems long-running agents can’t fully replace humans yet. I’m always grateful, and thank you for not getting annoyed and for giving me advice even though I’m always lacking. Have a good day. Thank you so much.

May I save your comment and write it on my homepage later? Your advice seems like it will be a big help. Since I’m mostly doing things by reading manuals and books and running into problems myself, certain problems get solved quickly, but there are sections where I get stuck like this, and I always get a lot of help from you. Thank you always.

Thanks for the advice. This is what I struggle with the most. I’ve learned formal verification other than Lean proofs and used it a few times. It holds up well, but as soon as it becomes a slightly longer-term task, it passes formal verification but turns into work that doesn’t reach the goal G I’m aiming for, and I don’t know how to solve that. I clearly need a separate review agent—have you built a separate harness for the review agent?

Other people say that when they do AI coding, they finish quickly, but for me it’s painful because I keep having to verify it myself.

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.

While learning and applying formal verification in the context of using AI agents, what I feel is that sometimes it's hard to express my own thoughts as formal verification. But more than that, I doubt whether formal verification being done correctly actually solves the phenomenon of AI spinning in circles on a specific task.

For example, I want to eat chicken, so I try formally verifying "chicken dish," and every time GPT or Claude starts digging into the origin of the sauce in the chicken dish or the breed of the chicken. Then the chicken dish never gets finished and never makes it to dinner, and instead I gain deep knowledge about the origin of chickens.

Of course, I know that formal verification has liveness — meaning that there must be progress in the work is also part of formal verification — but the AI judges that learning the origin of the chicken counts as progress too. Yet it ends up doing work that it actually shouldn't be doing.

Personally, while organizing these AI anti-patterns, I feel that when you formally verify one condition, verification of another condition gets weakened, and within that phenomenon I sense the AI spinning in circles again. In the end, I end up going through the process of reading and merging everything one by one myself, and I want to know whether this is something only I experience.

I think it's because technologists are easier to manage.

Product engineers, on the other hand, are actually quite ambiguous to evaluate. Many methodologies have been introduced, starting from Barry Boehm, but over time they gradually stop fitting, and there are many points that are hard to assess. It's essentially a matter of organizational management theory. The ideal of organizational management theory is that diversity comes together to create synergy, but conversely, such diversity means that decision-making within the organization slows down.

Technologists, by contrast, are very easy to observe in terms of speed or code quality. In fact, most people choose a career of learning technology and making money rather than founding a startup, and from that perspective, since "career" tends to be emphasized as an employee's career rather than a founder's career, isn't that why technologists are emphasized?

What companies value as a capability is ultimately an evaluation that can be measured. And product engineering, when you think about it, presupposes discussions with decision makers.

'Is it necessary to implement this feature?'

'Do customers actually need this feature?'

'Isn't the business model wrong?'

Most decision makers are people high up in the hierarchy, and friction with them is unavoidable. In other words, it crosses existing role boundaries, which means more frequent conflicts in organizational dynamics.

Whether that is ultimately a gain or a loss for the organization is something nobody can konw

These days, scraping bots and referrer spam seem really bad. Recently, referrer spam disguised as aocr.org was scraping every corner of my homepage, and as a personal website, it’s a bit of a burden.

I’m not sure whether AI companies can keep going with these low costs. My workflow is already completely merged into AI. I don’t want to go back to digging through Stack Overflow and spending an hour writing 100 lines of code like before.

It’s a pity. If he hadn’t been born in North Korea like that, he would have become a truly great programmer. My life is really hard and painful, but sometimes I think I’m better off than they are.

I'm curious—from what area does a lake count as a large lake? The paper uses Lake Iseo as an example, which makes me wonder.