Graph RAG · SciLib

∫ Product

Graph RAG

Подбор лемм Mathlib для целей Lean4: граф знаний и векторная аугментация. Восемь шагов pipeline, без обращений к LLM на горячем пути.

Try it → /grag/info SciLib-GRC21 paper

Pipeline C21

  1. Feature extraction by regex (9 patterns, 0 LLM calls).
  2. Classify patterns: apply / rw / simp / def.
  3. Seed entity resolution via SPARQL to GraphDB.
  4. Graph expansion: usesInType, usesInValue edges.
  5. Enrich from PostgreSQL (lean_code, attributes).
  6. Classify candidates by tactic.
  7. Structured formatting of hints.
  8. Vector augmentation via Qdrant (when needed).

Demo

Request hints

Paste Lean4 code or a goal fragment and get relevant Mathlib lemmas.