Provensql: İki SQL Sorgusunun Eşdeğerliğini Matematiksel Olarak Kanıtlıyor

Provensql, bir SQL refactor'ünün güvenli olup olmadığı sorusuna kesin cevap vermek için geliştirilmiş açık kaynak bir araç. İki sorguyu karşılaştırıp dört dürüst sonuçtan birini döndürüyor: EQUIVALENT (kanıtlanmış), DIFFERENT (somut bir karşı-örnek satırıyla), SCHEMA_CHANGE veya UNKNOWN — tahmin yürütmek yerine bilmediğini kabul ediyor.

Araç, yapısal olarak sağlam: hiçbir zaman yanlış bir EQUIVALENT sonucu döndürmüyor. Eşdeğerliği bozan 511 mutasyon üzerinde test edildiğinde sıfır hatalı pozitif üretmiş. Konjunktif fragment için bir SMT kanıt motoru, diğer durumlar için karşı-örnek araması kullanılıyor. Karşılaştırma olarak çalıştırılan gpt-5 tabanlı bir LLM yargıcı, 213 etiketli çiftten 2'sinde gerçekte farklı olan sorguları hatalı şekilde eşdeğer ilan etmiş; Provensql'in mimarisi bu tür bir hatayı yapısal olarak imkansız kılıyor.

Özellikle dikkat çeken kısmı, gerçek sayılar üzerinde geçerli olan ama IEEE-754 kayan nokta aritmetiğinde (yeniden gruplama nedeniyle) veya çalışma zamanı hata davranışında (a/b yerine SAFE_DIVIDE gibi) farklılaşan dönüşümleri de yakalayabilmesi — diğer çoğu kontrol aracının bu vakaları 'gerçek sayı' kabul edip sessizce onayladığı bir alan. Provensql, pip ile kurulabiliyor, PR'ları denetleyen bir GitHub Action sunuyor ve Apache-2.0 lisansıyla dağıtılıyor.