金驰

近日，普林斯顿大学团队开源了用于自动定理证明的形式化推理模型Goedel-Prover，并在数学问题的自动形式化证明生成任务上达到SOTA。该模型基于两个形式化转换器训练，其中一个基于Lean Workbook中的非形式-形式语言对训练，另一个采用Claude-sonnet-3.5标注的语言对进行训练。通过专家迭代方法提升性能，在miniF2F上的正确率比最优模型提高7.6%。