arXiv subjects

Supratik Chakraborty

Publications and source records attributed to Supratik Chakraborty.

At least 19 recordsLinked to original sources

arXiv2026

Latent Performance Profiling of Large Language Models

Large language models (LLMs) frequently achieve impressive scores on standardized benchmarks, yet accuracy alone offers a limited view of their capabilities. Evaluating open-source LLMs through leaderboards faces persistent issues like data contamination, narrow task scope, and weak alignment with real-world reliability. Benchmark-based evaluations such as MMLU PRO, BBH, or IFEval primarily capture what a model outputs on fixed test sets, not how it processes information, calibrates uncertainty, or structures internal knowledge. In this article, we advocate for a shift from benchmark-centric evaluation toward a complementary, state-centered intrinsic assessment of LLMs. To this end, we introduce Latent Performance Profiling (LPP) -- a framework that derives task-agnostic diagnostics from hidden activations and output distributions. LPP defines a set of scalar metrics on a model's latent representations and dynamics, revealing scale-independent traits that enable interpretable comparisons and uncover hidden vulnerabilities. Unlike static accuracy scores, LPP provides stable, architecture-sensitive signatures across models of similar size. With extensive empirical analyses across eight LLMs, spanning a size range of 0.5B-14B, we demonstrate that models with similar benchmark scores can exhibit contrasting latent profiles, such as differences in entropy or adaptability. Guided by these insights, we design synthetic probes for uncertainty and symbolic reasoning that align with intrinsic metrics while decoupling from leaderboard bias. We recommend that reporting LPP alongside benchmarks provides a deeper, interpretable understanding of model behavior, enabling more reliable model selection, safety assessment, and evaluation beyond surface-level accuracy.

cs.CL↗

arXiv2026

Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

We study the problem of synthesizing programs from nonlinear real arithmetic (NRA) specifications. Existing techniques, such as syntax-guided synthesis (SyGuS), fail to synthesize programs when the specification is unrealizable. We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary NRA specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to work on rational inputs and outputs. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by SyGuS for NRA (real inputs and outputs) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications. We have implemented our approach in a prototype tool called NQSynth that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specifications realizable.

cs.PL↗

arXiv2026

On-the-fly LTLf Synthesis under Partial Observability

LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset construction that universally quantifies these variables. Existing approaches perform this construction as a separate step prior to game solving, often generating belief states that are unnecessary in practice. We propose an on-the-fly approach to LTLf synthesis under partial observability based on observable progression. Our method incrementally builds the belief-state DFA by progressing the specification with respect to observable variables only, universally quantifying unobservable variables on the fly. We prove the correctness of the construction and show that it naturally enables on-the-fly game solving, leading to a fully on-the-fly synthesis framework. Our implementation leverages DFAs represented using Multi-Terminal Binary Decision Diagrams: a compact representation that has proven highly effective for LTLf synthesis under full observability. Experimental results demonstrate that our approach significantly outperforms existing methods and further highlight the practical benefits of integrating on-the-fly game solving with belief-state construction.

cs.LO↗

arXiv2026

Knowledge Compilation for Quantification in Alternating Automata

We present a knowledge compilation approach for existential and universal quantification in alternating automata. Knowledge compilation transforms formulas into normal forms with special properties that enable efficient answering of questions of interest. For Boolean formulas, several normal forms that have proven effective for existential/universal quantification, and even for functional synthesis, have been studied in the literature. For infinite word automata, quantification is a fundamental operation in verification tasks such as QPTL satisfiability checking and HyperLTL model checking. Existing algorithms rely on nondeterministic infinite word automata, where existential projection can be efficiently performed state-wise, but universal projection requires complementation. Complementing nondeterministic infinite word automata, however, is expensive in practice, making existing algorithms infeasible for automata in practice. Towards addressing this problem, we propose novel knowledge compilation techniques for existential and universal quantification on alternating safety automata. Our approach compiles alternating automata into normal forms where projection can be applied uniformly and efficiently to each state's transition function. Using the compilations for each type of quantification, we can effectively eliminate a sequence of alternating quantifiers in formulas without complementation. Our BDD-based prototype demonstrates the practical effectiveness of our algorithms on a suite of QPTL satisfiability benchmarks.

