MathKernel：LLMの数学的推論に「証拠」と「信頼ラベル」をもたらすオープンソースの多エンジン計算基盤
MathKernel: An evidence-aware multi-engine mathematics kernel and MCP server
MathKernelは、LLMが数学的意図の解釈に集中し、計算と証拠の記録を専門エンジンに委ねるためのPythonライブラリおよびMCPサーバーです。SymPy、Z3、Lean、mpmathなど複数のエンジンを統合し、各結果に信頼レベル（EXACT、SYMBOLIC、CERTIFIED NUMERIC、FORMALなど）と導出過程のトレイルを付与します。これにより、近似入力の祖先が暗黙のうちに消えることを防ぎ、数学的主張の検証可能性を高めます。
LLMは数学的な意図には優れているが、算術には弱い。MathKernelは役割分担を逆転させる。モデルは解析・計画・解釈を行い、カーネルは計算し、主張固有の証拠を記録する。
- nxobject
余談ですが、「MathKernel」という名前は既に使われています。Mathematica自身のカーネル実行ファイルがそう呼ばれており、既にそれを参照しているツールがある場合、少し残念なことです。
- overfitCNN
私はこの分野でAlkahestというプロジェクトを構築しています: https://github.com/alkahest-cas/alkahest。これはRustで書かれた数式処理システムで、その操作の多くに対して、形式的に検証可能な対応するLean証明書を生成します。AlkahestはPythonライブラリまたはRustクレートとして利用可能です。エージェントでの使用を想定して設計されており、優れたデバッグ出力を備えています。迅速に反復開発を進めているので、問題やコメント、アイデアがあればお気軽にどうぞ。
- xvilka
Woxi[1][2]のサポートも追加できます。ほとんどの記号計算に対応しており、さまざまなPythonライブラリを接着するよりもはるかに高速になるはずです。