APOLLO là một hệ thống chứng minh định lý tự động kết hợp trình biên dịch Lean và sức mạnh lập luận của LLM để chứng minh các định lý toán học. Trong khi các phương pháp chứng minh định lý dựa trên LLM thông thường tạo ra các bằng chứng vượt qua các hệ thống xác minh thông qua hàng nghìn lần lấy mẫu, APOLLO sử dụng một đường ống mô-đun trong đó LLM tạo ra các bằng chứng, các tác nhân sửa lỗi cú pháp trong các bằng chứng, Lean xác định lỗi, cô lập các định lý con bị lỗi, sử dụng trình giải tự động và gọi LLM một cách tiết kiệm chi phí cho các mục tiêu còn lại. Quá trình kết hợp lại và xác minh lại các bằng chứng con đã sửa này được lặp lại cho đến số lần thử tối đa do người dùng kiểm soát. Trên chuẩn miniF2F, nó đạt độ chính xác 84,9% đối với các mô hình có ít hơn 8B tham số, trong khi vẫn duy trì chi phí lấy mẫu dưới 100. Hơn nữa, nó cải thiện độ chính xác của GoedelProverSFT lên 65,6% và giảm độ phức tạp của mẫu từ 25.600 xuống còn vài trăm.
