Graph RAG · SciLib

∫ Продукт

Graph RAG

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

Попробовать → /grag/info Статья SciLib-GRC21

Pipeline C21

  1. Извлечение признаков по регулярным выражениям (9 шаблонов, 0 LLM).
  2. Классификация шаблонов: apply / rw / simp / def.
  3. Резолвинг seed-сущностей через SPARQL к GraphDB.
  4. Расширение по графу: связи usesInType, usesInValue.
  5. Обогащение из PostgreSQL (lean_code, атрибуты).
  6. Классификация кандидатов по тактикам.
  7. Структурированное форматирование подсказок.
  8. Векторная аугментация через Qdrant (по необходимости).

Демо

Запросить подсказки

Вставьте Lean4-код или фрагмент цели и получите релевантные леммы из Mathlib.