Z3 — высокопроизводительный теоретический доказатель, разработанный в Microsoft Research, с API для Python (Z3Py). Он применяется в верификации ПО/железа, решении ограничений, анализе гибридных систем, безопасности и биологии. Базовый синтаксис позволяет создавать переменные через Int('x') или Real('x'), определять ограничения и решать их с помощью solve(). Z3Py поддерживает упрощение выражений simplify(), работу с рациональными и иррациональными числами, а также логические операции And, Or, Not.

Z3 обрабатывает нелинейные полиномиальные ограничения и точно представляет произвольно большие целые числа, рациональные и алгебраические иррациональные числа. Пример решения системы: solve(x > 2, y < 10, x + 2*y == 7). Для вывода результатов можно настроить точность: set_option(precision=30). Важно различать Python-деление 3/2 и рациональные числа Z3, созданные через Q(1,3) или RealVal(1)/3. Система может быть как выполнимой (satisfiable), так и невыполнимой (unsatisfiable).

• Старые заметки 2012 года о Z3/SMT показывают, что API и примеры устарели; вместо Z3Py используйте pip install z3-solver и Python 3.
• Пользователи делятся ссылками на инструменты и ресурсы: knuckledragger, z4-solver, cvc5, SAT/SMT by Example, и примеры на Hakank.org.
• Обсуждение подчеркивает, что SAT/SMT-решатели остаются мощным, но недооцененным инструментом, особенно в сочетании с интерактивными доказательствами.

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

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

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

Простое введение в z3

Изучение мира решателей ограничений на простых примерах.

Что такое решатели?

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

Терминология

В документации z3 много жаргона. Например, «Sort» означает тип, а «constants» — это переменные, которыми оперирует решатель. Solver работает со своим языком SMT-LIB2, а библиотеки переводят код в этот язык.

Простое уравнение

Решим уравнение x + 4 = 7. Вот код на Rust:

use z3::{Solver, ast::Int};
fn main() {
    let solver = Solver::new();
    let x = Int::new_const("x");
    solver.assert(&(x + 4).eq(&7));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    println!("x = {}", model.eval(&x, true).unwrap());
}

Решатель находит x = 3. Это базовый пример, но он показывает принцип работы.

• Обсуждение причин некорректных ответов в задаче о сдаче (coin change) при использовании решателя Z3 без нижних границ, что приводит к минимизации до отрицательной бесконечности.
• Рекомендации ресурсов для изучения SAT/SMT-решателей, включая конкретные PDF-документы и статьи.
• Обсуждение практического применения решателей (Z3, OR-Tools, MiniZinc) для различных задач, включая игры и оптимизацию запросов.
• Сравнение и рекомендации по выбору решателей для начинающих на Python, с упоминанием Z3, OR-Tools и CPMpy.
• Трудности моделирования проблем для решателей и важность правильной постановки ограничений для избежания неинтуитивного поведения.
• Обсуждение технических особенностей интеграции решателей в языки программирования, таких как перегрузка операторов в Rust.
• Упоминание о применении решателей для доказательства теорем и поиска контрпримеров, например, к гипотезе Гольдбаха.