APOLLO est un système automatisé de démonstration de théorèmes qui combine le compilateur Lean et la puissance de raisonnement de LLM pour démontrer des théorèmes mathématiques. Alors que les méthodes conventionnelles de démonstration de théorèmes basées sur LLM génèrent des preuves qui passent les systèmes de vérification à travers de nombreux (des milliers) d'échantillonnages, APOLLO utilise un pipeline modulaire dans lequel LLM génère les preuves, les agents corrigent les erreurs syntaxiques dans les preuves, Lean identifie les erreurs, isole les sous-théorèmes ratés, utilise un solveur automatique et appelle LLM à moindre coût pour les objectifs restants. Ce processus de recombinaison et de revérification des sous-preuves corrigées est répété jusqu'à un nombre maximal de tentatives contrôlable par l'utilisateur. Sur le benchmark miniF2F, il atteint une précision de 84,9 % pour les modèles de moins de 8 000 paramètres, tout en maintenant un coût d'échantillonnage inférieur à 100. De plus, il améliore la précision de GoedelProverSFT à 65,6 % et réduit la complexité de l'échantillon de 25 600 à plusieurs centaines.
