摘要

我们探讨了在形式数学语言建模背景下专家迭代（expert iteration）的应用。研究发现，在相同的计算预算下，专家迭代（即证明搜索与学习过程交替进行）显著优于仅依赖证明搜索的方法。此外，我们观察到，当应用于一组难度差异较大的形式化命题时，专家迭代能够自动发现并逐步解决难度递增的问题集，而无需依赖相应的真值证明。最后，通过将该专家迭代方法应用于人工精心整理的问题集，我们在miniF2F基准测试中取得了当前最优性能，实现了对多个来自高中数学奥林匹克竞赛的高难度问题的自动求解。