4 accepted papers
Lean is an advanced proof assistant designed to facilitate formal theorem proving by providing a variety of interactive feedback. In this paper, we explore methodologies to leverage proof assistant feedback to augment the capabilities of large language models in constructing formal proofs. First, we…
AlphaStar, the AI that reaches GrandMaster level in StarCraft II, is a remarkable milestone demonstrating what deep reinforcement learning can achieve in complex Real-Time Strategy (RTS) games. However, the complexities of the game, algorithms and systems, and especially the tremendous amount of com…
Sequences with low aperiodic autocorrelation sidelobes are well-known to have extensive applications in active sensing and communication systems. In this paper, we consider the sequence design problem of minimizing the ℓp-norm of the autocorrelation side-lobes, which can then be used to minimize the…
Unimodular sequences with low autocorrelations are desired in many applications, especially in the area of radar and code-division multiple access (CDMA). In this paper, we propose a new algorithm to design unimodular sequences with low integrated sidelobe level (ISL), which is a widely used measure…