Давно уже есть такой ИИ в виде разных математиков из разных стран, которые генерят уеву хучу теорем и док-в к ним. Никто в этом разобраться не может. Ориентируются на громкие имена, журналы и тому подобное. Есть знаменитые теоремы. Одно дело доказательство случайного утверждения про случайно сгенерированные алгебраические структуры, а другое дело доказать гипотезу Римана. Это как с музыкой, есть AI-cлоп, а есть классика. И классику нужно знать.

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

Если теорема очень важная, то нужно потратить время на разбор доказательства. Доказательство — это довольно ригидная формальная вишь, если долго его крутить, то либо его можно будет полностью понять, либо найти там ошибку.

Почему нельзя сосредоточиться на самых важных доказательствах, и заставлять АИ изъясняться понятно?

(Reply to this) (Parent) (Thread)

Проблема Булевых пифагоровых троек вроде была решена компьютером.
Но там доказательство на 200 тб.
А по другому компьютер не может.
Я про такое. Такие доказательства годятся?
Ведь мы их в принципе не можем проверить.

(Reply to this) (Parent) (Thread)

Нет. одно дело это решение перебором, а другое, когда AИ пишет доказательства.

(Reply to this) (Parent) (Thread)

Тоже так думаю...

(Reply to this) (Parent)

1.
обычно, ценность доказательства - это лучше понять предмет.
а сама "истинность" как применимость теоремы менее важна.
напр, гипотеза римана и т.п.

2.
есть ли интересные вопросы в математике, от разрешения которых "оракулом" ИИ будет польза? (см также кристал болл Харви Фридмана, старая дискуссия в ФОМ)

3.
ИИ в принципе может генерировать новые интересные теоремы (как гипотезы об известных сущностях) и теории (как новые формальные модели известных отношений). почему нет?

(Reply to this) (Parent)

а чем решение перебором не угодило? по мне так самый надежный вид доказательства взять и проверить каждую особь, не закоадется ошибка при переопределениях. или вы что-то другое имели ввиду?

(Reply to this) (Parent) (Thread)

Ты Перцев?

(Reply to this) (Parent)

Да ничего на самом деле.

Просто. если АI пишет доказательство — это не то же самое, что задача решена перебором как в случае с пятью красками.

(Reply to this) (Parent) (Thread)

Почти одно и то же как по мне, в любом случае это ситуация когда доказательство достаточно большое чтобы его сделал человек но разбивается на известные составные части чтобы его можно было автоматизировать.

Просто оно может быть широкое (перебор), длинное (цепочка подстановок), сложное (много ветвлений), длинно-широкое и т.д.

(Reply to this) (Parent) (Thread)

Ты дурачок? ИИ пишет доказательства так же, как человек. Дело не в том, что доказательство большое, это просто что-то ранее не известное, имеющее научную новизну.

(Reply to this) (Parent) (Thread)

Хз хз хз хз... Если ИИ оперирует формальной моделью то она может конечно генерировать ранее неведомые утверждения но сделать что-то что не позволяется моделью не может.

Если же ИИ это LLM то она не пишет доказательства. Она пишет слова примерно как человек да (как например Родя в своем бложике). Но чтобы преобразовать это в доказательство нужно загнать это в алгоритм с моделью. Кароч может ли со всем этим справиться ИИ не знаю, думаю что те что щас есть вряд ли.

(Reply to this) (Parent) (Thread)

ИИ, который LLM, строит внутри себя строят внутри себя целостные модели процесса генерации данных — модели мира
https://sergey-57776.medium.com/первое-их-трех-непреодолимых-для-ии-препятствий-преодолено-e0a6c36deaff

>Если же ИИ это LLM то она не пишет доказательства. Она пишет слова примерно как человек да (как например Родя в своем бложике). Но чтобы преобразовать это в доказательство нужно загнать это в алгоритм с моделью.

Что это значит? Давай на примере конкретной статьи разберем
https://sakana.ai/ai-scientist-first-publication/

(Reply to this) (Parent)

This system autonomously generates hypotheses, runs experiments, analyzes data, and writes scientific manuscripts.
https://github.com/SakanaAI/AI-Scientist-v2

(Reply to this) (Parent) (Thread)

>Что это значит

Я имел ввиду что процесс преобразования текст > верифицированное доказательство нуждается в проверке, и как эту самую проверку сделать без участия человека (но чтобы человек мог убедиться что она валидна) мне не ясно.

Конечно эта проблема есть и для текстов написанных человеком. Так что тут проблема не в том что ИИ не может быть как человек, а в том что он не решает проблемы которые есть у человеческих исследователей, а наоборот, масштабирует их.

