MathKernel: математическое ядро для LLM, которое доказывает, а не просто вычисляет
MathKernel: An evidence-aware multi-engine mathematics kernel and MCP server
MathKernel — это библиотека Python и MCP-сервер, которые берут на себя вычисления для LLM, возвращая результаты с указанием уровня доверия, движка и полной цепочки вывода. Вместо одного решателя он использует несколько движков: символьный (SymPy), точный, формальный (Lean), сертифицированные интервалы (mpmath) и численный. Каждый результат помечен как SYMBOLIC, EXACT, CERTIFIED NUMERIC или EMPIRICAL, а приблизительные входные данные не могут «тихо» превратиться в точный ответ. Проект охватывает обширную предметную область: от алгебры и графов до дифференциальной геометрии и PDE, с проверяемыми сертификатами и явным разделением доказанного и эмпирического.
LLM хороши в математическом намерении и плохи в математической арифметике. MathKernel меняет разделение труда: модель разбирает, планирует и интерпретирует; ядро вычисляет и записывает доказательства, специфичные для утверждения.
- nxobject
Как замечание: название "MathKernel" уже занято — так называется исполняемый файл ядра самой Mathematica, что немного неудачно, когда у вас уже есть инструменты, которые на него ссылаются.
- overfitCNN
Я разрабатываю проект в этой области под названием Alkahest: https://github.com/alkahest-cas/alkahest. Это система компьютерной алгебры, написанная на Rust, которая генерирует соответствующие сертификаты Lean для многих своих операций, которые можно формально проверить.
Alkahest доступен как библиотека Python или крейт Rust. Он предназначен для использования агентами и имеет хороший вывод для отладки.
Я быстро его развиваю, не стесняйтесь присылать мне любые проблемы/комментарии/идеи.
- xvilka
Вы могли бы также добавить поддержку Woxi[1][2] для большей части символьной математики, это также должно быть намного быстрее, чем куча склеек из разных библиотек Python.