Мы привыкли, что большие языковые модели умеют писать код, генерировать тексты и даже объяснять математику — но всё это остаётся вероятностным «угадыванием». Проект ProofOfThought предлагает радикально иной подход: объединить нейросетевое мышление с строгой формальной логикой.
Созданная на Python библиотека ProofOfThought связывает LLM (через OpenAI API) и доказатель теорем Z3, превращая модель в нечто вроде цифрового философа, который не просто отвечает на вопросы, а обосновывает каждый шаг своего вывода.
⚙️ Как это работает
ProofOfThought строится на идее нейросимвольных рассуждений — синтеза нейронных сетей и формальных языков. Архитектура включает два слоя:
🪜 Высокоуровневый API (z3dsl.reasoning) — простой интерфейс для запросов естественного языка.
🧩 Низкоуровневый DSL (z3dsl) — JSON-язык, через который Python взаимодействует с Z3, превращая рассуждение в доказательство.
Пример настолько изящен, что им хочется поделиться целиком:
from openai import OpenAI
from z3dsl.reasoning import ProofOfThought
client = OpenAI(api_key="...")
pot = ProofOfThought(llm_client=client)
result = pot.query("Would Nancy Pelosi publicly denounce abortion?")
print(result.answer) # False
🧠 Здесь LLM переводит фразу на формальный язык, Z3 проверяет логическую непротиворечивость утверждения, и на выходе мы получаем не вероятностный ответ, а результат формального доказательства.
🔬 Почему это важно
💡 Интерпретируемость.
Одно из главных ограничений LLM — невозможность объяснить, почему был дан тот или иной ответ. ProofOfThought решает эту проблему, заставляя модель выражать рассуждения в виде логических формул, которые можно проверить.
⚖️ Надёжность.
Z3 — промышленный SMT-доказатель (Satisfiability Modulo Theories), разработанный Microsoft Research. Он применяется в верификации кода, анализе систем безопасности и даже компиляторах. Объединение с LLM создаёт гибридную систему, где нейросеть предлагает гипотезу, а Z3 подтверждает её строгость.
🚀 Практическое применение.
ProofOfThought уже поддерживает EvaluationPipeline, позволяющий тестировать LLM+Z3 на датасетах вроде StrategyQA и получать метрики точности:
from z3dsl.reasoning import EvaluationPipeline
evaluator = EvaluationPipeline(pot, output_dir="results/")
result = evaluator.evaluate(dataset="strategyqa_train.json", max_samples=10)
print(f"Accuracy: {result.metrics.accuracy:.2%}")
💬 Моё мнение
Как человек, который видел, как ChatGPT уверенно “доказывает” заведомо ложные факты, я считаю ProofOfThought шагом к ответственной AI-логике.
Нейросеть здесь перестаёт быть “оракулом”, и превращается в партнёра по рассуждению, чьи шаги можно верифицировать.
Можно сказать, это первый реальный пример того, что называли System 2 Reasoning — медленного, рационального мышления. То, что отличает нас от машин, постепенно становится их функцией.
Но, конечно, проект только в начале пути. У него нет полноценного NLP-декодера для сложных фраз, а Z3, при всей своей строгости, не всесилен в интерпретации двусмысленностей человеческой речи.
Тем не менее — это направление, где AI перестаёт быть “интуицией” и становится “рассуждением”.
🔗 Источники
- 💻 Репозиторий проекта: ProofOfThought (GitHub)
- 📘 Доклад на NeurIPS 2024: “Proof of Thought: Neurosymbolic program synthesis allows robust and interpretable reasoning”
Если GPT — это талантливый писатель, то ProofOfThought — его строгий редактор-логик.
И, возможно, именно из их сотрудничества вырастет первый по-настоящему мыслящий искусственный интеллект.