"Intelligent Machines and Idiotic Humans: A Startup Story"
(идеи для AI-стартапов)

Серия 4. Нейронный верификатор кода.

Реально крутая (потенциально) работа "Teaching AI advanced mathematical reasoning" -- как запрещённая в России Мета скрестила нейронную сеть с теорем-прувером Lean и обучила её доказательству теорем, что потенциально позволит автоматизировать занятия формальной верификацией (у людей это получается пока очень дорого и тяжело) и в перспективе гарантировать качество кода и доказывать его безошибочность!

Они похвастались, что дескать теперь наш AI решает в 5 раз больше задач с математических Олимпиад, нежели любой другой, и привели примеры решений. Впрочем, один PhD написал им в комментах, что если эти задачи -- уровень математических Олимпиад, то я потерял уважение ко всем их победителям :)

Но направление крайне перспективное -- состыковываем всяческие символические вычислители с LLM.