LLMs are bad at vibing specifications
16 hours ago
- 大语言模型正在生成形式化规约，但常常产生琐碎、同义反复的属性，无法验证任何有意义的内容。
- 许多AI生成的规约由于错误使用了语言特性（如布尔模块）而无法编译或进行模型检验。
- 形式化方法的真正价值在于微妙的属性，但大语言模型倾向于只生成明显而薄弱的属性。
- 使用大语言模型进行形式化方法可能仍然需要专业知识，这引发了对其降低技能门槛程度的质疑。
- 为《程序员逻辑》一书宣布了赠书活动，并提供了多个时区特定的优惠券以解决先前的问题。