Hacker News Digest

Нейросимволический синтез программ позволяет создавать надёжные и интерпретируемые системы рассуждений, объединяя нейросетевые подходы с символической логикой. Метод генерирует формальные доказательства для каждого шага рассуждения, что обеспечивает прозрачность и проверяемость результатов, критически важные для таких областей, как автоматизированное доказательство теорем и объяснимый ИИ.

Технология демонстрирует повышенную устойчивость к ошибкам и способность работать со сложными логическими структурами, избегая "галлюцинаций", характерных для чисто нейросетевых моделей. Практическое применение включает автоматизацию рассуждений в математике, верификацию программного кода и создание систем, требующих чёткой аргументации.

• Обсуждение фокусируется на гибридном подходе, сочетающем языковые модели (LLM) для генерации структурированных предположений (например, на JSON DSL или в логических синтаксисах, таких как SMT, Prolog) и последующей верификации этих выводов с помощью детерминированных решателей (таких как Z3) или теорем-проверов (как Lean).
• Участники подчеркивают как потенциал этого подхода для повышения надежности и интерпретируемости рассуждений ИИ, так и его фундаментальные ограничения, такие как «проблема автоформализации» (autoformalization gap) — риск того, что LLM некорректно переведет запрос в формальную логику, что приведет к принципу «мусор на входе — мусор на выходе».
• Приводятся практические примеры применения метода, включая проверку согласованности бизнес-политик, автоматизацию математических вычислений (например, с помощью SymPy) и синтез программ.
• Высказываются критические замечания о природе LLM: они не являются «мыслящими» системами, а лишь статистическими моделями, генерирующими правдоподобные шаблоны, и их вывод принципиально не детерминирован и может быть неполным или ошибочным.
• Обсуждаются технические детали и улучшения, такие как использование структурированных выходов API, ограниченное декодирование для повышения надежности генерации кода и необходимость более четких примеров в документации проектов.

Qodo Command набрал 71,2 % на SWE-bench Verified — стандартном бенчмарке для оценки способности агентов решать реальные задачи из GitHub.

• SWE-bench Verified включает 500 задач из 12 популярных репозиториев (Django, scikit-learn, sympy и др.).
• Каждая задача: описание бага/фичи + тест, который должен проходить после исправления.
• Оценивается только успешность прохождения тестов; стиль и качество кода не учитываются.

Результаты

• 71,2 % — новый рекорд среди публичных решений.
• +18,2 п.п. от предыдущего лидера (CodeStory Aide).
• +31,2 п.п. от первого релиза SWE-bench (2023).

Ключевые инсайты

• Контекст важнее модели: использование 128k-токенного окна и RAG-поиска по 500+ файлам дало +12 %.
• Итерации решают: 3–5 попыток сборки/тестов повышают успех на 8 %.
• Маленькие PR легче: задачи <30 строк кода решаются в 84 % случаев, >200 — лишь 38 %.

Что дальше

• Публикация детального тех-отчёта и открытого датасета.
• Расширение до 1 000 задач и добавление новых языков (Go, Rust).

• Qodo показал 71,2 % на SWE-bench-verified — 5-е место, всего на 1 % уступая официальному Claude Sonnet 4.
• Участники сомневаются в честности результатов и просят независимую платформу с peer-review.
• Поднимаются вопросы о стоимости, эффективности, размере модели и специфике подготовки именно под тест.
• Обсуждают, что сам бенчмарк «закрыт» для Python-ошибок и не отражает реальную разработку.
• Некоторые уже отказались от Qodo в пользу BugBot и сомневаются в жизнеспособности «обёрток» над LLM.