SciLib-GRC21: восемь шагов без LLM

Когда мы начинали Graph RAG для Mathlib, главная задача формулировалась просто: дать Lean-разработчику релевантные леммы быстро и без галлюцинаций. LLM не подходили — они угадывают имена, которых в библиотеке нет. Чистый векторный поиск работал, но плохо переносился между разделами математики и проседал на задачах с сильной типовой структурой.

Идея

Извлечь признаки регулярными выражениями (без обращений к LLM). Найти семена в графе через SPARQL. Расширить через типизированные предикаты usesInType и usesInValue. Обогатить из PostgreSQL. Аугментировать векторами при необходимости. Восемь шагов, ноль LLM-вызовов на горячем пути, типичное время — 80–200 миллисекунд.

Главное наблюдение

Векторный поиск (без графа) статистически неотличим от LeanSearch (p = 0.931). Граф-расширение поверх той же векторной базы — превосходит его значимо. Значит, выигрыш даёт граф-структура и онтологически управляемая категоризация подсказок, а не качество эмбеддингов само по себе.

Полное описание pipeline и метрики — в карточке SciLib-GRC21. Демо — на странице Graph RAG.