arXiv subjects

Saikat Chakraborty

Publications and source records attributed to Saikat Chakraborty.

At least 37 records · Page 2Linked to original sources

arXiv2024

A model-independent compact dynamical system formulation for exploring bounce and cyclic cosmological evolutions in $f(R)$ gravity

Using the dynamical systems approach together with the cosmographic parameters, we present a model-independent dynamical system formulation for cosmology in f(R) gravity. The formulation is model-independent in the sense that one needs to specify not a particular functional form of f(R) a-priori, but rather a particular cosmological evolution, which fixes the cosmography. In a sense, our approach is the way around the reconstruction method. This is shown using both non-compact and compact dynamical variables. The focus in this paper is on the compact analysis since we demonstrate the applicability of this formulation using examples of bouncing and cyclic cosmology. In particular, our analysis reveals, in a model-independent manner, the problem of achieving such cosmologies when the universe is globally spatially flat and devoid of matter.

gr-qc↗

arXiv2024

LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation

Large language models (LLMs) have shown great potential in automating significant aspects of coding by producing natural code from informal natural language (NL) intent. However, given NL is informal, it does not lend easily to checking that the generated code correctly satisfies the user intent. In this paper, we propose a novel interactive workflow TiCoder for guided intent clarification (i.e., partial formalization) through tests to support the generation of more accurate code suggestions. Through a mixed methods user study with 15 programmers, we present an empirical evaluation of the effectiveness of the workflow to improve code generation accuracy. We find that participants using the proposed workflow are significantly more likely to correctly evaluate AI generated code, and report significantly less task-induced cognitive load. Furthermore, we test the potential of the workflow at scale with four different state-of-the-art LLMs on two python datasets, using an idealized proxy for a user feedback. We observe an average absolute improvement of 45.97% in the pass@1 code generation accuracy for both datasets and across all LLMs within 5 user interactions, in addition to the automatic generation of accompanying unit tests.

cs.SE↗

arXiv2024

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem producing a definition given a formal specification expressed as an F* type. We provide a program fragment checker that queries F* to check the correctness of candidate solutions. We also report on an extended version of our dataset containing a total of 940K lines of programs and proofs, with a total of 54k top-level F* definitions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate the use of AI to synthesize programs and their proofs in F*, with promising results. Our main finding in that the performance of fine-tuned smaller language models (such as Phi-2 or StarCoder) compare favorably with large language models (such as GPT-4), at a much lower computational cost. We also identify various type-based retrieval augmentation techniques and find that they boost performance significantly. With detailed error analysis and case studies, we identify potential strengths and weaknesses of models and techniques and suggest directions for future improvements.

cs.PL↗

arXiv2024

A model independent approach to the study of structure growth in $f(R)$ gravity

Over the last decade, much attention has been given to the study of modified gravity theories to find a more natural explanation for the late-time acceleration of the Universe. Particular attention has focused on the so-called $f(R)$ dark energy models. Instead of focusing on a particular f(R) model, we present a completely model-independent approach to study the background dynamics and the growth of matter density perturbations for those f(R) models that mimic the $Λ$CDM evolution at the background level. We do this by characterising the dynamics of the gravitational field using a set of dimensionless variables and using cosmography to determine the expansion history. We then illustrate the integrity of this method by fixing the cosmography to be the same as an exact $Λ$CDM model, allowing us to test the solution. We compare the exact evolution of the density contrast and growth index with what one obtains from various levels of the quasi-static approximation, without choosing the form of $f(R)$ dark energy.

gr-qc↗

arXiv2024

A dynamical systems formulation for inhomogeneous LRS-II spacetimes

We present a dynamical system formulation for inhomogeneous LRS-II spacetimes using the covariant 1+1+2 decomposition approach. Our approach describes the LRS-II dynamics from the point of view of a comoving observer. Promoting the covariant radial derivatives of the covariant dynamical quantities to new dynamical variables and utilizing the commutation relation between the covariant temporal and radial derivatives, we were able to construct an autonomous system of first-order ordinary differential equations along with some purely algebraic constraints. Using our dynamical system formulation we found several interesting features in the LRS-II phase space with dust, one of them being that the homogeneous solutions constitute an invariant submanifold. For the particular case of LTB, we were also able to recover the previously known result that an expanding LTB tends to Milne in the absence of a cosmological constant, providing a potential validation of our formalism.

