CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems

TL;DR

This paper introduces CSLibPremiseBench, a benchmark for premise retrieval in Lean 4's CSLib library, evaluating various heuristics and a structure-guided reranker, highlighting the influence of repository structure and proxy labels.

Contribution

It provides a reproducible benchmark and empirical analysis of premise retrieval methods specific to CSLib, emphasizing the impact of repository design and label robustness.

Findings

CSG-Rerank offers modest early-rank MRR improvements over BM25.

Proxy labels require explicit caveats due to their limitations.

Repository structure significantly influences premise retrieval performance.

Abstract

CSLib is an emerging Lean 4 library for computer-science formalization, but its premise-retrieval behavior is not well represented by broad mathematical theorem-proving benchmarks. We introduce CSLibPremiseBench, a reproducible CSLib-specific benchmark and empirical study for source-visible premise retrieval over Lean 4 theorem and lemma declarations. The benchmark pins CSLib v4.29.0 at commit 0d37cc7fcc985cfc53b155e7eef2453f846c6da2, builds with Lean 4.29.0, and evaluates a strict import/source-order task set with 801 proxy-labelable tasks and 1875 CSLib candidate declarations. The labels are source-visible CSLib proof-reference proxies, not elaborated Lean dependency traces. We audit label robustness using stricter source-visible matching and a 300-task Lean environment expression probe, then compare BM25, symbol/name overlap, namespace/module and import-graph heuristics, PageRank-style module priors, fixed hybrids, and CSG-Rerank, a structure-guided graph-lexical reranker. CSG-Rerank gives a modest early-rank MRR gain over lexical BM25 under the strict policy, but does not reliably outperform BM25+symbol and does not improve Recall@10. A context-packet audit similarly finds stronger module/family concentration without reliable top-k proxy-gold coverage or token-utility gains. We position CSLibPremiseBench as a benchmark and audit paper: repository structure and candidate-policy design materially shape CSLib premise retrieval, proxy labels require explicit caveats, and proof-generation or proof-repair performance is not claimed.