О проекте

SciLib — лаборатория семантического анализа научных данных. Объединяет исследователей ФИЦ ИУ РАН (Вычислительный центр им. А. А. Дороницына) и МФТИ ФПМИ. Мы делаем инструменты, которыми пользуемся сами: онтологическое описание научных объектов, граф знаний над формализованными корпусами, мультимодальную векторизацию, и системы контекстного поиска поверх этой инфраструктуры.

Большинство наших артефактов — на открытых лицензиях с указанием авторов. Часть моделей и обучающих корпусов распространяется по запросу из соображений контроля качества и совместного авторства.

Современная наука производит знание быстрее, чем умеет его упорядочивать. Один и тот же научный объект существует в нескольких параллельных формах — формулировка на естественном языке, формула, фрагмент кода в системе доказательств, изображение в статье, элемент в датасете. Эти формы редко связаны друг с другом семантически: поиск по тексту не находит формулу, формула не привязана к коду, код не сослан с журнальной публикацией. Так теряется главное — общий смысл.

SciLib строит инфраструктуру, в которой эти связи восстанавливаются явно. В основе — модульная онтология (OWL/DL), которая строго разделяет три уровня описания научного объекта: интерпретация — что объект значит; представление — в какой форме он выражен; ресурс — где и как он хранится. Такое разделение обеспечивает инвариантность к адресату: одно и то же знание одинаково доступно исследователю и программе, без смешения семантики с техническими деталями реализации.

Поверх онтологии — граф знаний над Mathlib (формализованная математика, Lean4): около 213 000 утверждений с типизированными рёбрами зависимостей (usesInType, usesInValue) и таксономия из 660+ доменных подклассов с провенансом. Векторное пространство построено поверх той же онтологии как семантический контракт — формальные сущности и их эмбеддинги ссылаются на одни и те же идентификаторы.

Это инфраструктура, а не автономный продукт. На ней работают: подбор лемм для целей Lean4 без галлюцинаций, графовая навигация для исследователя, кросс-модальный поиск по пяти представлениям объекта (англоязычный текст, русскоязычный текст, Lean4-код, LaTeX-формула, изображение). В перспективе — расширение онтологии на смежные области (теоретическая физика, формальная логика, теория информации) и привязка формализованных результатов к препринтам и журнальным публикациям через ORCID и DOI.

Лаборатория опирается на компетенции ФИЦ ИУ РАН в построении научных онтологий и цифровых библиотек, и многолетний опыт МФТИ в формализации математики и применении машинного обучения к задачам символьного рассуждения. Мы открыты к сотрудничеству с журналами, университетами и исследовательскими группами — на условиях прозрачных лицензий и совместного авторства.