How I fell in love with Erlang 🔥 Горячее 💬 Длинная дискуссия
Автор рассказывает о своем пути к любви к Erlang, начавшегося с непонимания базовых концепций программирования в восемь лет, когда столкнулся с выражением "X = X + 1" в BASIC, показавшимся ему математической ложью. В университете он столкнулся с такими же трудностями при изучении C, но продолжил учиться через практику и эксперименты. Переломный момент наступил, когда партнер по бриджу спросил, как суммировать числа от 1 до 10 без циклов, что привело его к открытию рекурсии в Prolog — математически чистого подхода, где описывалось "что" является, а не "как" вычислять.
Знакомство с Erlang произошло случайно на турнире по бриджу от шведского игрока, который описал его как функциональный язык для распределенных, отказоустойчивых систем. Автор был поражен возможностью простого обмена сообщениями между разными узлами без сложных протоколов, демонстрируя пример ping-pong на Erlang. Этот язык, сочетающий функциональность, распределенность и отказоустойчивость, стал тем, что он искал с детства — способом программирования, где математика говорит правду.
Комментарии (209)
- @az09mugen отмечает полезность функции
> cd ..в конце статьи за простоту и мобильную доступность. - @az09mugen предполагает наличие пасхалки (easter egg) в этой функции.
- @Gleamball выражает благодарность за выступление и обмен информацией.
Rule-Based Expert Systems: The Mycin Experiments (1984)
MYCIN — один из первых экспертных систем, разработанных в Стэнфордском проекте эвристического программирования в 1970-х. Эта система использовала правила для диагностики бактериальных инфекций и рекомендации лечения антибиотиками. Её архитектура стала образцом для многих последующих систем: она включала базу знаний с сотнями правил вида «если-то», механизм логического вывода и средства объяснения своих решений.
Ключевые инновации MYCIN — работа с неопределённостью через факторы уверенности, разделение знаний и логики, а также генерация понятных пользователю объяснений. На её основе создали EMYCIN — инструмент для построения других экспертных систем. Книга подводит итог десятилетним экспериментам, анализируя сильные и слабые стороны подхода, и подчёркивает важность практических исследований для развития ИИ.
Комментарии (19)
- Вспоминают ранние подходы к ИИ, включая экспертные системы и перцептроны, как исторический контекст.
- Отмечают практическую пользу экспертных систем и логического программирования (например, на Prolog) для обработки данных.
- Обсуждают, что современные LLM выиграли гонку, но им не хватает логического обоснования и семантики.
- Указывают на ограничения экспертных систем из-за нехватки вычислительных мощностей в прошлом.
- Сравнивают успехи статистических методов (нейросети) с символическим ИИ, признавая победу первых.
ProofOfThought: LLM-based reasoning using Z3 theorem proving 🔥 Горячее 💬 Длинная дискуссия
Нейросимволический синтез программ позволяет создавать надёжные и интерпретируемые системы рассуждений, объединяя нейросетевые подходы с символической логикой. Метод генерирует формальные доказательства для каждого шага рассуждения, что обеспечивает прозрачность и проверяемость результатов, критически важные для таких областей, как автоматизированное доказательство теорем и объяснимый ИИ.
Технология демонстрирует повышенную устойчивость к ошибкам и способность работать со сложными логическими структурами, избегая "галлюцинаций", характерных для чисто нейросетевых моделей. Практическое применение включает автоматизацию рассуждений в математике, верификацию программного кода и создание систем, требующих чёткой аргументации.
Комментарии (164)
- Обсуждение фокусируется на гибридном подходе, сочетающем языковые модели (LLM) для генерации структурированных предположений (например, на JSON DSL или в логических синтаксисах, таких как SMT, Prolog) и последующей верификации этих выводов с помощью детерминированных решателей (таких как Z3) или теорем-проверов (как Lean).
- Участники подчеркивают как потенциал этого подхода для повышения надежности и интерпретируемости рассуждений ИИ, так и его фундаментальные ограничения, такие как «проблема автоформализации» (autoformalization gap) — риск того, что LLM некорректно переведет запрос в формальную логику, что приведет к принципу «мусор на входе — мусор на выходе».
- Приводятся практические примеры применения метода, включая проверку согласованности бизнес-политик, автоматизацию математических вычислений (например, с помощью SymPy) и синтез программ.
- Высказываются критические замечания о природе LLM: они не являются «мыслящими» системами, а лишь статистическими моделями, генерирующими правдоподобные шаблоны, и их вывод принципиально не детерминирован и может быть неполным или ошибочным.
- Обсуждаются технические детали и улучшения, такие как использование структурированных выходов API, ограниченное декодирование для повышения надежности генерации кода и необходимость более четких примеров в документации проектов.
An AI-first program synthesis framework built around a new programming language
Universalis: язык, который читают эксперты, а пишут LLM
Автор: Erik Meijer
- Цель — дать знатокам предметной области возможность формулировать задачи естественным языком и получать готовые программы без участия разработчиков.
- Средство — язык Universalis (в честь Лейбница), исполняемый нейро-компьютером Automind. Код похож на Excel-формулы, обёрнутые в «живые» описания.
Пример
Вопрос: «Алиса купила килограмм яблок за @B и продала за @S. Какой процент прибыли @P?»
Ответ-Universalis:
[@D is (@S-@B)]
[@P is (@D/@B)*100]
Вводим @B=10, @S=17 → @P=70 %.
Особенности
- Синтаксис максимально приближен к естественному языку.
- Внутри — логические предикаты Prolog.
- Поддержка пред-/пост-условий для валидации данных.
- Среда «живого программирования» наподобие электронной таблицы: переключение между формулами и значениями.
Комментарии (14)
- Критика: статья расплывчата, синтаксис «языка» меняется, управляющие конструкции описаны прозой, примеры сводятся к «сделай всё за меня».
- Сомнения: это реальный язык или фантазия LLM?
- Опасения: упрощение ведёт к потоку «мусорного» кода.
- Технические детали: под капотом Kotlin DataFrames, возможна ad-hoc типизация.
- ACM Queue обвиняют в рекламе без упоминания ограничений.
- Перспектива: рано или поздно придётся заново изобретать модули, типы, ошибки, параллелизм и т.д.