Pesquisadores apresentam o TreeThink, uma biblioteca Python de código aberto projetada para busca em árvore modular e totalmente assíncrona na prova de teoremas neurais. Ela integra métodos de busca consolidados com pipelines de inferência baseados em vLLM e diversas técnicas de avaliação de nós.
- Suporta Lean~4, Rocq, Isabelle/HOL e raciocínio em linguagem natural.
- Conecta-se diretamente ao servidor REPL de cada linguagem para verificação em tempo real e extração do estado da prova.
- Demonstra aceleração de até 6.3x no tempo real de execução por meio de execução assíncrona nos benchmarks miniF2F e MATH500.
A biblioteca permite a busca de provas formais entre linguagens e suporte ao raciocínio em linguagem natural, com o código-fonte lançado sob a licença MIT.