cs.LO↗

arXiv2025

On Robustness of Linear Classifiers to Targeted Data Poisoning

Data poisoning is a training-time attack that undermines the trustworthiness of learned models. In a targeted data poisoning attack, an adversary manipulates the training dataset to alter the classification of a targeted test point. Given the typically large size of training dataset, manual detection of poisoning is difficult. An alternative is to automatically measure a dataset's robustness against such an attack, which is the focus of this paper. We consider a threat model wherein an adversary can only perturb the labels of the training dataset, with knowledge limited to the hypothesis space of the victim's model. In this setting, we prove that finding the robustness is an NP-Complete problem, even when hypotheses are linear classifiers. To overcome this, we present a technique that finds lower and upper bounds of robustness. Our implementation of the technique computes these bounds efficiently in practice for many publicly available datasets. We experimentally demonstrate the effectiveness of our approach. Specifically, a poisoning exceeding the identified robustness bounds significantly impacts test point classification. We are also able to compute these bounds in many more cases where state-of-the-art techniques fail.

cs.LG↗

arXiv2025

Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models

Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: accuracy and explainability. Exploring the trade-off between these objectives is essential for developing trustworthy interpretations. While many techniques for multi-objective interpretation synthesis have been developed, they typically lack formal guarantees on the Pareto-optimality of the results. Methods that do provide such guarantees, on the other hand, often face severe scalability limitations when exploring the Pareto-optimal space. To address this, we develop a framework based on local optimality guarantees that enables more scalable synthesis of interpretations. Specifically, we consider the problem of synthesizing a set of Pareto-optimal interpretations with local optimality guarantees, within the immediate neighborhood of each solution. Our approach begins with a multi-objective learning or search technique, such as Multi-Objective Monte Carlo Tree Search, to generate a best-effort set of Pareto-optimal candidates with respect to accuracy and explainability. We then verify local optimality for each candidate as a Boolean satisfiability problem, which we solve using a SAT solver. We demonstrate the efficacy of our approach on a set of benchmarks, comparing it against previous methods for exploring the Pareto-optimal front of interpretations. In particular, we show that our approach yields interpretations that closely match those synthesized by methods offering global guarantees.

cs.LG↗

arXiv2025

Presburger Functional Synthesis: Complexity and Tractable Normal Forms

Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this paper, we launch an investigation of this problem for the theory of Presburger Arithmetic, that we call Presburger Functional Synthesis (PFnS). We show that PFnS can be solved in EXPTIME and provide a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Further, we show that PFnS for one input and one output variable is as hard as BFnS in general. We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS. We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF. Finally, we identify a syntactic normal form that is easier to check but is exponentially less succinct than PSyNF.

cs.LO↗

arXiv2025

Counting Answer Sets of Disjunctive Answer Set Programs

Answer Set Programming (ASP) provides a powerful declarative paradigm for knowledge representation and reasoning. Recently, counting answer sets has emerged as an important computational problem with applications in probabilistic reasoning, network reliability analysis, and other domains. This has motivated significant research into designing efficient ASP counters. While substantial progress has been made for normal logic programs, the development of practical counters for disjunctive logic programs remains challenging. We present SharpASP-SR, a novel framework for counting answer sets of disjunctive logic programs based on subtractive reduction to projected propositional model counting. Our approach introduces an alternative characterization of answer sets that enables efficient reduction while ensuring that intermediate representations remain of polynomial size. This allows SharpASP-SR to leverage recent advances in projected model counting technology. Through extensive experimental evaluation on diverse benchmarks, we demonstrate that SharpASP-SR significantly outperforms existing counters on instances with large answer set counts. Building on these results, we develop a hybrid counting approach that combines enumeration techniques with SharpASP-SR to achieve state-of-the-art performance across the full spectrum of disjunctive programs.

cs.LO↗

arXiv2024

A shallow dive into the depths of non-termination checking for C programs