gr-qc↗

arXiv2024

REINFOREST: Reinforcing Semantic Code Similarity for Cross-Lingual Code Search Models

This paper introduces a novel code-to-code search technique that enhances the performance of Large Language Models (LLMs) by including both static and dynamic features as well as utilizing both similar and dissimilar examples during training. We present the first-ever code search method that encodes dynamic runtime information during training without the need to execute either the corpus under search or the search query at inference time and the first code search technique that trains on both positive and negative reference samples. To validate the efficacy of our approach, we perform a set of studies demonstrating the capability of enhanced LLMs to perform cross-language code-to-code search. Our evaluation demonstrates that the effectiveness of our approach is consistent across various model architectures and programming languages. We outperform the state-of-the-art cross-language search tool by up to 44.7\%. Moreover, our ablation studies reveal that even a single positive and negative reference sample in the training process results in substantial performance improvements demonstrating both similar and dissimilar references are important parts of code search. Importantly, we show that enhanced well-crafted, fine-tuned models consistently outperform enhanced larger modern LLMs without fine tuning, even when enhancing the largest available LLMs highlighting the importance for open-sourced models. To ensure the reproducibility and extensibility of our research, we present an open-sourced implementation of our tool and training procedures called REINFOREST.

cs.SE↗

arXiv2024

Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?

Informal natural language that describes code functionality, such as code comments or function documentation, may contain substantial information about a programs intent. However, there is typically no guarantee that a programs implementation and natural language documentation are aligned. In the case of a conflict, leveraging information in code-adjacent natural language has the potential to enhance fault localization, debugging, and code trustworthiness. In practice, however, this information is often underutilized due to the inherent ambiguity of natural language which makes natural language intent challenging to check programmatically. The emergent abilities of Large Language Models (LLMs) have the potential to facilitate the translation of natural language intent to programmatically checkable assertions. However, it is unclear if LLMs can correctly translate informal natural language specifications into formal specifications that match programmer intent. Additionally, it is unclear if such translation could be useful in practice. In this paper, we describe nl2postcond, the problem of leveraging LLMs for transforming informal natural language to formal method postconditions, expressed as program assertions. We introduce and validate metrics to measure and compare different nl2postcond approaches, using the correctness and discriminative power of generated postconditions. We then use qualitative and quantitative methods to assess the quality of nl2postcond postconditions, finding that they are generally correct and able to discriminate incorrect code. Finally, we find that nl2postcond via LLMs has the potential to be helpful in practice; nl2postcond generated postconditions were able to catch 64 real-world historical bugs from Defects4J.

cs.SE↗

arXiv2024

Automated Code Editing with Search-Generate-Modify

Code editing is essential in evolving software development. Many automated code editing tools have been proposed that leverage both Information Retrieval-based techniques and Machine Learning-based code generation and code editing models. Each technique comes with its own promises and perils, and they are often used together to complement their strengths and compensate for their weaknesses. This paper proposes a hybrid approach to better synthesize code edits by leveraging the power of code search, generation, and modification. Our key observation is that a patch obtained by search and retrieval, even if imperfect, can provide helpful guidance to a code generation model. However, a retrieval-guided patch produced by a code generation model can still be a few tokens off from the intended patch. Such generated patches can be slightly modified to create the intended patches. SARGAM is a novel tool designed to mimic a real developer's code editing behavior. Given an original code version, the developer may search for related patches, generate or write the code, and then modify the generated code to adapt it to the right context. Our evaluation of SARGAM on edit generation shows superior performance with respect to current state-of-the-art techniques. SARGAM also shows great effectiveness on automated program repair tasks.

cs.SE↗

arXiv2024

Studying LLM Performance on Closed- and Open-source Data

