«Результаты меня удивили, потому что слово „мозг“ подразумевает единый непрерывный орган, который, казалось бы, должен иметь единое происхождение, — сказал Джокхай.
Оцените глубину открытия - раньше ученые думали что мозг это "единый непрерывный орган", потому что называется одним словом "мозг". Но исследования показали что это не так.
«Наше исследование позволяет предположить, что в процессе эволюции две уже существовавшие нервные системы просто оказались пространственно сближены, — сказал Ло.
То есть раньше было два мозга, в разных частях тела. Но в процессе эволюции они оба перебрались в одно место - в череп. Вообще в этом есть логика. И некоторые решения людей даже подтверждают, что раньше мозг был в другом месте.
Исследователи выяснили это, изучая развивающиеся эмбрионы мышей. Они обнаружили два различных типа клеток‑предшественников мозга. Один тип, в котором экспрессируется ген Otx2, впоследствии превращается в передний и средний мозг. Другой, в котором экспрессируется ген Gbx2, предназначен для формирования заднего мозга.
Это открытие позволило объяснить десятилетия неудач в этой области: учёные пытались превратить один тип клеток‑предшественников в другой, хотя первый принципиально не способен в него превратиться.
Это стандартный метод исследования взаимозависимости, при исследовании дифференциации клеток. Нет цели превратить. Цель узнать превращается или нет.
На протяжении десятилетий исследователи придерживались теории, согласно которой на раннем этапе развития существует единая клетка‑предшественник, из которой затем формируется весь мозг.
Так оно и есть - клетка‑предшественник одна единая. Для всех органов вообще.
Бильярдные системы связывали с вычислениями и раньше, однако прежним моделям требовались дополнительные усложнения: несколько взаимодействующих шаров, трёхмерные конструкции или движущиеся стенки. Миранда и Рамос отказались от всего этого. Для работы их системы достаточно одной частицы, движущейся в двух измерениях между неподвижными стенками.
Тогда конфигурация лабиринта, и форма стенок, должны быть бесконечно сложными. А это противоречит концепции упрощения.
Единичная операция проста - отскок шара от стенки под углом. Но использовать полученный результат для следующей операции уже сложно. И чем больше последовательных операций, тем сложнее конфигурация.
Это только начало истории. Сейчас математики соберутся на сходку, и будут решать что делать с конкурирующей фирмой, грозящей отобрать у них хлеб. Война группировок начинается.
Но что именно означает «решила»?
Создала код на языке lean, который компилируется без ошибок.
Код создается на основе математического текста (всякие формулы и утверждения). Это называется "формализация на языке Lean". Если при компиляции происходит ошибка, то в математический текст вносятся изменения. На основе обновленного текста снова создается код, и происходит попытка компиляции. И так до тех пор пока ошибки не пропадут.
Математический текст генерируется на основе реальных работ написанных математиками.
А как зависит высота опорной орбиты от высоты рабочей? Для рабочей высоты 800 км опорная будет такая же как для 500 км, или должна быть выше?
Почему выгоднее поднимать орбиту на 200 км за счет индивидуальных двигателей на спутниках, а не сразу выводить спутники ближе к рабочей высоте? Это оптимальный вариант чтобы распределить их на орбите в правильном положении друг относительно друга, при пакетном запуске? Так проще растаскивать их по окружности? Или дело в сбросе носителя, и расходе ракетного топлива?
Спутники вышли в разнобой, и довольно далеко от желаемой орбиты. Это просто факт. В чем причина не написано. Причины могут быть разными, и не обязательно связанными с ракетой-носителем. Изначально орбита планировалась еще выше, по некоторым сведениям.
Вопрос еще в том, как правильно выводить спутники на заданную орбиту. По идее чем выше точность, и меньше движений по корректировке, тем лучше, и меньше лишних разговоров.
Какая точность вывода на орбиту считается нормальной? (в +- километрах)
Какой именно чат-бот применялся, не сообщается. ИИ ошибочно определил характер перевозимого груза и указал, что судно якобы транспортирует компоненты ядерного оружия;
получив ложные сведения, аналитик вновь обратился к ИИ — на этот раз для подготовки из них стандартного разведывательного отчёта
Насколько известно, первичные разведданные сейчас создаются системой Maven Smart System от Palantir. А потом эти данные обрабатываются чат-ботом, чтобы военные смогли понять что в них написано.
Видимо все равно произошло недопонимание. Или ИИ хотел угодить военным, и дать им желанную информацию о перевозке ядерного оружия.
Получится, если число вариантов ограничено некоторыми условиями. Например: Количество математических действий ограничено. Количество методов исследования функций в матанализе ограничено. Количество типов математических утверждений ограничено. Есть библиотека доказательств формализованных в Lean. Есть набор математических утверждений, верность которых уже проверена в Lean (эквивалентный код успешно компилируется в Lean). Используя эти утверждения в качестве шаблонов, и подставляя в них тематические элементы (термины и части формул), нужно построить цепочку утверждений, эквивалентный код которой будет успешно компилироваться в Lean. Такая задача может быть решена брутфорсом за ограниченное время. Но не факт что в полученной цепочке утверждений будет общий смысл, и она будет что-то доказывать.
В некотором смысле любая исследовательская задача - это и перебор вариантов в том числе, но не тупой.
Человек осознанно выбирает подходящую методику решения задачи, и учитывает множество факторов. В переборе вариантов есть направленность и рациональность. Кроме того, человек в процессе исследования разрабатывает новые методы решения задач.
Такие истории не имеют смысла без подробного технического описания агента.
они они коллективно решили связаться с людьми за пределами симуляции
Зачем нужно это художественное описание? Из этого непонятно что именно генерировала модель, в какой последовательности, на основе какого промпта, и куда отправлялся результат генерации.
Процесс правильно описывать как "эволюцию данных", а не как "действия агентов". Данные генерируются в ответ на входящий промпт, затем на основе этих данных генерируется следующий промпт в цепочке. Источниками данных для следующего промпта может быть буфер обмена, API, файл, и прочее. Результат генерации может быть текстом или набором команд.
Сначала оцениваешь возможность создания собственного проекта, а когда понимаешь что это дело безнадежное, идешь в найм. Как только чувствуешь что готов создавать собственный проект, уходишь из найма.
Генерировать осмысленные леммы в бесконечном пространстве вариантов случайным перебором невозможно чисто комбинаторно
Для ЛЛМ уже доступна библиотека различных "осмысленных лемм", в различных форматах, включая библиотеку mathlib. Они модифицируются с использованием элементов тематически связанных с уравнением. Элементы выдергиваются в том числе из работ математиков по этой теме. Отдельные утверждения верифицируются в Lean. Генерируются последовательности утверждений, и верифицируются в Lean. Десятки тысяч агентов координированно, избегая дублирования, перебирают варианты достройки цепочки утверждений, "угадывая следующий токен", пока не добьются схождения.
Оцените глубину открытия - раньше ученые думали что мозг это "единый непрерывный орган", потому что называется одним словом "мозг". Но исследования показали что это не так.
То есть раньше было два мозга, в разных частях тела. Но в процессе эволюции они оба перебрались в одно место - в череп. Вообще в этом есть логика. И некоторые решения людей даже подтверждают, что раньше мозг был в другом месте.
Это давно известно. https://pubmed.ncbi.nlm.nih.gov/11748135/
Это стандартный метод исследования взаимозависимости, при исследовании дифференциации клеток. Нет цели превратить. Цель узнать превращается или нет.
Так оно и есть - клетка‑предшественник одна единая. Для всех органов вообще.
Тогда конфигурация лабиринта, и форма стенок, должны быть бесконечно сложными. А это противоречит концепции упрощения.
Единичная операция проста - отскок шара от стенки под углом. Но использовать полученный результат для следующей операции уже сложно. И чем больше последовательных операций, тем сложнее конфигурация.
Чтобы получить несферический шар, надо на него натянуть сову.
Это только начало истории. Сейчас математики соберутся на сходку, и будут решать что делать с конкурирующей фирмой, грозящей отобрать у них хлеб. Война группировок начинается.
Создала код на языке lean, который компилируется без ошибок.
Код создается на основе математического текста (всякие формулы и утверждения). Это называется "формализация на языке Lean". Если при компиляции происходит ошибка, то в математический текст вносятся изменения. На основе обновленного текста снова создается код, и происходит попытка компиляции. И так до тех пор пока ошибки не пропадут.
Математический текст генерируется на основе реальных работ написанных математиками.
Эта тема давно разрабатывается. Про ИИ и Lean4 писали в прошлом году https://habr.com/ru/companies/bothub/news/969334/
Мало технических деталей. Это какой-то выделенный канал связи? Его нельзя заменить обычным доступом через провайдера?
Что за компания? Какой продукт создает?
В итоге важен результат. Было бы интересно узнать насколько успешна деятельность компании в целом, и проследить чем все закончится в данном случае.
А как зависит высота опорной орбиты от высоты рабочей? Для рабочей высоты 800 км опорная будет такая же как для 500 км, или должна быть выше?
Почему выгоднее поднимать орбиту на 200 км за счет индивидуальных двигателей на спутниках, а не сразу выводить спутники ближе к рабочей высоте? Это оптимальный вариант чтобы распределить их на орбите в правильном положении друг относительно друга, при пакетном запуске? Так проще растаскивать их по окружности? Или дело в сбросе носителя, и расходе ракетного топлива?
Реальные орбиты и вызывают вопросы, если была заявлена высота 800 километров.
Так сколько нормально "дрейфовать к своей орбите" - 100 км, 200 км? Все равно на какую высоту забрасывать, сами доползут?
Спутники вышли в разнобой, и довольно далеко от желаемой орбиты. Это просто факт. В чем причина не написано. Причины могут быть разными, и не обязательно связанными с ракетой-носителем. Изначально орбита планировалась еще выше, по некоторым сведениям.
Так РосКосмос и занимается - выводит спутники на орбиту, с помощью Союзов.
Вопрос еще в том, как правильно выводить спутники на заданную орбиту. По идее чем выше точность, и меньше движений по корректировке, тем лучше, и меньше лишних разговоров.
Какая точность вывода на орбиту считается нормальной? (в +- километрах)
А на уровне строгих алгоритмов такая задача не решается?
Насколько известно, первичные разведданные сейчас создаются системой Maven Smart System от Palantir. А потом эти данные обрабатываются чат-ботом, чтобы военные смогли понять что в них написано.
Видимо все равно произошло недопонимание. Или ИИ хотел угодить военным, и дать им желанную информацию о перевозке ядерного оружия.
Может DE0-CV? Древняя плата на Cyclone V 5CEBA4F23C7N, у которого 3080 Kbits встроенной памяти.
Получится, если число вариантов ограничено некоторыми условиями. Например: Количество математических действий ограничено. Количество методов исследования функций в матанализе ограничено. Количество типов математических утверждений ограничено. Есть библиотека доказательств формализованных в Lean. Есть набор математических утверждений, верность которых уже проверена в Lean (эквивалентный код успешно компилируется в Lean). Используя эти утверждения в качестве шаблонов, и подставляя в них тематические элементы (термины и части формул), нужно построить цепочку утверждений, эквивалентный код которой будет успешно компилироваться в Lean. Такая задача может быть решена брутфорсом за ограниченное время. Но не факт что в полученной цепочке утверждений будет общий смысл, и она будет что-то доказывать.
Человек осознанно выбирает подходящую методику решения задачи, и учитывает множество факторов. В переборе вариантов есть направленность и рациональность. Кроме того, человек в процессе исследования разрабатывает новые методы решения задач.
Такие истории не имеют смысла без подробного технического описания агента.
Зачем нужно это художественное описание? Из этого непонятно что именно генерировала модель, в какой последовательности, на основе какого промпта, и куда отправлялся результат генерации.
Процесс правильно описывать как "эволюцию данных", а не как "действия агентов". Данные генерируются в ответ на входящий промпт, затем на основе этих данных генерируется следующий промпт в цепочке. Источниками данных для следующего промпта может быть буфер обмена, API, файл, и прочее. Результат генерации может быть текстом или набором команд.
Сначала оцениваешь возможность создания собственного проекта, а когда понимаешь что это дело безнадежное, идешь в найм. Как только чувствуешь что готов создавать собственный проект, уходишь из найма.
Разве смысл в экономии? Другой разработчик мог за то же время заработать 200 евро, и купить фирменное решение.
Для ЛЛМ уже доступна библиотека различных "осмысленных лемм", в различных форматах, включая библиотеку mathlib. Они модифицируются с использованием элементов тематически связанных с уравнением. Элементы выдергиваются в том числе из работ математиков по этой теме. Отдельные утверждения верифицируются в Lean. Генерируются последовательности утверждений, и верифицируются в Lean. Десятки тысяч агентов координированно, избегая дублирования, перебирают варианты достройки цепочки утверждений, "угадывая следующий токен", пока не добьются схождения.
Что это означает?