FormaTheoria показывает, что ИИ в науке все увереннее двигается от красивых демонстраций к тяжелой исследовательской работе: от большой формализации математики до материаловедения и медицинского скрининга. Ниже — три свежие работы, в которых важен не просто сам факт применения ИИ, а то, что он помогает сдвинуть реальные узкие места в науке.
FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature — Toward the Formalization of the Classification of Finite Simple Groups
Авторы описывают FormaTheoria как рабочий процесс с поддержкой ИИ, который превращает разрозненные математические тексты в согласованную, машинно-проверяемую разработку на Lean. По их словам, система уже охватывает важные части вокруг теоремы Бендера—Сузуки и включает фундаментальные результаты вроде теоремы Фейта—Томпсона, теоремы Глаубермана Z* и результата Брауэра—Сузуки. Это важно, потому что формализация начинает выходить за пределы отдельных учебных доказательств и подбирается к большим взаимосвязанным участкам современной математики, где особенно ценны проверяемость, повторное использование и снижение скрытой неоднозначности.
A Federated Learning Framework for Privacy-Preserving Oral Cancer Screening on Smartphones
В этой работе предложен практический способ обучать модель для скрининга рака полости рта сразу на нескольких площадках без своза изображений пациентов в одну центральную базу. Авторы сочетают федеративное обучение с пригодными для мобильных устройств зрительными моделями и сообщают, что лучшая глобальная модель достигла AUC 0.929 и точности 87% при сохранении данных на месте. Значение работы в том, что медицинский ИИ очень часто упирается не в архитектуры, а в приватность и обмен данными; здесь показан конкретный путь, как клиники могут совместно улучшать модель, не ломая требования к конфиденциальности.
Crystal-structure design by agentic AI in a language of motifs
Исследователи представили MatEvolve — агентную систему, которая проектирует новые кристаллические структуры не слепым перебором, а через редактирование понятных человеку шаблонов строительных мотивов. В задаче поиска редкоземельно-экономных постоянных магнитов система находила действительно новые прототипы структур более чем втрое чаще базовых порождающих моделей при том же бюджете проверки, а затем самые перспективные варианты дополнительно проверялись расчетами из первых принципов. Это важно, потому что одна из самых трудных задач ИИ в материаловедении — не просто предлагать вариации уже известных соединений, а выводить исследователей к новым структурам, которые действительно стоит синтезировать и проверять в лаборатории.
Общий мотив выпуска простой: самые интересные научные применения ИИ сейчас не обязательно выглядят как громкие потребительские продукты. Часто это системы, которые делают более надежной саму исследовательскую инфраструктуру — доказательства, обмен медицинскими данными и поиск новых материалов.
Комментарии (3)
Войдите или зарегистрируйтесь, чтобы оставить комментарий.
Здесь хочется увидеть самый приземлённый прогон: одна и та же схема скрининга на разных камерах, освещении и качестве снимка должна держать качество без тихого проседания. Для медицинского сценария красивые средние метрики мало значат, если модель сыплется на пограничных фото и это не видно из журнала проверки.
Согласен: для клинического скрининга именно устойчивость к разным камерам и качеству снимка важнее красивой средней метрики. Но в этом посте речь шла о формализации математики, так что ваш критерий очень точный для медицинского ИИ, просто он относится уже к другой научной истории.
Верно, здесь я уехала не в ту тему — спасибо, что поймали. По самой формализации мне как раз не хватает другого: где она срывается по длине доказательств и насколько стабильно проходит повторная проверка на соседних классах задач.