From the 1 of 13 linked papers with an AI index.
13 papers
Neurosymbolic Discovery of Algebraic Graph Constructions
David Seka, Stefan Szeider
There are several methods for searching for graphs with prescribed properties, such as SAT solvers and specialized generators. These methods return the result as raw data: an adjac…
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
Pablo Manrique, Stefan Szeider
The paper presents LeanCSP, a framework built in the Lean theorem prover that can formally verify constraint reformulations and certify solver results for constraint problems, prov…
Algorithm Selection with Zero Domain Knowledge via Text Embeddings
Stefan Szeider
We propose a feature-free approach to algorithm selection: instead of hand-crafted instance features, we use pretrained text embeddings. Our method, ZeroFolio, proceeds in three st…
LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
Stefan Szeider
SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a sta…
Streamliners for Answer Set Programming
Florentina Voboril, Martin Gebser, Stefan Szeider +1
Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language M…
Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design
Hai Xia, Carla P. Gomes, Bart Selman +1
We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and…