Search

Existing methods for safe multi-agent control using logic specifications like Signal Temporal Logic (STL) often face scalability issues. This is because they rely either on single-agent perspectives or on Mixed Integer Linear Programming (MILP)-based planners, which are complex to optimize. These methods have proven to be computationally expensive and inefficient when dealing with a large number of agents. To address these limitations, we present a new scalable approach to multi-agent control in this setting. Our method treats the relationships between agents using a graph structure rather than in terms of a single-agent perspective. Moreover, it combines a multi-agent collision avoidance controller with a Graph Neural Network (GNN) based planner, models the system in a decentralized fashion, and trains on STL-based objectives to generate safe and efficient plans for multiple agents, thereby optimizing the satisfaction of complex temporal specifications while also facilitating multi-agent collision avoidance. Our experiments show that our approach significantly outperforms existing methods that use a state-of-the-art MILP-based planner in terms of scalability and performance. The project website is https://jeappen.com/mastl-gcbf-website/ and the code is at https://github.com/jeappen/mastl-gcbf ., Comment: Accepted to CoRL 2024. arXiv admin note: text overlap with arXiv:2401.14554 by other authors

Over 2000 Gamma ray sources identified by the Large Area Telescope (LAT) on NASA's Fermi Gamma-ray Space Telescope are considered unassociated, meaning that they have no known counterparts in any other frequency regime. We have carried out an image-based search for steep spectrum radio sources, with in-band spectral index less than -1.4, within the error regions of Fermi unassociated sources using 1 to 1.4 GHz radio data from the MeerKAT Absorption Line Survey (MALS) Data Release. MALS DR1 with a median rms noise of 22 to 25 microJy and 735,649 sources is a significant advance over past image-based searches with improvements in sensitivity, resolution and bandwidth. Steep spectrum candidates were identified using a combination of in-band spectral indices from MALS and existing radio surveys. We developed an optical and infrared source classification scheme in order to distinguish between galactic pulsars and radio galaxies. In total, we identify nine pulsar candidates towards six Fermi sources that are worthy of follow-up for pulsation searches. We also report 41 steep spectrum radio galaxy candidates that may be of interest in searches for high-redshift radio galaxies. We show that MALS due to its excellent continuum sensitivity can detect 80 percent of the known pulsar population. This exhibits the promise of identifying exotic pulsar candidates with future image-based surveys with the Square Kilometre and its precursors., Comment: 13 pages, 5 figures, Accepted for publication in ApJ

