通过对照语言验证 LLM 自动形式化规格的论文

论文提出用对照语言（contrapuntal languages）验证 LLM 自动形式化生成的代码规格：构造一对任务专用形式语言，各自独立形式化用户意图，仅当求解器证明两种形式化等价时才接受该规格，以实现错误去相关。