24 citations · 43 across the 14 of their papers we have counts for
14 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 pr…
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…
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…
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
Naoto Onda, Kazumi Kasaura, Yuta Oriike +3
We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach co…
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…
Provably Efficient RL under Episode-Wise Safety in Constrained MDPs with Linear Function Approximation
Toshinori Kitamura, Arnob Ghosh, Tadashi Kozuno +5
We study the reinforcement learning (RL) problem in a constrained Markov decision process (CMDP), where an agent explores the environment to maximize the expected cumulative reward…
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…
Generation of Geodesics with Actor-Critic Reinforcement Learning to Predict Midpoints
Kazumi Kasaura
To find the shortest paths for all pairs on manifolds with infinitesimally defined metrics, we introduce a framework to generate them by predicting midpoints recursively. To learn…
Swarm Body: Embodied Swarm Robots
Sosuke Ichihashi, So Kuroki, Mai Nishimura +4
The human brain's plasticity allows for the integration of artificial body parts into the human body. Leveraging this, embodied systems realize intuitive interactions with the envi…
Homotopy-Aware Multi-Agent Path Planning on Plane
Kazumi Kasaura
We propose an efficient framework using Dynnikov coordinates for homotopy-aware multi-agent path planning in planar domains that may contain obstacles. We developed a method for ge…
Benchmarking Actor-Critic Deep Reinforcement Learning Algorithms for Robotics Control with Action Constraints
Kazumi Kasaura, Shuwa Miura, Tadashi Kozuno +3
This study presents a benchmark for evaluating action-constrained reinforcement learning (RL) algorithms. In action-constrained RL, each action taken by the learning system must co…
Periodic Multi-Agent Path Planning
Kazumi Kasaura, Ryo Yonetani, Mai Nishimura
Multi-agent path planning (MAPP) is the problem of planning collision-free trajectories from start to goal locations for a team of agents. This work explores a relatively unexplore…
On extension of overconvergent log isocrystals on log smooth varieties
Kazumi Kasaura
By works of Kedlaya and Shiho, it is known that, for a smooth variety over a field of positive characteristic and its simple normal crossing divisor , an overconv…