10 papers
Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
Kazumi Kasaura, Kei Tsukamoto, Kento Mori +6
Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data p…
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Kazumi Kasaura, Naoto Onda, Yuta Oriike +3
Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produ…
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
Sho Sonoda, Kazumi Kasaura, Yuma Mizuno +2
Understanding and certifying the generalization performance of machine learning algorithms -- i.e. obtaining theoretical estimates of the test error from the training error -- is a…
Near-Optimal Policy Identification in Robust Constrained Markov Decision Processes via Epigraph Form
Toshinori Kitamura, Tadashi Kozuno, Wataru Kumagai +6
Designing a safe policy for uncertain environments is crucial in real-world control systems. However, this challenge remains inadequately addressed within the Markov decision proce…
Compactness in Constructive Mathematics via Affine Logic
Kazumi Kasaura
We study topology, particularly compactness, as an extension of Shulman's work on constructive mathematics via affine logic, while allowing propositional impredicativity. We introd…
Symmetry-Breaking in Multi-Agent Navigation: Winding Number-Aware MPC with a Learned Topological Strategy
Tomoki Nakao, Kazumi Kasaura, Tadashi Kozuno
In decentralized multi-agent navigation, agents that independently compute their controls without communicating goals or intentions can fall into symmetry-induced deadlocks because…