LLMs are bad at vibing specifications
16 hours ago
- LLMs are generating formal specifications but often produce trivial, tautological properties that do not verify anything meaningful.
- Many AI-generated specs fail to compile or model-check due to incorrect usage of language features like Boolean modules.
- The true value of formal methods lies in subtle properties, but LLMs tend to generate only obvious, weak properties.
- Using LLMs for formal methods may still require expertise, raising questions about how much they lower the skill threshold.
- A book giveaway for 'Logic for Programmers' is announced with multiple timezone-specific coupons to address previous issues.