Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914202213416960 |
|---|---|
| author | Santos, Marco Dos de Saxcé, Hugues Wang, Haiming Wang, Ran Baksys, Mantas Unsal, Mert Liu, Junqi Liu, Zhengying Li, Jia |
| author_facet | Santos, Marco Dos de Saxcé, Hugues Wang, Haiming Wang, Ran Baksys, Mantas Unsal, Mert Liu, Junqi Liu, Zhengying Li, Jia |
| contents | We introduce the Kimina Lean Server, an open-source project designed as a high-performance verifier for reinforcement learning pipelines. Built on top of the Lean REPL (Read-Eval-Print Loop) maintained by the Lean FRO, our server combines server-side parallelism by managing multiple Lean processes in parallel with a Least Recently Used (LRU) caching mechanism that reuses Lean imports across requests. On the client side, a lightweight Python package enables submitting proof batches and receiving Lean feedback, including extracted tactics and tactic states.
Together, these features enable a scalable workflow for large-scale verification and data extraction. In our experiments, the Kimina Lean Server outperforms previous Lean interaction tools, achieving a 1.5 to 2 times speedup in verification time. Moreover, its improved efficiency has enabled its use in the large-scale training of state-of-the-art models such as Kimina-Prover.
We hope that our open-source project will support the neural theorem proving community and accelerate future progress by enabling efficient large-scale verification and proof data extraction. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_21230 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification Santos, Marco Dos de Saxcé, Hugues Wang, Haiming Wang, Ran Baksys, Mantas Unsal, Mert Liu, Junqi Liu, Zhengying Li, Jia Logic in Computer Science We introduce the Kimina Lean Server, an open-source project designed as a high-performance verifier for reinforcement learning pipelines. Built on top of the Lean REPL (Read-Eval-Print Loop) maintained by the Lean FRO, our server combines server-side parallelism by managing multiple Lean processes in parallel with a Least Recently Used (LRU) caching mechanism that reuses Lean imports across requests. On the client side, a lightweight Python package enables submitting proof batches and receiving Lean feedback, including extracted tactics and tactic states. Together, these features enable a scalable workflow for large-scale verification and data extraction. In our experiments, the Kimina Lean Server outperforms previous Lean interaction tools, achieving a 1.5 to 2 times speedup in verification time. Moreover, its improved efficiency has enabled its use in the large-scale training of state-of-the-art models such as Kimina-Prover. We hope that our open-source project will support the neural theorem proving community and accelerate future progress by enabling efficient large-scale verification and proof data extraction. |
| title | Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.21230 |