Kimina-Prover-Preview — мощный инструмент от MoonshotAI для автоматического построения доказательств в логике первого порядка с использованием LLM

Что это?

Kimina — это "LLM-aided theorem prover", который комбинирует эвристический поиск с языковыми моделями, чтобы строить формальные доказательства по заданной цели и предпосылкам.

Особенности:

Поддержка логики первого порядка (FOL)

Использует LLM (через API OpenAI, Claude и др.) для генерации обоснований

Интеграция с Lean для проверки корректности

Поддерживает кастомные промпты и множественные режимы поиска

Как работает:

Формулируется цель и список предпосылок

LLM предлагает следующий логический шаг

Инструмент проверяет, валиден ли шаг с точки зрения формальной логики

Если успешно — продолжается доказательство

Установка:

git clone https://github.com/MoonshotAI/Kimina-Prover-Preview.git

cd Kimina-Prover-Preview

pip install -r requirements.txt

GitHub: github.com/MoonshotAI/Kimina-Prover-Preview

Источник: github.com

Комментарии: