arXiv subjects

Andrei Popescu

Publications and source records attributed to Andrei Popescu.

At least 19 recordsLinked to original sources

arXiv2026

Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints

Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic $\lambda$-calculus terms, as used in Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle/HOL. Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an LLM-powered AI agent independently produce pen-and-paper proofs, and the AI agent autoformalizes both in Isabelle, with further human-hinted AI interventions refining and generalizing the development.

cs.LO↗

arXiv2024

Advancing Algorithmic Approaches to Probabilistic Argumentation under the Constellation Approach

Reasoning with defeasible and conflicting knowledge in an argumentative form is a key research field in computational argumentation. Reasoning under various forms of uncertainty is both a key feature and a challenging barrier for automated argumentative reasoning. It was shown that argumentative reasoning using probabilities faces in general high computational complexity, in particular for the so-called constellation approach. In this paper, we develop an algorithmic approach to overcome this obstacle. We refine existing complexity results and show that two main reasoning tasks, that of computing the probability of a given set being an extension and an argument being acceptable, diverge in their complexity: the former is #P-complete and the latter is #-dot-NP-complete when considering their underlying counting problems. We present an algorithm for the complex task of computing the probability of a set of arguments being a complete extension by using dynamic programming operating on tree-decompositions. An experimental evaluation shows promise of our approach.

cs.AI↗

arXiv2024

Pegasus-v1 Technical Report

This technical report introduces Pegasus-1, a multimodal language model specialized in video content understanding and interaction through natural language. Pegasus-1 is designed to address the unique challenges posed by video data, such as interpreting spatiotemporal information, to offer nuanced video content comprehension across various lengths. This technical report overviews Pegasus-1's architecture, training strategies, and its performance in benchmarks on video conversation, zero-shot video question answering, and video summarization. We also explore qualitative characteristics of Pegasus-1 , demonstrating its capabilities as well as its limitations, in order to provide readers a balanced view of its current state and its future direction.

cs.MM↗

arXiv2023

HighTEA: High energy Theory Event Analyser

We introduce HighTEA, a new paradigm for deploying fully-differential next-to-next-to leading order (NNLO) calculations for collider observables. In principle, any infrared safe observable can be computed and, with very few restrictions, the user has complete freedom in defining their calculation's setup. For example, one can compute generic n-dimensional distributions, can define kinematic variables and factorization/renormalization scales, and can modify the strong coupling and parton distributions. HighTEA operates on the principle of analyzing precomputed events. It has all the required hardware and software infrastructure such that users only need to request their calculation via the internet before receiving the results, typically within minutes, in the form of a histogram. No specialized knowledge or computing infrastructure is required to fully utilize HighTEA, which could be used by both experts in particle physics and the general public. The current focus is on all classes of LHC processes. Extensions beyond NNLO, or to $e^+e^-$ colliders, are natural next steps.

hep-ph↗

arXiv2023

Nominal Recursors as Epi-Recursors: Extended Technical Report

We study nominal recursors from the literature on syntax with bindings and compare them with respect to expressiveness. The term "nominal" refers to the fact that these recursors operate on a syntax representation where the names of bound variables appear explicitly, as in nominal logic. We argue that nominal recursors can be viewed as epi-recursors, a concept that captures abstractly the distinction between the constructors on which one actually recurses, and other operators and properties that further underpin recursion.We develop an abstract framework for comparing epi-recursors and instantiate it to the existing nominal recursors, and also to several recursors obtained from them by cross-pollination. The resulted expressiveness hierarchies depend on how strictly we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax. We also apply our methodology to produce an expressiveness hierarchy of nominal corecursors, which are principles for defining functions targeting infinitary non-well-founded terms (which underlie lambda-calculus semantics concepts such as B\"ohm trees). Our results are validated with the Isabelle/HOL theorem prover.

cs.LO↗

arXiv2022

Flavour anti-$k_\text{T}$ algorithm applied to $Wb\bar{b}$ production at the LHC

We apply the recently proposed flavoured anti-$k_{\text{T}}$ jet algorithm to $Wb\bar{b}$ production at the Large Hadron Collider at $\sqrt{s}=8$ TeV. We present results for the total cross section and differential distributions at the next-to-next-to-leading order (NNLO) in QCD. We discuss the effects of the remaining parametric freedom in the flavoured anti-$k_{\text{T}}$ prescription, and compare it against the standard flavour-$k_{\text{T}}$ algorithm. We compare the total cross section results against the CMS data, finding good agreement. The NNLO QCD corrections are significant, and their inclusion substantially improves the agreement with the data.

hep-ph↗

arXiv2022

Rensets and Renaming-Based Recursion for Syntax with Bindings

I introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitution) on syntax with bindings. Rensets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, renaming is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, rensets yield a truly minimalistic characterization of lambda-calculus terms as an abstract datatype -- one involving a recursively enumerable set of unconditional equations, referring only to the most fundamental term operators: the constructors and renaming. This characterization yields a recursion principle, which (similarly to the case of nominal sets) can be improved by incorporating Barendregt's variable convention. When interpreting syntax in semantic domains, my renaming-based recursor is easier to deploy than the nominal recursor. My results have been validated with the proof assistant Isabelle/HOL.

cs.LO↗

arXiv2022

NNLO QCD corrections to $Wb\bar{b}$ production at the LHC

We compute theoretical predictions for the production of a W-boson in association with a bottom-quark pair at hadron colliders at next-to-next-to-leading order (NNLO) in QCD, including the leptonic decay of the W-boson, while treating the bottom quark as massless. This calculation constitutes the very first $2 \to 3$ process with a massive external particle to be studied at such a perturbative order. We derive an analytic expression for the required two-loop five-particle amplitudes in the leading colour approximation employing finite-field methods. Numerical results for the cross section and differential distributions are presented for the Large Hadron Collider at $\sqrt{s} = 8$ TeV. We observe an improvement of the perturbative convergence for the inclusive case and for the prediction with a jet veto upon the inclusion of the NNLO QCD corrections.

hep-ph↗

arXiv2022

Angular coefficients in W+j production at the LHC with high precision

The extraction of the W-boson mass, a fundamental parameter of the Standard Model, from hadron-hadron collision requires precise theory predictions. In this regard, angular coefficients are crucial to model the dynamics of W-boson production. In this work, we provide, for the first time, angular coefficients at NNLO QCD + NLO EW accuracy for finite transverse momentum W-boson at the LHC. The corrections can reach up to 10% in certain regions of phase space. They are accompanied by a significant reduction of the scale uncertainty. This work should, besides providing reference values for theory-data comparison, provide state-of-the-art theory input for W-boson mass measurements.

hep-ph↗

arXiv2021

Polarised W+j production at the LHC: a study at NNLO QCD accuracy

We study polarisation of W-bosons produced in association with one jet at the LHC. In particular, we provide all necessary theoretical ingredients for the precise extraction of polarisation fractions. To that end, we present new polarised predictions up to NNLO QCD accuracy employing the narrow-width approximation, in two phase spaces: inclusive and fiducial. We compare results in the fiducial phase space to a full off-shell computation as well as experimental data. Finally, we fit the polarisation fractions using shape templates and show that NNLO corrections significantly improve their determination.

hep-ph↗

arXiv2021

Configuring Multiple Instances with Multi-Configuration

Configuration is a successful application area of Artificial Intelligence. In the majority of the cases, configuration systems focus on configuring one solution (configuration) that satisfies the preferences of a single user or a group of users. In this paper, we introduce a new configuration approach - multi-configuration - that focuses on scenarios where the outcome of a configuration process is a set of configurations. Example applications thereof are the configuration of personalized exams for individual students, the configuration of project teams, reviewer-to-paper assignment, and hotel room assignments including individualized city trips for tourist groups. For multi-configuration scenarios, we exemplify a constraint satisfaction problem representation in the context of configuring exams. The paper is concluded with a discussion of open issues for future work.

cs.AI↗

arXiv2021

Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS

We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to several fundamental constructions and results: sound semantic interpretation, the Church-Rosser and standardization theorems, and higher-order abstract syntax (HOAS) encoding. For Church-Rosser and standardization, our work covers both the call-by-name and call-by-value versions of the calculus, following classic papers by Takahashi and Plotkin. During the formalization, we were able to stay focused on the high-level ideas of the development -- thanks to the arsenal provided by our general theory: a wealth of basic facts about the substitution, swapping and freshness operators, as well as recursive-definition and reasoning principles, including a specialization to semantic interpretation of syntax.

cs.LO↗

arXiv2021

NNLO QCD study of polarised $W^+ W^-$ production at the LHC

Longitudinal polarisation of the weak bosons is a direct consequence of Electroweak symmetry breaking mechanism providing an insight into its nature, and is instrumental in searches for physics beyond the Standard Model. We perform a polarisation study of the diboson production in the $p p \to e^+ν_eμ^-\barν_μ$ process at NNLO QCD in the fiducial setup inspired by experimental measurements at ATLAS. This is the first polarisation study at NNLO. We employ the double-pole approximation framework for the polarised calculation, and investigate NNLO effects arising in differential distributions.

hep-ph↗

arXiv2021

An Overview of Recommender Systems and Machine Learning in Feature Modeling and Configuration

Recommender systems support decisions in various domains ranging from simple items such as books and movies to more complex items such as financial services, telecommunication equipment, and software systems. In this context, recommendations are determined, for example, on the basis of analyzing the preferences of similar users. In contrast to simple items which can be enumerated in an item catalog, complex items have to be represented on the basis of variability models (e.g., feature models) since a complete enumeration of all possible configurations is infeasible and would trigger significant performance issues. In this paper, we give an overview of a potential new line of research which is related to the application of recommender systems and machine learning techniques in feature modeling and configuration. In this context, we give examples of the application of recommender systems and machine learning and discuss future research issues.

cs.IR↗

arXiv2017

The fate of small classically stable Q-balls

The smallest classically stable Q-balls are, in fact, generically metastable: in quantum theory they decay into free particles via collective tunneling. We derive general semiclassical method to calculate the rate of this process in the entire kinematical region of Q-ball metastability. Our method uses Euclidean field-theoretical solutions resembling the Coleman's bounce and fluctuations around them. As an application of the method, we numerically compute the decay rate to the leading semiclassical order in a particular one-field model. We shortly discuss cosmological implications of metastable Q-balls.

hep-ph↗

arXiv2017

A Formalized General Theory of Syntax with Bindings

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying numbers of inputs, quotiented to alpha-equivalence and sorted according to a binding signature. The theory includes a rich collection of properties of the standard operators on terms, such as substitution and freshness. It also includes induction and recursion principles and support for semantic interpretation, all tailored for smooth interaction with the bindings and the standard operators.

cs.LO↗

arXiv2016

Encoding Monomorphic and Polymorphic Types

Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.

cs.LO↗

arXiv2015

Foundational Extensible Corecursion

This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.

cs.PL↗