Showing cs.AIShow all
2 papers · 1 filter
cs.AI2025
Efficient Neural Clause-Selection Reinforcement
Martin Suda
Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-d…
cs.AI2024
Regularization in Spider-Style Strategy Discovery and Schedule Construction
Filip Bártek, Karel Chvalovský, Martin Suda
To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given pro…