Топологический анализ математических доказательств, генерируемых большими языковыми моделями на формальном языке Lean4

В течение семестра проведено обширное исследование в области генерации математических доказательств на формальном языке Lean4. Изучена литература, произведено ознакомление с синтаксисом и структурой Lean4, а также теорией персистентных гомологий. Собран датасет правильных и неправильных доказательств в Lean4 и разработан дизайн двух экспериментов для разных мощностей. На малых мощностях проведён эксперимент с использованием модели Qwen2.5-coder, который предположительно выявил различия в понимании Lean4 для разных голов модели.

Провести эксперимент на большом датасете с использованием более мощных вычислительных ресурсов. Углублённо исследовать различия в распределении топологических признаков между правильными и неправильными доказательствами на языке Lean4. Изучить альтернативный геометрический подход к анализу доказательств через исследование геометрического места точек эмбедингов тактик и состояний Lean4. Написать текст дипломной работы после получения всех результатов исследований.