使用状态链将非形式化证明翻译为形式化证明

我们解决了在受限计算预算下，将自然语言表达的非形式化数学证明翻译为 Lean4 形式化证明的问题。我们的方法基于两个关键见解。首先，非形式化证明往往通过一系列逻辑转换（通常是蕴含或等价）进行，而没有明确指定中间结果或辅助引理。相比之下，诸如 Lean 之类的形式化系统要求显式表示每个证明状态以及连接它们的策略。其次，每个非形式化推理步骤都可以看作是证明状态之间的抽象转换，但识别相应的形式化策略通常需要非平凡的领域知识和对证明上下文的精确控制。为了弥合这一差距，我们提出了一个两阶段框架。我们不直接生成形式化策略，而是首先提取状态链，这是一个与非形式化论证的逻辑结构对齐的中间形式化证明状态序列。然后，我们生成策略以在 CoS 中的相邻状态之间进行转换，从而构建完整的形式化证明。这种中间表示显著降低了策略生成的复杂性，并改善了与非形式化推理模式的对齐。我们构建了专门的数据集和基准用于训练和评估，并引入了一个交互式框架以支持从形式化状态生成策略。实证结果表明，我们的方法大大优于现有基线，实现了更高的证明成功率。