MathKernel, LLM'lere Python kütüphanesi ve MCP sunucusu aracılığıyla kanıt farkındalıklı matematik sunuyor

LLM'ler için tasarlanmış bir matematik runtime'ı

GitHub üzerinde herkese açık olarak barındırılan ve Hacker News'in ana sayfasında öne çıkan MathKernel adlı proje, kendisini dil modelleri için tasarlanmış kanıt farkındalıklı, çok motorlu bir matematik runtime'ı olarak tanımlıyor. Projenin deposuna göre iki biçimde geliyor — bir Python kütüphanesi olan mathkernel ve bir MCP sunucusu olan mathkernel-mcp — böylece sıradan uygulamalar ve LLM agent'ları aynı hesaplama yüzeyini kullanabiliyor. MCP paketlemesi, mevcut LLM istemcilerinin zaten konuştuğu tool-calling kurallarına doğrudan bağlanmasını sağlıyor.

Temel varsayım, modellerin kullanıcının matematiksel olarak ne istediğini yorumlamakta iyi, aritmetiği yürütmekte ise kötü olduğudur. MathKernel işi buna göre bölüyor: model ayrıştırır, planlar ve yorumlar; çekirdek ise hesaplar ve her sonuca talebe özgü kanıtlar ekler.

Bir orkestrasyon katmanı, bir solver daha değil

Depodaki belgelendirme, MathKernel'ın tek bir solver değil, tipli bir orkestrasyon katmanı olduğunu vurguluyor. Herkese açık bir facade; ayrıştırma, bağlamlar, nesne kimliği, kalıcılık, kanıt oluşturma, kaynak politikası ve türetim izlemeyi üstlenirken, asıl matematik alan adaptörlerine emanet ediliyor. Özellik matrisi, altta yatan yerleşik motorlara itibar ediyor: sembolik cebir ve analiz için SymPy; akıl yürütme ve biçimsel doğrulama için Z3 ve Lean; sertifikalı sayısal hesaplar için mpmath ve interval modülü; performans açısından kritik yollar için NumPy, SciPy, numba ve CUDA kernel'ları.

Sunum katmanları bilinçli olarak aşağı akışta konumlanıyor. Belgelendirmeye göre görselleştirme ve sonifikasyon bileşenleri kanıtı görüntüleyebilir, ancak cilalı bir grafik ya da ses eseri üretmek daha güçlü matematiksel kanıt oluşturmuyor.

Güven etiketleri ve türetim izleri

Her sonuç açık bir güven düzeyi, bir motor etiketi ve bir türetim izi taşıyor. Proje; kesin hesabı, doğrulanmış sertifikaları, sembolik sonuçları, sertifikalı kapsamları, ampirik kanıtları ve biçimsel kanıtları birbirinden farklı iddia türleri olarak ele alıyor ve yalnızca kesin aritmetiğin bir biçimsel kanıt olmadığını açıkça belirtiyor. Girdileri yaklaşıklara dayanan sonuçlar bu kökeni sessizce bırakmak yerine koruyor. Güven modelinde iki ek uyarı daha yer alıyor: motorlar arasındaki uzlaşma tek başına bir kanıt değildir ve tek bir güven etiketi tam kanıt paketinin yerine geçmez.

Özellik matrisi her yeteneği kanıt tavanına göre derecelendiriyor. Sembolik cebir sonuçları SYMBOLIC olarak etiketleniyor ve yaklaşık girdi kökeni bu etiketi düşürebiliyor. Kesin graf algoritmaları EXACT tanık sertifikaları üretirken, NP-zor optimizasyon sonuçları OPTIMUM, CANDIDATE, IMPOSSIBLE ya da UNKNOWN olarak etiketleniyor; böylece bir şeyin var olmadığı sezgisel olarak iddia edilmiyor. Akıl yürütme görevleri — yükümlülük planlama, eşdeğerlik denetimleri, karşı örnek arama — hangi doğrulayıcının desteklediğine bağlı olarak SYMBOLIC, EXACT veya FORMAL olarak geri dönüyor.

Kapsamın genişliği

Belgelenmiş hesaplama yüzeyi geniş: analiz ve seriler, yakınsaklık bölgesi yükümlülükleriyle integral dönüşümleri, rezidüler ve konform dönüşümler dahil kompleks analiz, tipli sürekli olasılık, üreten fonksiyonlarla kesin kombinatorik, GF(p^m)'ye kadar sonlu cebir ve Smith/Hermite normal formları, kesin lineer cebir, keyfi hassasiyetli tam sayı aritmetiği ve sembolik gidiş-dönüş denetimleriyle TypeScript, Python veya Rust'a kod üretimi. Ayrıca araştırma düzeyinde alanlara da uzanıyor — Koopman tabanlı sonlu dinamiği, dallanan Markov tensörleri ve kesin özdeşliklerin, sayısal spektrumların ve Monte Carlo denetimlerinin etiketlenip ayrı tutulduğu bir bilgi geometrisi ve istatistiksel çıkarım alanları ailesi.

Neden önemli

Bugün çoğu LLM matematik aracı bir Python REPL'inden veya tek bir bilgisayar cebiri sisteminden ibaret. Bu, modelin bir sonucun ne kadar güveni hak ettiğini bilmesi gerektiğinde — bir sadeleştirmenin bir varsayımı gizleyip gizlemediğinde, bir kayan nokta sonucunun sertifikalı olup olmadığında, bir optimal çözümün gerçekten optimal olup olmadığında — yetersiz kalıyor. MathKernel'ın bahsi, köken bilgisinin agent'lı matematik için birinci sınıf bir gereklilik olduğudur: biçimsel bir kanıtı makul bir sembolik cevaptan ayırt edebilen bir agent, ne zaman daha fazla hesaplayacağına, daha sıkı doğrulayacağına ya da temkinli davranacağına karar verebilir. Tasarım tercihleri — iddiaların girdi kökeniyle sınırlanması, sunumun kanıtı şişirmesinin yasaklanması, yokluğun asla sezgisel olarak iddia edilmemesi — LLM destekli matematikтин nasıl görünebileceğine dair kayda değer derecede titiz bir yaklaşım. Güven modelinin bu kadar çok motor arasında pratikte tutup tutmayacağı ise projenin yanıtlaması gereken açık soru.