3 papers
stat.ML2026
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
Sho Sonoda, Shunta Akiyama, Yuya Uezato
Agentic theorem provers combine a reasoning model, retrieval, search, and a proof assistant verifier, yet it remains unclear which components actually improve finite-budget proof s…
cs.DS2026
On the Complexity of the Matching Problem of Regular Expressions with Backreferences
Soh Kumabe, Yuya Uezato
ReDoS is a well-known type of algorithmic complexity attack, where an adversary supplies maliciously crafted strings to a regular expression matching engine, aiming to exhaust comp…
cs.LG2026
Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
Sho Sonoda, Shunta Akiyama, Yuya Uezato
Agentic theorem provers often introduce intermediate lemmas, proof sketches, or subgoal decompositions before returning to tactic-level search. This can look like an expensive deto…