शोधकर्ताओं ने TreeThink पेश किया है, जो एक ओपन-सोर्स पायथन लाइब्रेरी है जो न्यू्रल प्रमेय सिद्ध में मॉड्यूलर, पूर्ण रूप से एसींक्रोनस ट्री सर्च के लिए डिज़ाइन की गई है। यह स्थापित सर्च विधियों को vLLM-आधारित इनफरेंस पाइलाइन्स और विविध नोड मूल्यांकन तकनीकों के साथ एकीकृत करती है।
- Lean~4, Rocq, Isabelle/HOL और प्राकृतिक भाषा तर्क का समर्थन करती है।
- वास्तविक समय सत्यापन और प्रमेय अवस्था निष्कर्षण के लिए प्रत्येक भाषा के REPL सर्वर से सीधे जुड़ती है।
- miniF2F और MATH500 बेंचमार्क्स पर एसींक्रोनस निष्पादन से 6.3x तक दीवार-घड़ी गति वृद्धि दिखाता है।
यह लाइब्रेरी क्रॉस-भाषा औपचारिक प्रमेय सर्च और प्राकृतिक भाषा तर्क समर्थन सक्षम बनाती है, जिसका स्रोत कोड MIT लाइसेंस के तहत जारी किया गया है।