ILP + SMT: Regeln mit präzisen numerischen Grenzen lernen

In einer neuen Veröffentlichung wird gezeigt, wie das Inductive Logic Programming‑System PyGol nahtlos mit dem SMT‑Solver Z3 zusammenarbeitet. Kandidatenschlüsse, die von PyGol generiert werden, werden als quantifier‑freie Formeln über Hintergrundtheorien wie lineare oder nichtlineare reelle Arithmetik interpretiert. Dadurch können numerische Parameter instanziiert und von Z3 verifiziert werden, während die deklarative, relationale Bias‑Struktur von ILP erhalten bleibt.

Das Ergebnis ist eine hybride Regelbasis, die symbolische Prädikate mit lernbaren numerischen Einschränkungen kombiniert – von Schwellenwerten und Intervallen bis hin zu mehrteiligen arithmetischen Relationen. Durch die modulare Architektur lassen sich neue, komplexere Regeln ableiten, die zuvor in klassischen ILP‑Systemen schwer zu erfassen waren.

Die Autoren formalisierten das SMT‑ILP‑Framework und testeten es an einer Reihe synthetischer Datensätze, die lineare, relationale, nichtlineare und mehrstufige Schlussfolgerungen forderten. Die Ergebnisse demonstrieren, dass die Kombination von ILP und SMT die Ausdruckskraft symbolischer Regellernen deutlich erweitert und zugleich eine flexible Basis für zukünftige Erweiterungen bietet.