Les chercheurs présentent TreeThink, une bibliothèque Python open-source conçue pour la recherche arborescente modulaire et entièrement asynchrone dans la preuve de théorèmes neurale. Elle intègre des méthodes de recherche établies avec des pipelines d'inférence basés sur vLLM et diverses techniques d'évaluation de nœuds.
- Prend en charge Lean~4, Rocq, Isabelle/HOL et le raisonnement en langage naturel.
- Se connecte directement au serveur REPL de chaque langage pour la vérification en temps réel et l'extraction de l'état de preuve.
- Démontre un gain de vitesse de 6,3x en temps réel grâce à l'exécution asynchrone sur les benchmarks miniF2F et MATH500.
La bibliothèque permet la recherche de preuves formelles inter-langages et le support du raisonnement en langage naturel, avec le code source publié sous licence MIT.