Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao

摘要

自动形式化（Autoformalization）是指将自然语言表述的数学问题转化为机器可验证的形式化陈述，这对于利用形式化数学推理来解决以自然语言提出的数学问题至关重要。尽管大型语言模型（LLM）能够生成语法正确的形式化陈述，但它们常常无法保留原始问题的语义意图。这一局限性源于当前LLM方法将自动形式化视为一种简单的翻译任务，缺乏人类专家在处理过程中自然具备的自我反思与迭代优化机制。为解决上述问题，我们提出ReForm——一种具有反思能力的自动形式化方法，该方法将语义一致性评估深度集成到形式化生成过程中。该机制使模型能够迭代地生成形式化陈述，评估其语义保真度，并通过逐步优化实现对已识别错误的自我修正。为有效训练这一具有反思能力的模型，我们引入了前瞻性有界序列优化（Prospective Bounded Sequence Optimization, PBSO），该方法在序列生成的不同位置施加差异化的奖励机制，以确保模型在自动形式化和语义验证两方面均具备高准确性，从而避免表面化、浅层化的批评，保障反思过程的有效性。在四个自动形式化基准上的大量实验表明，ReForm相较最强基线方法平均提升达17.2个百分点。为进一步提升评估的可靠性，我们构建了ConsistencyCheck——一个包含859个专家标注样本的基准数据集。该数据集不仅验证了大型语言模型作为评判者的能力，更揭示了自动形式化任务本身的固有难度：即使由人类专家执行，仍会在高达38.5%的情况下产生语义错误。