We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in Linear Temporal Logic over Finite Traces (LTLf), interpreting them as symbolic finite automata (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures implicit in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach., Comment: To appear at POPL'25

Despite significant advancements in large language models (LLMs) that enhance robot agents' understanding and execution of natural language (NL) commands, ensuring the agents adhere to user-specified constraints remains challenging, particularly for complex commands and long-horizon tasks. To address this challenge, we present three key insights, equivalence voting, constrained decoding, and domain-specific fine-tuning, which significantly enhance LLM planners' capability in handling complex tasks. Equivalence voting ensures consistency by generating and sampling multiple Linear Temporal Logic (LTL) formulas from NL commands, grouping equivalent LTL formulas, and selecting the majority group of formulas as the final LTL formula. Constrained decoding then uses the generated LTL formula to enforce the autoregressive inference of plans, ensuring the generated plans conform to the LTL. Domain-specific fine-tuning customizes LLMs to produce safe and efficient plans within specific task domains. Our approach, Safe Efficient LLM Planner (SELP), combines these insights to create LLM planners to generate plans adhering to user commands with high confidence. We demonstrate the effectiveness and generalizability of SELP across different robot agents and tasks, including drone navigation and robot manipulation. For drone navigation tasks, SELP outperforms state-of-the-art planners by 10.8% in safety rate (i.e., finishing tasks conforming to NL commands) and by 19.8% in plan efficiency. For robot manipulation tasks, SELP achieves 20.4% improvement in safety rate. Our datasets for evaluating NL-to-LTL and robot task planning will be released in github.com/lt-asset/selp.

We discuss the magnetic ground state and properties of a frustrated two-dimensional classical Heisenberg model of interacting hexagonal clusters of spins. The energy of the ground states is found exactly for arbitrary values of $J_1$ (intra-cluster couplings) and $J_2$ (inter-cluster couplings). Our main results concern a frustrated region of the phase diagram, where we show that the set of ground states has a degeneracy larger than that due to global rotation symmetry. Furthermore, the ground state manifold does not have a fixed total magnetization~: there is a range of allowed values. At finite temperature, our Monte-Carlo simulations show that the entropy selects the most probable value of the total magnetization, while the histogram of the Monte-Carlo time series is non-trivial. This model is a first step towards modelling properties of a class of frustrated magnetic structures composed of coupled spin clusters., Comment: 6 pages, 7 figures, submitted to Phys Rev B Letters

We present the second data release of the MeerKAT Absorption Line Survey (MALS), consisting of wideband continuum catalogues of 391 pointings observed at L~band. The full wideband catalogue covers 4344 deg$^2$ of sky, reaches a depth of 10 $\mu$Jy beam$^{-1}$, and contains 971,980 sources. With its balance between survey depth and sky coverage, MALS DR2 covers five orders of magnitude of flux density, presenting a robust view of the extragalactic radio source population down to 200 $\mu$Jy. Using this catalogue, we perform a measurement of the cosmic radio dipole, an anisotropy in the number counts of radio sources with respect to the cosmic background, analogous to the dipole found in the cosmic microwave background (CMB). For this measurement, we present the characterisation of completeness and noise properties of the catalogue, and show that a declination-dependent systematic affects the number density of faint sources. In the dipole measurement on the MALS catalogue, we recover reasonable dipole measurements once we model the declination systematic with a linear fit between the size of the major axis of the restoring beam and the amount of sources of each pointing. The final results are consistent with the CMB dipole in terms of direction and amplitude, unlike many recent measurements of the cosmic radio dipole made with other centimetre wavelength catalogues, which generally show a significantly larger amplitude. This result demonstrates the value of dipole measurements with deeper and more sparse radio surveys, as the population of faint sources probed may have had a significant impact on the measured dipole., Comment: 25 pages, 14 figures. Accepted for publication in Astronomy & Astrophysics. The MALS wideband catalogues and images are publicly available at https://mals.iucaa.in

Entanglement is a key resource for a wide range of tasks in quantum information and computing. Thus, verifying availability of this quantum resource is essential. Extensive research on entanglement detection has led to no-go theorems (Lu et al. [Phys. Rev. Lett., 116, 230501 (2016)]) that highlight the need for full state tomography (FST) in the absence of adaptive or joint measurements. Recent advancements, as proposed by Zhu, Teo, and Englert [Phys. Rev. A, 81, 052339, 2010], introduce a single-parameter family of entanglement witness measurements which are capable of conclusively detecting certain entangled states and only resort to FST when all witness measurements are inconclusive. We find a variety of realistic noisy two-qubit quantum states $\mathcal{F}$ that yield conclusive results under this witness family. We solve the problem of detecting entanglement among $K$ quantum states in $\mathcal{F}$, of which $m$ states are entangled, with $m$ potentially unknown. We recognize a structural connection of this problem to the Bad Arm Identification problem in stochastic Multi-Armed Bandits (MAB). In contrast to existing quantum bandit frameworks, we establish a new correspondence tailored for entanglement detection and term it the $(m,K)$-quantum Multi-Armed Bandit. We implement two well-known MAB policies for arbitrary states derived from $\mathcal{F}$, present theoretical guarantees on the measurement/sample complexity and demonstrate the practicality of the policies through numerical simulations. More broadly, this paper highlights the potential for employing classical machine learning techniques for quantum entanglement detection., Comment: 20 pages, 5 figures

Motivated by risk-sensitive reinforcement learning scenarios, we consider the problem of policy evaluation for variance in a discounted reward Markov decision process (MDP). For this problem, a temporal difference (TD) type learning algorithm with linear function approximation (LFA) exists in the literature, though only asymptotic guarantees are available for this algorithm. We derive finite sample bounds that hold (i) in the mean-squared sense; and (ii) with high probability, when tail iterate averaging is employed with/without regularization. Our bounds exhibit exponential decay for the initial error, while the overall bound is $O(1/t)$, where $t$ is the number of update iterations of the TD algorithm. Further, the bound for the regularized TD variant is for a universal step size. Our bounds open avenues for analysis of actor-critic algorithms for mean-variance optimization in a discounted MDP.

We consider the problem of estimating the Optimized Certainty Equivalent (OCE) risk from independent and identically distributed (i.i.d.) samples. For the classic sample average approximation (SAA) of OCE, we derive mean-squared error as well as concentration bounds (assuming sub-Gaussianity). Further, we analyze an efficient stochastic approximation-based OCE estimator, and derive finite sample bounds for the same. To show the applicability of our bounds, we consider a risk-aware bandit problem, with OCE as the risk. For this problem, we derive bound on the probability of mis-identification. Finally, we conduct numerical experiments to validate the theoretical findings.

Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library. In this paper, we consider the specification and verification of such representation invariants using symbolic finite automata (SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries. To facilitate modular and compositional reasoning, we integrate SFAs into a refinement type system to qualify stateful computations resulting from such interactions. The particular instantiation we consider, Hoare Automata Types (HATs), allows us to both specify and automatically type-check the representation invariants of a datatype, even when its implementation depends on stateful library methods that operate over hidden state. We also develop a new bidirectional type checking algorithm that implements an efficient subtyping inclusion check over HATs, enabling their translation into a form amenable for SMT-based automated verification. We present extensive experimental results on an implementation of this algorithm that demonstrates the feasibility of type-checking complex and sophisticated HAT-specified OCaml data structure implementations., Comment: PLDI'24

Data-driven neural path planners are attracting increasing interest in the robotics community. However, their neural network components typically come as black boxes, obscuring their underlying decision-making processes. Their black-box nature exposes them to the risk of being compromised via the insertion of hidden malicious behaviors. For example, an attacker may hide behaviors that, when triggered, hijack a delivery robot by guiding it to a specific (albeit wrong) destination, trapping it in a predefined region, or inducing unnecessary energy expenditure by causing the robot to repeatedly circle a region. In this paper, we propose a novel approach to specify and inject a range of hidden malicious behaviors, known as backdoors, into neural path planners. Our approach provides a concise but flexible way to define these behaviors, and we show that hidden behaviors can be triggered by slight perturbations (e.g., inserting a tiny unnoticeable object), that can nonetheless significantly compromise their integrity. We also discuss potential techniques to identify these backdoors aimed at alleviating such risks. We demonstrate our approach on both sampling-based and search-based neural path planners.

Superconductivity was recently reported in several quasicrystalline systems. These are materials which are structurally ordered, but since they are not translationally invariant, the usual BCS theory does not apply. At the present time, the underlying mechanism and the properties of the superconducting phase are insufficiently understood. To gain a better understanding of quasiperiodic superconductors, we consider the attractive Hubbard model on the Fibonacci chain, and examine its low-temperature superconducting phase in detail using the Bogoliubov-de Gennes mean-field approach. We obtain superconducting solutions as a function of the parameters controlling the physical properties of the system: the strength of the Hubbard attraction $U$, the chemical potential $\mu$, and the strength of the modulation of the Fibonacci Hamiltonian, $w$. We find that there is a bulk transition at a critical temperature that obeys a power law in $U$. The local superconducting order parameter is self-similar both in real and perpendicular space. The local densities of states vary from site to site, however, the width of the superconducting gap is the same on all sites. The interplay between the Hubbard attraction and the intrinsic gaps of the Fibonacci chain results in a complex zero-temperature $\mu$-$U$ phase diagram with insulating domes surrounded by superconducting regions. Finally, we show that tuning $w$ from weak to strong quasicrystalline modulation gives rise to qualitatively different thermodynamic behaviors as could be observed by measuring the specific heat.

The astronomical community is grappling with the increasing volume and complexity of data produced by modern telescopes, due to difficulties in reducing, accessing, analyzing, and combining archives of data. To address this challenge, we propose the establishment of a coordinating body, an "entity," with the specific mission of enhancing the interoperability, archiving, distribution, and production of both astronomical data and software. This report is the culmination of a workshop held in February 2023 on the Future of Astronomical Data Infrastructure. Attended by 70 scientists and software professionals from ground-based and space-based missions and archives spanning the entire spectrum of astronomical research, the group deliberated on the prevailing state of software and data infrastructure in astronomy, identified pressing issues, and explored potential solutions. In this report, we describe the ecosystem of astronomical data, its existing flaws, and the many gaps, duplication, inconsistencies, barriers to access, drags on productivity, missed opportunities, and risks to the long-term integrity of essential data sets. We also highlight the successes and failures in a set of deep dives into several different illustrative components of the ecosystem, included as an appendix., Comment: 59 pages; please send comments and/or questions to foadi@googlegroups.com

We theoretically study the real-space distribution of the supercurrent that flows under a uniform vector potential in a two-dimensional quasiperiodic structure. This is done by considering the attractive Hubbard model on the quasiperiodic Ammann-Beenker structure and studying the superconducting phase within the Bogoliubov-de Gennes mean-field theory. Decomposing the local supercurrent into the paramagnetic and diamagnetic components, we numerically investigate their dependencies on average electron density, temperature, and the angle of the applied vector potential. We find that the diamagnetic current locally violates the current conservation law, necessitating compensation from the paramagnetic current, even at zero temperature. The paramagnetic current shows exotic behaviors in the quasiperiodic structure, such as local currents which are oriented transversally or reversely to that of the applied vector potential., Comment: 14 pages, 11 figures

The MeerKAT Absorption Line Survey (MALS) has observed 391 telescope pointings at L-band (900 - 1670 MHz) at $\delta\lesssim$ $+20\deg$. We present radio continuum images and a catalog of 495,325 (240,321) radio sources detected at a signal-to-noise ratio (SNR) $>$5 over an area of 2289 deg$^2$ (1132 deg$^2$) at 1006 MHz (1381 MHz). Every MALS pointing contains a central bright radio source ($S_{1\,\mathrm{GHz}} \gtrsim 0.2$ Jy). The median spatial resolution is $12^{\prime\prime}$ ($8^{\prime\prime}$). The median rms noise away from the pointing center is 25 $\mu$Jy beam$^{-1}$ (22 $\mu$Jy beam$^{-1}$) and is within $\sim$ 15% of the achievable theoretical sensitivity. The flux density scale ratio and astrometric accuracy deduced from multiply observed sources in MALS are less than 1% (8% scatter) and $1^{\prime\prime}$, respectively. Through comparisons with NVSS and FIRST at 1.4 GHz, we establish the catalog's accuracy in the flux density scale and astrometry to be better than 6% (15% scatter) and $0.8^{\prime\prime}$, respectively. The median flux density offset is higher (9%) for an alternate beam model based on holographic measurements. The MALS radio source counts at 1.4 GHz are in agreement with literature. We estimate spectral indices ($\alpha$) of a subset of 125,621 sources (SNR$>$8), confirm the flattening of spectral indices with decreasing flux density and identify 140 ultra steep-spectrum ($\alpha<-1.3$) sources as prospective high-$z$ radio galaxies ($z>2$). We have identified 1308 variable and 122 transient radio sources comprising primarily of AGN that demonstrate long-term (26 years) variability in their observed flux densities. The MALS catalogs and images are publicly available at https://mals.iucaa.in., Comment: 64 pages, 25 figures, accepted for publication in the ApJS (full version of the paper with complete tables is available at DR1 release notes)

Our understanding of physical properties of quasicrystals owes a great deal to studies of tight-binding models constructed on quasiperiodic tilings. Among the large number of possible quasiperiodic structures, two dimensional tilings are of particular importance -- in their own right, but also for information regarding properties of three dimensional systems. We provide here a users manual for those wishing to construct and study physical properties of the 8-fold Ammann-Beenker quasicrystal, a good starting point for investigations of two dimensional quasiperiodic systems. This tiling has a relatively straightforward construction. Thus, geometrical properties such as the type and number of local environments can be readily found by simple analytical computations. Transformations of sites under discrete scale changes -- called inflations and deflations -- are easier to establish compared to the celebrated Penrose tiling, for example. We have aimed to describe the methodology with a minimum of technicalities but in sufficient detail so as to enable non-specialists to generate quasiperiodic tilings and periodic approximants, with or without disorder. The discussion of properties includes some relations not previously published, and examples with figures., Comment: Review article to appear in Israel Journal of Chemistry

Parser combinators are a well-known mechanism used for the compositional construction of parsers, and have shown to be particularly useful in writing parsers for rich grammars with data-dependencies and global state. Verifying applications written using them, however, has proven to be challenging in large part because of the inherently effectful nature of the parsers being composed and the difficulty in reasoning about the arbitrarily rich data-dependent semantic actions that can be associated with parsing actions. In this paper, we address these challenges by defining a parser combinator framework called Morpheus equipped with abstractions for defining composable effects tailored for parsing and semantic actions and a rich specification language used to define safety properties over the constituent parsers comprising a program. Even though its abstractions yield many of the same expressivity benefits as other parser combinator systems, Morpheus is carefully engineered to yield a substantially more tractable automated verification pathway. We demonstrate its utility in verifying a number of realistic, challenging parsing applications, including several cases that involve non-trivial data-dependent relations., Comment: 41 pages

We consider a queue-channel model that captures the waiting time-dependent degradation of information bits as they wait to be transmitted. Such a scenario arises naturally in quantum communications, where quantum bits tend to decohere rapidly. Trailing the capacity results obtained recently for certain queue-channels, this paper aims to construct practical channel codes for the erasure queue-channel (EQC) -- a channel characterized by highly correlated erasures, governed by the underlying queuing dynamics. Our main contributions in this paper are twofold: (i) We propose a generic `wrapper' based on interleaving across renewal blocks of the queue to convert any capacity-achieving block code for a memoryless erasure channel to a capacity-achieving code for the EQC. Next, due to the complexity involved in implementing interleaved systems, (ii) we study the performance of LDPC and Polar codes without any interleaving. We show that standard Ar{\i}kan's Polar transform polarizes the EQC for certain restricted class of erasure probability functions. We also highlight some possible approaches and the corresponding challenges involved in proving polarization of a general EQC., Comment: 10 pages, 5 figures, accepted to IEEE ISIT 2023

The single electron spectrum and wavefunctions in quasicrystals continue to be a fascinating problem, with few known solutions, especially in two and higher dimensions. This paper investigates the energy spectra and gap structures in tight-binding models on a quasiperiodic tiling in two dimensions. By varying a continuous parameter, we follow the evolution of the band structure from the discrete molecular or atomic states, to the multifractal states well-known from previous studies. We propose a scheme for labeling gaps in finite approximants. It is equivalent in the limit of infinite systems to the one presented by Kellendonk and Putnam based on the algebraic structure of this quasiperiodic system., Comment: Final version, with revised gap label definitions

Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producing all acceptable elements that satisfy the function's input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator's output satisfies this coverage requirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex. To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds ``must-style'' underapproximate reasoning principles as a fundamental part of the type system. The types associated with expressions now capture the set of values guaranteed to be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expression may produce. Beyond formalizing the notion of coverage types in the context of a rich core language with higher-order procedures and inductive datatypes, we also present a detailed evaluation study to justify the utility of our ideas.

Synthesizing planning and control policies in robotics is a fundamental task, further complicated by factors such as complex logic specifications and high-dimensional robot dynamics. This paper presents a novel reinforcement learning approach to solving high-dimensional robot navigation tasks with complex logic specifications by co-learning planning and control policies. Notably, this approach significantly reduces the sample complexity in training, allowing us to train high-quality policies with much fewer samples compared to existing reinforcement learning algorithms. In addition, our methodology streamlines complex specification extraction from map images and enables the efficient generation of long-horizon robot motion paths across different map layouts. Moreover, our approach also demonstrates capabilities for high-dimensional control and avoiding suboptimal policies via policy alignment. The efficacy of our approach is demonstrated through experiments involving simulated high-dimensional quadruped robot dynamics and a real-world differential drive robot (TurtleBot3) under different types of task specifications.

The number counts of homogeneous samples of radio sources are a tried and true method of probing the large scale structure of the Universe, as most radio sources outside the galactic plane are at cosmological distances. As such they are expected to trace the cosmic radio dipole, an anisotropy analogous to the dipole seen in the cosmic microwave background (CMB). Results have shown that although the cosmic radio dipole matches the direction of the CMB dipole, it has a significantly larger amplitude. This result challenges our assumption of the Universe being isotropic, which can have large repercussions for the current cosmological paradigm. Though significant measurements have been made, sensitivity to the radio dipole is generally hampered by systematic effects that can cause large biases in the measurement. Here we assess these systematics with data from the MeerKAT Absorption Line Survey (MALS). We present the analysis of ten MALS pointings, focusing on systematic effects that could lead to an inhomogeneous catalogue. We describe the calibration and creation of full band continuum images and catalogues, producing a combined catalogue containing 16,313 sources and covering 37.5 square degrees of sky down to a sensitivity of 10 $\mu$Jy/beam. We measure the completeness, purity, and flux recovery statistics for these catalogues using simulated data. We investigate different source populations in the catalogues by looking at flux densities and spectral indices, and how they might influence source counts. Using the noise characteristics of the pointings, we find global measures that can be used to correct for the incompleteness of the catalogue, producing corrected number counts down to 100 - 200 $\mu$Jy. We show that we can homogenise the catalogues and properly account for systematic effects. We determine that we can measure the dipole to $3\sigma$ significance with 100 MALS pointings., Comment: 30 pages, 25 figures. Accepted for publication in Astronomy & Astrophysics

We report the detection of stimulated hydrogen radio recombination line (RRL) emission from ionized gas in a $z=0.89$ galaxy using 580--1670 MHz observations from the MeerKAT Absorption Line Survey (MALS). The RRL emission originates in a galaxy that intercepts and strongly lenses the radio blazar PKS 1830-211 ($z=2.5$). This is the second detection of RRLs outside of the local universe and the first clearly associated with hydrogen. We detect effective H144$\alpha$ (and H163$\alpha$) transitions at observed frequencies of 1156 (798) MHz by stacking 17 (27) RRLs with 21$\sigma$ (14$\sigma$) significance. The RRL emission contains two main velocity components and is coincident in velocity with HI 21 cm and OH 18 cm absorption. We use the RRL spectral line energy distribution and a Bayesian analysis to constrain the density ($n_e$) and the volume-averaged pathlength ($\ell$) of the ionized gas. We determine $\log( n_e ) = 2.0_{-0.7}^{+1.0}$ cm$^{-3}$ and $\log( \ell ) = -0.7_{-1.1}^{+1.1}$ pc towards the north east (NE) lensed image, likely tracing the diffuse thermal phase of the ionized ISM in a thin disk. Towards the south west (SW) lensed image, we determine $\log( n_e ) = 3.2_{-1.0}^{+0.4}$ cm$^{-3}$ and $\log( \ell ) = -2.7_{-0.2}^{+1.8}$ pc, tracing gas that is more reminiscent of H II regions. We estimate a star formation (surface density) rate of $\Sigma_{\mathrm{SFR}} \sim 0.6$ M$_{\odot}$ yr$^{-1}$ kpc$^{-2}$ or SFR $\sim 50$ M$_{\odot}$ yr$^{-1}$, consistent with a star-forming main sequence galaxy of $M_{\star} \sim 10^{11}$ M$_{\odot}$. The discovery presented here opens up the possibility of studying ionized gas at high redshifts using RRL observations from current and future (e.g., SKA and ngVLA) radio facilities., Comment: 17 pages, 10 figures, 2 tables, accepted in ApJ