∂ Публикация · 2026
SciLib-GRC21 · подбор лемм поверх графа знаний
Аннотация
SciLib-GRC21 — pipeline подбора лемм Mathlib для целей Lean4. На входе — Lean4 теорема; на выходе — категоризированные подсказки лемм (apply / rw / simp / def). Пайплайн детерминированный: восемь шагов поверх связки GraphDB (онтология SciLib + MathLib RDF) → PostgreSQL (lean_code, атрибуты) → Qdrant (опциональная векторная аугментация). Без обращений к LLM на горячем пути.
Конструкция (восемь шагов)
- Извлечение признаков по 9 регулярным выражениям (типы Mathlib, имена, тактики).
- Классификация шаблонов: apply / rw / simp / def.
- Разрешение seed-сущностей через SPARQL к GraphDB.
- Расширение по графу: рёбра
usesInType,usesInValue, соседи 1–2 порядка с фильтрацией по типовой совместимости. - Обогащение из PostgreSQL (полный Lean-код, атрибуты, докстринги).
- Обратная классификация кандидатов по применимым тактикам.
- Структурированное форматирование подсказок.
- Опциональная векторная аугментация Qdrant — если граф-кандидатов мало.
Бенчмарк (MiniF2F, 488 задач × 104 запуска = 50 752 прогонов с верификацией Lean REPL)
| Метод | Pass@1 (все 488) | Pass@1 (hard, 59) | p-value vs C21 |
|---|---|---|---|
| A0 (без подсказок) | 48.7% | 3.3% | — |
| LeanSearch | 47.9% | 6.2% | 0.032 |
| LeanFinder | 48.8% | 7.3% | 0.100 |
| LeanExplore | 47.0% | 5.7% | 0.001 |
| SciLib-GRC21 | 50.0% | 8.6% | baseline |
Чисто векторный поиск (без графа) не отличим по статистике от LeanSearch (p = 0.931). Эффект SciLib-GRC21 даёт граф-структура и онтологически управляемая категоризация подсказок, а не качество эмбеддингов.
Доступ
Live API: POST /grag/search, POST /grag/check. Демо на странице Graph RAG. Описание результатов бенчмарка — в карточке эксперимента MiniF2F.