基于往返验证与修复的忠实自动形式化

针对大语言模型将自然语言形式化时的忠实度问题，本文提出一种无需真实标注的往返验证方法：将语句形式化后回译为自然语言并再次形式化，利用形式化工具检查逻辑等价性。若结果不一致，通过诊断步骤定位失败阶段并执行针对性修复。在 150 条交通规则上的评估显示，该诊断引导的修复策略将形式等价率从 45-61% 提升至 83-85%，显著优于随机修复基线，且语义漂移更少。