7 papers
A Fine-Grained Dichotomy for Bounded-Variable Query Evaluation: The Calculus of Relations, a Boolean Modal Logic, and One-Variable Counting Logic
Yoshiki Nakamura, Yuya Uezato
We study the fine-grained complexity of evaluating Boolean bounded-variable first-order queries over sparse relational structures. For every fixed , every relational signa…
An Exponential Succinctness Gap between Three-Variable Logic and the Calculus of Relations
Yuya Uezato
Three-variable first-order logic (FO3) and the calculus of relations (CoR) define the same binary queries, an equivalence going back to Tarski in the 1940s. While the classical tra…
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…
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…
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…
Regular Expressions with Backreferences and Lookaheads Capture NLOG
Yuya Uezato
Backreferences and lookaheads are vital features to make classical regular expressions (REGEX) practical. Although these features have been widely used, understanding of the unrest…
Accelerating XOR-based Erasure Coding using Program Optimization Techniques
Yuya Uezato
Erasure coding (EC) affords data redundancy for large-scale systems. XOR-based EC is an easy-to-implement method for optimizing EC. This paper addresses a significant performance g…