3 papers
cs.LO2026
LLM2SMT: Building an SMT Solver with Zero Human-Written Code
Mikoláš Janota, Mirek Olšák
Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM…
cs.LO2025
SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Chad E. Brown, Karel Chvalovský, Mikoláš Janota +2
We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathemat…
cs.LO2024
Symbolic Computation for All the Fun
Chad E. Brown, Mikoláš Janota, Mirek Olšák
Motivated by the recent 10 million dollar AIMO challenge, this paper targets the problem of finding all functions conforming to a given specification. This is a popular problem at…