Исследователи представляют TreeThink, библиотеку с открытым исходным кодом на Python, предназначенную для модульного полностью асинхронного поиска по дереву в нейронном доказательстве теорем. Она интегрирует устоявшиеся методы поиска с конвейерами вывода на основе vLLM и разнообразными техниками оценки узлов.
- Поддерживает Lean~4, Rocq, Isabelle/HOL и рассуждения на естественном языке.
- Непосредственно подключается к серверу REPL каждого языка для проверки в реальном времени и извлечения состояния доказательства.
- Демонстрирует ускорение до 6.3x по реальному времени за счет асинхронного выполнения на бенчмарках miniF2F и MATH500.
Библиотека обеспечивает поиск формальных доказательств между языками и поддержку рассуждений на естественном языке, исходный код выпущен под лицензией MIT.