Combining Textual and Structural Information for Premise Selection in Lean
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915644436381696 |
|---|---|
| author | Petrovčič, Job Denis, David Eliecer Narvaez Todorovski, Ljupčo |
| author_facet | Petrovčič, Job Denis, David Eliecer Narvaez Todorovski, Ljupčo |
| contents | Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25\% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_23637 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Combining Textual and Structural Information for Premise Selection in Lean Petrovčič, Job Denis, David Eliecer Narvaez Todorovski, Ljupčo Machine Learning Artificial Intelligence Computation and Language Logic in Computer Science Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25\% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection. |
| title | Combining Textual and Structural Information for Premise Selection in Lean |
| topic | Machine Learning Artificial Intelligence Computation and Language Logic in Computer Science |
| url | https://arxiv.org/abs/2510.23637 |