Large Language models (LLMs) are finding wide use in software engineering practice. These models are extremely data-hungry, and are largely trained on open-source (OSS) code distributed with permissive licenses. In terms of actual use however, a great deal of software development still occurs in the for-profit/proprietary sphere, where the code under development is not, and never has been, in the public domain; thus, many developers, do their work, and use LLMs, in settings where the models may not be as familiar with the code under development. In such settings, do LLMs work as well as they do for OSS code? If not, what are the differences? When performance differs, what are the possible causes, and are there work-arounds? In this paper, we examine this issue using proprietary, closed-source software data from Microsoft, where most proprietary code is in C# and C++. We find that performance for C# changes little from OSS --> proprietary code, but does significantly reduce for C++; we find that this difference is attributable to differences in identifiers. We also find that some performance degradation, in some cases, can be ameliorated efficiently by in-context learning.

cs.SE↗

arXiv2024

Ranking LLM-Generated Loop Invariants for Program Verification

Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}.

cs.PL↗

arXiv2024

Towards Causal Deep Learning for Vulnerability Detection

Deep learning vulnerability detection has shown promising results in recent years. However, an important challenge that still blocks it from being very useful in practice is that the model is not robust under perturbation and it cannot generalize well over the out-of-distribution (OOD) data, e.g., applying a trained model to unseen projects in real world. We hypothesize that this is because the model learned non-robust features, e.g., variable names, that have spurious correlations with labels. When the perturbed and OOD datasets no longer have the same spurious features, the model prediction fails. To address the challenge, in this paper, we introduced causality into deep learning vulnerability detection. Our approach CausalVul consists of two phases. First, we designed novel perturbations to discover spurious features that the model may use to make predictions. Second, we applied the causal learning algorithms, specifically, do-calculus, on top of existing deep learning models to systematically remove the use of spurious features and thus promote causal based prediction. Our results show that CausalVul consistently improved the model accuracy, robustness and OOD performance for all the state-of-the-art models and datasets we experimented. To the best of our knowledge, this is the first work that introduces do calculus based causal learning to software engineering models and shows it's indeed useful for improving the model accuracy, robustness and generalization. Our replication package is located at https://figshare.com/s/0ffda320dcb96c249ef2.

cs.SE↗

arXiv2023

Finding Inductive Loop Invariants using Large Language Models

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.

cs.PL↗

arXiv2023

Interactive Code Generation via Test-Driven User-Intent Formalization

Large language models (LLMs) have shown great potential in automating significant aspects of coding by producing natural code from informal natural language (NL) intent. However, when interacting with LLMs, users have no guarantees that the code suggestions produced correctly satisfy the intent they provided. In fact, it is hard to define a notion of correctness since natural language can be ambiguous and lacks a formal semantics. In this paper, we propose the workflow of {\it interactive test-driven code generation}, which leverages lightweight user feedback to (a) formalize the user intent using generated tests that can be useful for debugging, and (b) produce an improved set of code suggestions by pruning and ranking candidate code suggestions. We describe a language-agnostic abstract algorithm and a concrete implementation TiCoder. We perform an automated evaluation of TiCoder on the \emph{MBPP} and \emph{HumanEval} code generation benchmarks. Our results are promising with using the OpenAI Codex LLM: our best algorithm improves the \passk{1} code generation accuracy (in absolute percentages) between $22.49\%$ to $37.71\%$ for MBPP and between $24.79\%$ to $53.98\%$ for HumanEval using between 1 to 5 simulated user queries.

cs.SE↗

arXiv2023

GrACE: Generation using Associated Code Edits

Developers expend a significant amount of time in editing code for a variety of reasons such as bug fixing or adding new features. Designing effective methods to predict code edits has been an active yet challenging area of research due to the diversity of code edits and the difficulty of capturing the developer intent. In this work, we address these challenges by endowing pre-trained large language models (LLMs) of code with the knowledge of prior, relevant edits. The generative capability of the LLMs helps address the diversity in code changes and conditioning code generation on prior edits helps capture the latent developer intent. We evaluate two well-known LLMs, Codex and CodeT5, in zero-shot and fine-tuning settings respectively. In our experiments with two datasets, the knowledge of prior edits boosts the performance of the LLMs significantly and enables them to generate 29% and 54% more correctly edited code in top-1 suggestions relative to the current state-of-the-art symbolic and neural approaches, respectively.

