Об этом проекте

AIQ DKPS Formalization содержит формализации на Lean 4 для эмбеддингов генеративных моделей «черного ящика» на основе ответов, сосредоточенные на пространстве перспективы ядра данных (DKPS) и инфраструктуре многомерного шкалирования (multidimensional-scaling) / спектральных возмущений (spectral-perturbation). Основной библиотекой продукта является ForTauCeti, сопровождаемая специализированными пакетами формализации, такими как DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026 и Helm2025. Эти библиотеки формализуют теорию операторов, многомерное шкалирование с использованием raw-stress, двойное центрирование классического MDS, спектральные возмущения, учет ортогонального выравнивания, идеалы операторов, концентрацию выборочного среднего, распространение высоковероятностных событий и перенос согласованности.