Los investigadores presentan TreeThink, una biblioteca de Python de código abierto diseñada para la búsqueda en árbol modular y completamente asíncrona en la demostración de teoremas con redes neuronales. Integra métodos de búsqueda establecidos con pipelines de inferencia basados en vLLM y diversas técnicas de evaluación de nodos.
- Soporta Lean~4, Rocq, Isabelle/HOL y razonamiento en lenguaje natural.
- Se conecta directamente al servidor REPL de cada lenguaje para verificación en tiempo real y extracción del estado de la demostración.
- Demuestra una aceleración de hasta 6.3x en tiempo real mediante ejecución asíncrona en los benchmarks miniF2F y MATH500.
La biblioteca permite la búsqueda de demostraciones formales entre lenguajes y soporte para razonamiento en lenguaje natural, con el código fuente publicado bajo la licencia MIT.