Checking for Non-Termination (NT) of a given program P, i.e., determining if P has at least one non-terminating run, is an undecidable problem that continues to garner significant research attention. While unintended NT is common in real-world software development, even the best-performing tools for NT checking are often ineffective on real-world programs and sometimes incorrect due to unrealistic assumptions such as absence of overflows. To address this, we propose a sound and efficient technique for NT checking that is also effective on realworld software. Given P, we encode the NT property as an assertion inside each loop of P to check for recurrent states in that loop, up to a fixed unwinding depth, using a Bounded Model Checker. The unwinding depth is increased iteratively until either NT is found or a predefined limit is reached. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers

cs.SE↗

arXiv2024

Network Inversion of Binarised Neural Nets

While the deployment of neural networks, yielding impressive results, becomes more prevalent in various applications, their interpretability and understanding remain a critical challenge. Network inversion, a technique that aims to reconstruct the input space from the model's learned internal representations, plays a pivotal role in unraveling the black-box nature of input to output mappings in neural networks. In safety-critical scenarios, where model outputs may influence pivotal decisions, the integrity of the corresponding input space is paramount, necessitating the elimination of any extraneous "garbage" to ensure the trustworthiness of the network. Binarised Neural Networks (BNNs), characterized by binary weights and activations, offer computational efficiency and reduced memory requirements, making them suitable for resource-constrained environments. This paper introduces a novel approach to invert a trained BNN by encoding it into a CNF formula that captures the network's structure, allowing for both inference and inversion.

cs.LG↗

arXiv2024

On Dependent Variables in Reactive Synthesis

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis.

cs.LO↗

arXiv2023

Exact ASP Counting with Compact Encodings

Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from diverse domains in a natural way. Building on advances in propositional SAT solving, the past two decades have witnessed the emergence of well-engineered systems for solving the answer set satisfiability problem, i.e., finding models or answer sets for a given answer set program. In recent years, there has been growing interest in problems beyond satisfiability, such as model counting, in the context of ASP. Akin to the early days of propositional model counting, state-of-the-art exact answer set counters do not scale well beyond small instances. Exact ASP counters struggle with handling larger input formulas. The primary contribution of this paper is a new ASP counting framework, called sharpASP, which counts answer sets avoiding larger input formulas. This relies on an alternative way of defining answer sets that allows for the lifting of key techniques developed in the context of propositional model counting. Our extensive empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters. Specifically, by using sharpASP, we were able to solve 1062 benchmarks with PAR2 score of 3082 whereas using prior state-of-the-art, we could only solve 895 benchmarks with a PAR2 score of 4205, all other experimental conditions being the same.

cs.LO↗

arXiv2023

Auditable Algorithms for Approximate Model Counting

Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, developing algorithms for approximate counting is an important research area. Building on the practical success of SAT-solvers, the focus has recently shifted from theory to practical implementations of approximate counting algorithms. This has brought to focus new challenges, such as the design of auditable approximate counters that not only provide an approximation of the model count, but also a certificate that a verifier with limited computational power can use to check if the count is indeed within the promised bounds of approximation. Towards generating certificates, we start by examining the best-known deterministic approximate counting algorithm that uses polynomially many calls to a $Σ_2^P$ oracle. We show that this can be audited via a $Σ_2^P$ oracle with the query constructed over $n^2 \log^2 n$ variables, where the original formula has $n$ variables. Since $n$ is often large, we ask if the count of variables in the certificate can be reduced -- a crucial question for potential implementation. We show that this is indeed possible with a tradeoff in the counting algorithm's complexity. Specifically, we develop new deterministic approximate counting algorithms that invoke a $Σ_3^P$ oracle, but can be certified using a $Σ_2^P$ oracle using certificates on far fewer variables: our final algorithm uses only $n \log n$ variables. Our study demonstrates that one can simplify auditing significantly if we allow the counting algorithm to access a slightly more powerful oracle. This shows for the first time how audit complexity can be traded for complexity of approximate counting.

cs.LO↗

arXiv2022

