мы с вами периодически разговариваем про математику, в частности про успехи моделей в решении математических задач

а тут произошло интересное:
- 25 июля кто-то запостил доказательство гипотезы Коллатца в виде кода на Lean4
- 26 июля пришли баг-репорты в несколько солверов Lean4
- 28 июля кто-то нашел, что вышеупомянутое доказательство эксплуатирует эти баги в солверах

по итогу оказалось, что ИИ научился находить баги в системах проверки для того, чтобы они засчитывали его сгенерированные доказательства, как правильные; учитывая, что ИИ сплошь и рядом делает это при обучении c подкреплением - неудивительно; вот тут - хороший обзор по т.н. reward hacking

P.S. на заглавной картинке - фрактал Коллатца #математика

@valuableai