Neural Solver

Нейро-символический решатель логических задач — десктопное приложение, объединяющее мощь больших языковых моделей (LLM) с классическим алгоритмом автоматического доказательства теорем (метод резолюций).

🎯 Описание

Neural Solver позволяет решать логические задачи на естественном языке. Вы просто описываете задачу текстом, а система:

1. Парсит естественный язык в формальные логические формулы (КНФ) с помощью LLM
2. Доказывает теорему методом резолюций
3. Объясняет результат на понятном языке с помощью LLM

✨ Возможности

• 🧠 Понимание естественного языка — формулируйте задачи как обычный текст
• ⚡ Метод резолюций — надёжный алгоритм автоматического доказательства теорем
• 📝 Понятные объяснения — результат в виде связного текста, а не сухих формул
• 🖥️ Кроссплатформенность — работает на Windows и Linux
• 🎨 Современный UI — нативное окно с веб-интерфейсом (WebView)

🚀 Быстрый старт

Загрузка готового приложения

Скачайте последний релиз для вашей платформы:

• Windows (app-windows.exe)
• Linux (app-linux) + установлена libwebkit2gtk-4.1-dev

Сборка из исходников

Требования:

• Go 1.23+
• CGO (для WebView)
• Linux: libwebkit2gtk-4.1-dev, libgtk-3-dev

# Клонирование репозитория
git clone https://github.com/Talismanch1k/neuro-solver.git
cd neuro-solver

# Сборка
go build -o neurosolver .

# Запуск
./neurosolver

📖 Примеры использования

Классический силлогизм

Ввод:

Все люди смертны. Сократ — человек. Докажи, что Сократ смертен.

Результат:

Сначала мы берем правило «Если кто‑то человек, то он смертен» и временно считаем, что Сократ не смертен.
Применяя это правило к конкретному объекту Сократ, мы получаем вывод, что тогда Сократ не может быть человеком.
Затем сопоставляем этот вывод с известным фактом, что Сократ человек, и видим прямое противоречие.
Поскольку мы пришли к противоречию, исходное предположение о бессмертии было ложным, значит, Сократ действительно смертен.

🏗️ Архитектура

neurosolver/
├── main.go              # Точка входа, WebView GUI
├── assets/              # Веб-интерфейс (HTML/CSS/JS)
│   ├── index.html
│   ├── style.css
│   └── script.js
├── llmcore/             # Интеграция с LLM (OpenRouter API)
│   ├── llm_queries.go   # API-запросы
│   └── prompts.go       # Системные промпты
├── resolution/          # Движок резолюций
│   └── resolve.go       # Алгоритм доказательства
└── .github/workflows/   # CI/CD (автосборка релизов)

Компоненты

Компонент	Описание
WebView GUI	Нативное окно с embedded веб-интерфейсом
LLM Core	Парсинг NL → КНФ и генерация объяснений
Resolution Engine	Классический алгоритм резолюций с унификацией

⚙️ Конфигурация

Приложение использует OpenRouter API для LLM-запросов. API-ключ встраивается при сборке релизов или может быть задан через переменную окружения:

export OPENAI_API_KEY="your-openrouter-api-key"
./neurosolver

🧪 Тестирование

# Запуск всех тестов
go test ./...

# Тесты движка резолюций
go test ./resolution -v

# Тесты LLM (требуется API-ключ)
go test ./llmcore -v

📚 Технологии

• Go — основной язык
• WebView — нативный GUI с веб-рендерингом
• OpenRouter — доступ к различным LLM
• Метод резолюций — алгоритм автоматического доказательства теорем (простая реализация с экспоненциальным ростом)

📄 Лицензия

MIT License — свободное использование, модификация и распространение.

---

Neural Solver — когда классическая логика встречает современный ИИ 🤖✨