Full-Program Induction: Verifying Array Programs sans Loop Invariants

Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size $N$. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter $N$. The technique performs non-trivial transformations of the given program and pre-conditions during the inductive step. The transformations assist in effectively reducing the assertion checking problem by transforming a program with multiple loops to a program which has fewer and simpler loops or is loop-free. Significantly, full-program induction does not require generation or use of loop-specific invariants. To assess the efficacy of our technique, we have developed a prototype tool called Vajra. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a large set of array manipulating benchmarks from the international software verification competition (SV-COMP) and on several programs inspired by algebraic functions that perform polynomial computations.

cs.PL↗

arXiv2022

On synthesizing Skolem functions for first order logic formulae

Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).

cs.LO↗

arXiv2022

On eventual non-negativity and positivity for the weighted sum of powers of matrices

The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w_1 , A_1 ), . . . , (w_m , A_m )}, we ask if the weighted sum of powers of these matrices is eventually non-negative P (resp. n positive), i.e., does there exist an integer N s.t for all n greater than N , (w_1 A_1^n + ... + w_m A_m^n) is atmost 0 (resp. greater than 0). The restricted setting when m = w_1 = 1, results in so-called eventually non-negative (or eventually positive) matrices, which enjoy nice spectral properties and have been well-studied in control theory. More applications arise in varied contexts, ranging from program verification to partially observable and multi-modal systems. Our goal is to investigate this problem and its link to linear recurrence sequences. Our first result is that for m at least 2, the problem is as hard as the ultimate positivity of linear recurrences, a long standing open question (known to be coNP-hard). Our second result is a reduction in the other direction showing that for any m at least 1, the problem reduces to ultimate positivity of linear recurrences. This shows precise upper bounds for several subclasses of matrices by exploiting known results on linear recurrence sequences. Our third main result is a novel reduction technique for a large class of problems (including those mentioned above) over rational diagonalizable matrices to the corresponding problem over simple real-algebraic matrices. This yields effective decision procedures for diagonalizable matrices.

cs.FL↗

arXiv2021

Projected Model Counting: Beyond Independent Support

The past decade has witnessed a surge of interest in practical techniques for projected model counting. Despite significant advancements, however, performance scaling remains the Achilles' heel of this field. A key idea used in modern counters is to count models projected on an \emph{independent support} that is often a small subset of the projection set, i.e. original set of variables on which we wanted to project. While this idea has been effective in scaling performance, the question of whether it can benefit to count models projected on variables beyond the projection set, has not been explored. In this paper, we study this question and show that contrary to intuition, it can be beneficial to project on variables beyond the projection set. In applications such as verification of binarized neural networks, quantification of information flow, reliability of power grids etc., a good upper bound of the projected model count often suffices. We show that in several such cases, we can identify a set of variables, called upper bound support (UBS), that is not necessarily a subset of the projection set, and yet counting models projected on UBS guarantees an upper bound of the true projected model count. Theoretically, a UBS can be exponentially smaller than the smallest independent support. Our experiments show that even otherwise, UBS-based projected counting can be more efficient than independent support-based projected counting, while yielding bounds of very high quality. Based on extensive experiments, we find that UBS-based projected counting can solve many problem instances that are beyond the reach of a state-of-the-art independent support-based projected model counter.

cs.AI↗

arXiv2021

Synthesizing Pareto-Optimal Interpretations for Black-Box Models

We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-understandable interpretations for black-box models often requires balancing conflicting objectives. A simple interpretation may be easier to understand for humans while being less precise in its predictions vis-a-vis a complex interpretation. Existing methods for synthesizing interpretations use a single objective function and are often optimized for a single class of interpretations. In contrast, we provide a more general and multi-objective synthesis framework that allows users to choose (1) the class of syntactic templates from which an interpretation should be synthesized, and (2) quantitative measures on both the correctness and explainability of an interpretation. For a given black-box, our approach yields a set of Pareto-optimal interpretations with respect to the correctness and explainability measures. We show that the underlying multi-objective optimization problem can be solved via a reduction to quantitative constraint solving, such as weighted maximum satisfiability. To demonstrate the benefits of our approach, we have applied it to synthesize interpretations for black-box neural-network classifiers. Our experiments show that there often exists a rich and varied set of choices for interpretations that are missed by existing approaches.

cs.LG↗