arXiv subjects
Publications and source records attributed to Subhajit Roy.
In this article, we establish Schauder-type estimates for the logarithmic Laplacian. We show that for a $\kappa$-H\"older inhomogeneous term, the solution is also $\kappa$-H\"older in the interior. In fact, the interior regularity slightly exceeds $\kappa$-H\"older smoothness up to a logarithmic correction. Additionally, we prove a Harnack inequality for non-negative solutions.
In this article, we study the equation $$ (-\Delta_p)^s u = f(u) $$ in a bounded domain $\Omega\subset \mathbb{R}^n$, where $n\geq 2$, $p>2$, and $f$ is locally Lipschitz. We establish a strong comparison principle in a fairly general setting and use it to derive symmetry results for positive $C^1$ solutions satisfying Dirichlet boundary conditions. We also show that the $C^1$ regularity assumption is indeed satisfied for $p\in \left[2,\frac{2}{1-s}\right)$.
Inductive generalization is a framework for reinforcement learning (RL) generalization in which inductively related task instances admit inductively related policies. Prior work captures this structure via a higher-order policy-evolution function learned directly with RL, but suffers from poor training scalability: as training tasks grow, aggregated reward feedback becomes noisy and conflicting, destabilizing training and weakening generalization. We propose DIBS, a decoupled behavioral cloning approach that separates learning task-specific policies from learning the evolution function. We first learn individual teacher policies per task via standard RL, then fit the evolution function via behavioral cloning on teacher-labeled state-action pairs. This replaces noisy reward aggregation with dense, stable supervision. DIBS achieves significant improvements in both training stability and zero-shot generalization against existing RL and meta-RL algorithms.
Spintronic nano-neurons offer a promising route towards energy-efficient, high-performance hardware neural networks thanks to their inherent low-input nonlinear dynamics. However, training such networks remains a major bottleneck as it depends on oversimplified models of device behaviour and is highly sensitive to device variability. Here, we introduce a hardware architecture that overcomes these limitations by enabling on-device generation of gradients. First, we introduce theoretically and demonstrate experimentally that magnetic tunnel junctions can generate tunable and complex nonlinear responses. Building on this, we implement an analogue finite-difference approach to enable on-chip training in spintronic neural networks with one and two hidden layers. We experimentally implemented device in the loop backpropagation in a magnetic tunnel junction based neural network, achieving a classification accuracy of 93.3% despite pronounced device variability. During training, the gradients generated by the proposed analog neurons closely match the values derived numerically, without incurring computational overhead. Via physical simulations, we also demonstrate that this approach can be scaled up to support training in deep architectures. Our results pave the way for reliable, trainable and fully analogue spintronic neural networks, opening up new possibilities for next-generation, energy-efficient artificial intelligence hardware.
Convolutional neural networks have remarkably progressed the performance of distinguishing plant diseases, severity grading, and nutrition deficiency prediction using leaf images. However, these tasks become more challenging in a realistic in-situ field condition. Often, a traditional machine learning model may fail to capture and interpret discriminative characteristics of plant health, growth and diseases due to subtle variations within leaf subcategories. A few deep learning methods have used additional preprocessing stages or network modules to address the problem, whereas several other methods have utilized pre-trained backbone CNNs, most of which are computationally intensive. Therefore, to address the challenge, we propose a lightweight autoencoder using separable convolutional layers in its encoder decoder blocks. A sigmoid gating is applied for refining the prowess of the encoders feature discriminability, which is improved further by the decoder. Finally, the feature maps of the encoder decoder are combined for rich feature representation before classification. The proposed Convolutional Lightweight Autoencoder for Plant disease classification, called CLAP, has been experimented on three public plant datasets consisting of cassava, tomato, maize, groundnut, grapes, etc. for determining plant health conditions. The CLAP has attained improved or competitive accuracies on the Integrated Plant Disease, Groundnut, and CCMT datasets balancing a tradeoff between the performance, and little computational cost requiring 5 million parameters. The training time is 20 milliseconds and inference time is 1 ms per image.
For $p\in (1,\infty)$ and $\alpha\in\mathbb{R}$, we consider measurable functions $g$ on $\mathbb{S}^{N-1}$ that satisfy the following weighted Hardy inequality: \begin{equation}\label{abs} \int_{\mathbb{R}^N}\frac{ g (x/|x|)}{|x|^{p+\alpha}}|u(x)|^p dx \leq C\int_{\mathbb{R}^N}\frac{|\nabla u(x)|^p}{|x|^\alpha} dx, \quad\forall\,u\in \mathcal{C}_c^\infty(\mathbb{R}^N), \end{equation} for some constant $C>0$. Depending on $N$, $p$, and $\alpha$, we identify suitable function spaces for $g$ so that \eqref{abs} holds. The constant obtained is sharp, in the sense that it is sharp when $g \equiv 1$. Furthermore, we establish the sharp fractional Hardy inequality with homogeneous weights.
Successful agent-human partnerships require that any agent generated information is understandable to the human, and that the human can easily steer the agent towards a goal. Such effective communication requires the agent to develop a finer-level notion of what is understandable to the human. State-of-the-art agents, including LLMs, lack this detailed notion of understandability because they only capture average human sensibilities from the training data, and therefore afford limited steerability (e.g., requiring non-trivial prompt engineering). In this paper, instead of only relying on data, we argue for developing generalizable, domain-agnostic measures of understandability that can be used as directives for these agents. Existing research on understandability measures is fragmented, we survey various such efforts across domains, and lay a cognitive-science-rooted groundwork for more coherent and domain-agnostic research investigations in future.
We investigate the fractional Orlicz boundary Hardy-type inequality for bounded Lipschitz domains. Further, we establish fractional Orlicz boundary Hardy-type inequalities with logarithmic corrections for specific critical cases across various domains, such as bounded Lipschitz domains, domains above the graph of a Lipschitz function, and the complement of a bounded Lipschitz domain.
Recently, we showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) L (i.e., ''L-transformers"). However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: the need to synthesize transformers for all of the domains simultaneously blows up the search space. Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this paper, we propose an algorithm to synthesize reduced L-transformers $\langle f_1^{\sharp R}, f_2^{\sharp R},..., f_n^{\sharp R}\rangle$ for a product domain $A_1 \times A_2 \times \ldots \times A_n$ , using multiple DSLs: $\mathcal{L} = \langle \mathcal{L}_1 , \mathcal{L}_2, ... , \mathcal{L}_n \rangle$. Synthesis of reduced-product transformers is quite challenging: first, the synthesis task has to tackle an increased ''feature set" because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other. We implemented our algorithm in a tool, Amurth2, and used it to synthesize abstract transformers for two product domains -- SAFE and JSAI -- available within the SAFEstr framework for JavaScript program analysis. For four of the six operations supported by SAFEstr, Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFEstr.
We present a novel inductive generalization framework for RL from logical specifications. Many interesting tasks in RL environments have a natural inductive structure. These inductive tasks have similar overarching goals but they differ inductively in low-level predicates and distributions. We present a generalization procedure that leverages this inductive relationship to learn a higher-order function, a policy generator, that generates appropriately adapted policies for instances of an inductive task in a zero-shot manner. An evaluation of the proposed approach on a set of challenging control benchmarks demonstrates the promise of our framework in generalizing to unseen policies for long-horizon tasks.
Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting, however, is a manual process that imposes significant burden on the programmer and, hence, there has been limited adoption of this technique. The task of porting not only requires inferring annotations, but may also need refactoring/rewriting of the code to make it amenable to such annotations. In this paper, we use Large Language Models (LLMs) towards addressing both these concerns. We show how to harness LLM capabilities to do complex code reasoning as well as rewriting of large codebases. We also present a novel framework for whole-program transformations that leverages lightweight static analysis to break the transformation into smaller steps that can be carried out effectively by an LLM. We implement our ideas in a tool called MSA that targets the CheckedC dialect. We evaluate MSA on several micro-benchmarks, as well as real-world code ranging up to 20K lines of code. We showcase superior performance compared to a vanilla LLM baseline, as well as demonstrate improvement over a state-of-the-art symbolic (non-LLM) technique.
We establish the weighted fractional Orlicz-Hardy inequalities for various Orlicz functions. Further, we identify the critical cases for each Orlicz function and prove the weighted fractional Orlicz-Hardy inequalities with logarithmic correction. Moreover, we discuss the analogous results in the local case. In the process, for any Orlicz function $\Phi$ and for any $\Lambda>1$, the following inequality is established $$ \Phi(a+b)\leq \lambda\Phi(a)+\frac{C( \Phi, \Lambda )}{(\lambda-1)^{p_\Phi^+-1}}\Phi(b),\;\;\;\forall\,a,b\in [0,\infty),\,\forall\,\lambda\in (1,\Lambda], $$ where $p_\Phi^+:=\sup\big\{t\varphi(t)/\Phi(t):t>0\big\},$ $\varphi$ is the right derivatives of $\Phi$ and $C( \Phi, \Lambda )$ is a positive constant that depends only on $\Phi$ and $\Lambda.$
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.
Let $\Omega$ be an open subset of $\mathbb{R}^N$ with $N\geq 2.$ We identify various classes of Young functions $\Phi$ and $\Psi$, and function spaces for a weight function $g$ so that the following weighted Orlicz-Sobolev inequality holds: \begin{equation*}\label{ineq:Orlicz} \Psi^{-1}\left(\int_{\Omega}|g(x)|\,\Psi(|u(x)| )dx \right)\leq C\Phi^{-1}\left(\int_{\Omega}\Phi(|\nabla u(x)|) dx \right),\;\;\;\forall\,u\in \mathcal{C}^1_c(\Omega), \end{equation*} for some $C>0$. As an application, we study the existence of eigenvalues for certain nonlinear weighted eigenvalue problems.
Quantified Boolean Formulas (QBF) extend propositional logic with quantification $\forall, \exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope. Dependency Quantified Boolean Formulas (DQBF) restrict the dependencies of existentially quantified variables. In DQBF, existentially quantified variables have explicit dependencies on a subset of universally quantified variables called Henkin dependencies. Given a Boolean specification between the set of inputs and outputs, the problem of Henkin synthesis is to synthesize each output variable as a function of its Henkin dependencies such that the specification is met. Henkin synthesis has wide-ranging applications, including verification of partial circuits, controller synthesis, and circuit realizability. This work proposes a data-driven approach for Henkin synthesis called Manthan3. On an extensive evaluation of over 563 instances arising from past DQBF solving competitions, we demonstrate that Manthan3 is competitive with state-of-the-art tools. Furthermore, Manthan3 could synthesize Henkin functions for 26 benchmarks for which none of the state-of-the-art techniques could synthesize.
We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of \emph{probabilistic symbolic variables}, which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the \textsc{KLEE} symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds' algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against \textsc{Psi}, an exact probabilistic symbolic inference engine, and \textsc{Storm}, a probabilistic model checker, and show that our method significantly outperforms both tools.
Attribute grammars allow the association of semantic actions to the production rules in context-free grammars, providing a simple yet effective formalism to define the semantics of a language. However, drafting the semantic actions can be tricky and a large drain on developer time. In this work, we propose a synthesis methodology to automatically infer the semantic actions from a set of examples associating strings to their meanings. We also propose a new coverage metric, derivation coverage. We use it to build a sampler to effectively and automatically draw strings to drive the synthesis engine. We build our ideas into our tool, PANINI, and empirically evaluate it on twelve benchmarks, including a forward differentiation engine, an interpreter over a subset of Java bytecode, and a mini-compiler for C language to two-address code. Our results show that PANINI scales well with the number of actions to be synthesized and the size of the context-free grammar, significantly outperforming simple baselines.
Logic locking "hides" the functionality of a digital circuit to protect it from counterfeiting, piracy, and malicious design modifications. The original design is transformed into a "locked" design such that the circuit reveals its correct functionality only when it is "unlocked" with a secret sequence of bits--the key bit-string. However, strong attacks, especially the SAT attack that uses a SAT solver to recover the key bitstring, have been profoundly effective at breaking the locked circuit and recovering the circuit functionality. We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-order relation, instead of a key of independent values, challenging the attacker to discover this key relation to recreate the circuit functionality. Our technique uses program synthesis to construct the locked design and synthesize a corresponding key relation. HOLL has low overhead and existing attacks for logic locking do not apply as the entity to be recovered is no more a value. To evaluate our proposal, we propose a new attack (SynthAttack) that uses an inductive synthesis algorithm guided by an operational circuit as an input-output oracle to recover the hidden functionality. SynthAttack is inspired by the SAT attack, and similar to the SAT attack, it is verifiably correct, i.e., if the correct functionality is revealed, a verification check guarantees the same. Our empirical analysis shows that SynthAttack can break HOLL for small circuits and small key relations, but it is ineffective for real-life designs.