То что по ссылке, по беглому просмотру, это как раз генератор текстов, т.е. такая улучшенная версия "корчевателя".

(Reply to this) (Parent) (Thread)

да этот чорт тут уже носился с этими "статьями" и ему уже объясняли что это говно

(Reply to this) (Parent) (Thread)

"объяснили"

(Reply to this) (Parent)

А откуда берётся процесс преобразования текст -> верифицированное доказательство, когда процесс обратный?
гипотеза -> проверка -> доказательство -> превращение в статью?
Компьютер сначала проверяет, а потом генерирует текст. Человек проверяет тем же методом, что и для обычных статей - через рецензирование.

Ты текст по ссылке смог вообще прочитать и понять?

>что он не решает проблемы которые есть у человеческих исследователей

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

Если требуются практические эксперименты, то, конечно, добавлятся внешние ограничения, ИИ превосходит человек лишь в скорости и точности обработки информации.

Недавно добрый люди прислал мне линк на свежую статью из Cell (1)). Там биофизики рассказали, как при помощи машинного обучения проанализировали десятки тысяч микробных геномов открытой базы данных. Собственно, это база Центра исследований микробиома в Технологическим университете в Квинсланде (Австралия). Ну и состав этого центра и множество авторов статьи в Cell сильно пересекаются, разумеется (но база и правда открытая, можете воспользоваться (2)). Так вот! Их алгоритм нашел более 800 тысяч фрагментов ДНК (ДНК участников микробиома, разумеется), которые кодируют потенциальные антимикробные соединения. Как они утверждают, 90% из этих фрагментов не были описаны прежде. И вот что важно: три из 100 соединений, синтезированных исследователями, действительно вылечили лабораторных мышей. Если экстраполировать эти процента удачи на остальную массу фрагментов, то у нас только тут что-то около 25 тысяч потенциально работающих антимикробных фрагментов.

Они вообще у себя вот что пишут: Machine learning predicts nearly 1 million new antibiotics in the global microbiome. И это, кажется, еще довольно пессимистичная оценка. И напомню, что сейчас известно всего несколько тысяч разнообразных натуральных и синтетических веществ, применяемых в качестве антибиотиков (все они объединены в 16 крупных классов).
Ну короче. Ураган вариантов.

Правда, непонятно, откуда мы возьмем столько ученых, чтобы проверять эти варианты, но вот в статье в журнале
Science (3) в мае пишут, значить, что уже начали создавать в ассортименте роботизированные лаборатории, чтобы на потоке проверять то, что нагенерили нейросети. Посадил вот так рядышком две нейросети, одна базу с ДНК ковыряет, другая полученные результаты в пробирке растит и проверяет. А человек только сбоку подходит и в окошечке забирает охапкой новые антибиотики, красота.

Если вы думаете, что в предыдущем абзаце я иронизирую, то нет - вот тут (4) пишут, что препараты, открытые ИИ, показывают 80-90% успешности на первой фазе испытаний, по сравнению с обычными 40-60%. Вот это да.
https://t.me/chrdk/1770

Конкретно здесь не БЯМ и пока требуется человеческое участие, но идея такая же.

(Reply to this) (Parent) (Thread)

OK, понял, я просто изначально о другом немного думал - об открытии новых математических фактов. Для обработки данных этот подход думаю рабочий.

(Reply to this) (Parent) (Thread)

Я думаю, в математике должно работать аналогично. Что такое математические факты? Научные открытия это поиск неизвестных существующих закономерностей. ИИ должен с этим справляться лучше человека. Рамануджан доставал какие-то коэффициенты из головы, чисто на интуции, ИИ может делать тоже самое, но с объяснением как они получились.

(Reply to this) (Parent)

>А по другому компьютер не может.

Это аксиома?

(Reply to this) (Parent)

Вручную проверяют алгоритм верификации, а он - все формальные доказательства.

(Reply to this) (Parent) (Thread)

Ты Перцев?

(Reply to this) (Parent) (Thread)

Да, он дроп Хуйлашки.

(Reply to this) (Parent) (Thread)

Ебанутым нет покоя.

(Reply to this) (Parent) (Thread)

самокритично проективно рефлексивно

(Reply to this) (Parent)

Всё так и есть.
В закорючах всяких вербицких никто не разбирается, поэтому они не хуессоры, а профессоры.
Хотя даже анонимное говно постоянно ловит одного из них на противоречиях в днявке.

(Reply to this) (Parent)