∇ Модель · grag · C21
Graph RAG Endpoint
Продакшн-сервис подбора лемм Mathlib и верификации Lean4. Связка GraphDB + PostgreSQL + Qdrant + Lean REPL. Endpoint /grag/search и /grag/check, без обращений к LLM на горячем пути.
Graph RAG Endpoint — продакшн-сервис лаборатории. Реализует pipeline SciLib-GRC21 как REST API.
Endpoints
POST /grag/search— Lean4-цель → категоризированные подсказки лемм (apply / rw / simp / def). 0 LLM-вызовов на горячем пути, типичное время < 200 мс.POST /grag/check— верификация Lean4-доказательства через REPL (Mathlib v4.28.0-rc1).GET /grag/info— описание pipeline и версий.GET /grag/health— health-check.
Стек
| Компонент | Роль | Масштаб |
|---|---|---|
| GraphDB | SPARQL поверх онтологии и графа знаний | ~33.8 M триплетов |
| PostgreSQL | метаданные утверждений, lean_code | 213 338 строк |
| Qdrant | векторный поиск (опционально) | 312-dim, scilib_mathlib_v1 |
| FastAPI + Lean REPL | API + верификация | 2 endpoint, проверка через REPL |
Использование
Без регистрации, без API-ключей. Промышленные интеграции — через info@scilibai.ru. Демо и описание — на странице Graph RAG.
Теги: api, graph-rag, premise-selection, lean4, mathlib