APOLLO：针对高级形式推理的自动化LLM与Lean协作

本研究解决了利用大型语言模型（LLMs）生成形式证明的挑战，提出了一种名为APOLLO的新方法，通过结合Lean编译器的优势与LLM的推理能力，显著提高了证明生成的效率与准确性。研究表明，APOLLO在保持低采样预算的情况下，实现了新的最高准确率，展示了这一方法在可扩展自动定理证明中的潜在应用价值。