cs.SE↗

arXiv2023

Observational predictions of inflationary model in spatially covariant gravity with two tensorial degrees of freedom for gravity

We study the inflationary model constructed from a Spatially Covariant Gravity (SCG). The Lagrangian for the SCG in our consideration is expressed as the polynomial of irreducible SCG monomials where the total number of derivatives of each monomial is two, and the theory propagates two tensorial degrees of freedom of gravity up to the first order in cosmological perturbations. The condition for having two tensorial degrees of freedom studied earlier in literature for such theories is derived in vacuum. We extend the condition for having two tensorial degrees of freedom to the case where a scalar field is included by imposing a gauge-fixing. We apply the resulting SCG to describe inflationary universe. The observational predictions such as the scalar spectral index and tensor-to-scalar ratio from this model are investigated. We find that the tensor-to-scalar ratio in this model can either be in the order of unity or be small depending on the parameter of the model.

gr-qc↗

arXiv2023

Global phase space analysis for a class of single scalar field bouncing solutions in general relativity

We carry out a compact phase space analysis of a non-canonical scalar field theory whose Lagrangian is of the form $F(X)-V(ϕ)$ within general relativity. In particular, we focus on a kinetic term of the form $F(X)=βX^m$ with power law potential $V_0 ϕ^n$ and exponential potential $V_0 e^{-λϕ/M_{Pl}}$ of the scalar field. The main aim of this work is to investigate the genericity of nonsingular bounce in these models and to investigate the cosmic future of the bouncing cosmologies when they are generic. A global dynamical system formulation that is particularly suitable for investigating nonsingular bouncing cosmologies is used to carry out the analysis. We show that when $F(X)=βX^m$ ($β<0$), nonsingular bounce is generic for a power law potential $V(ϕ) = V_0 ϕ^n$ only within the parameter range $\left\lbrace \frac{1}{2}<m<1,\,n<\frac{2m}{m-1}\right\rbrace$ and for an exponential potential $V(ϕ) = V_0 e^{-λϕ/M_{Pl}}$ only within the parameter range $\left\lbrace\frac{1}{2}<m\leq1\right\rbrace$. Except in these cases, nonsingular bounce in these models is not generic due to the non-existence of global past or future attractors. Our analysis serves to show the importance of a global phase space analysis to address important questions about nonsingular bouncing solutions, an idea that may and must be adopted for such solutions even in other theories.

gr-qc↗

arXiv2023

Dynamical Analysis of the Dirac-Born-Infeld type of Tachyon field minimally coupled with barotropic fluid using EOS parametrization of a field

In this paper, we present a dynamical system analysis of the tachyon dark energy model by parametrization of the equation of state (EoS) of the dark energy. The choice of parametrization can constrain the form of the field potential, and as a result, the theory can be directly constrained from the observation without assuming a particular form of the potential.

gr-qc↗

arXiv2023

CONCORD: Clone-aware Contrastive Learning for Source Code

Deep Learning (DL) models to analyze source code have shown immense promise during the past few years. More recently, self-supervised pre-training has gained traction for learning generic code representations valuable for many downstream SE tasks, such as clone and bug detection. While previous work successfully learned from different code abstractions (e.g., token, AST, graph), we argue that it is also essential to factor in how developers code day-to-day for general-purpose representation learning. On the one hand, human developers tend to write repetitive programs referencing existing code snippets from the current codebase or online resources (e.g., Stack Overflow website) rather than implementing functions from scratch; such behaviors result in a vast number of code clones. In contrast, a deviant clone by mistake might trigger malicious program behaviors. Thus, as a proxy to incorporate developers' coding behavior into the pre-training scheme, we propose to include code clones and their deviants. In particular, we propose CONCORD, a self-supervised, contrastive learning strategy to place benign clones closer in the representation space while moving deviants further apart. We show that CONCORD's clone-aware contrastive learning drastically reduces the need for expensive pre-training resources while improving the performance of downstream SE tasks. We also empirically demonstrate that CONCORD can improve existing pre-trained models to learn better representations that consequently become more efficient in both identifying semantically equivalent programs and differentiating buggy from non-buggy code.

cs.SE↗