用对偶语言验证自动形式化规范

研究提出“对偶语言”方法：用两种无法结构互译的任务专用形式语言让 LLM 各自独立形式化用户意图，仅当求解器证明两份形式化等价时才接受该规范。在 HumanEval+ 和 LiveCodeBench 上，用 GPT-5.4 mini 与 Qwen3.6-Flash 评测，正确规范占比分别比最强基线提升 12.0% 和 42.9%。