-
The Proof Analysis Problem
Authors:
Noel Arteche,
Albert Atserias,
Susanna F. de Rezende,
Erfan Khaniki
Abstract:
Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$, stating "$\varphi$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of…
▽ More
Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$, stating "$\varphi$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{Ref}(\varphi)$ given a satisfying assignment of $\varphi$. A question that remained open is: do all short Resolution refutations of $\operatorname{Ref}(\varphi)$ explicitly leak a satisfying assignment of $\varphi$?
We answer this question affirmatively by giving a polynomial-time algorithm that extracts a satisfying assignment for $\varphi$ given any short Resolution refutation of $\operatorname{Ref}(\varphi)$. The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook's theory $\mathsf{PV_1}$ of bounded arithmetic.
Motivated by this, we introduce a computational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a proof system $Q$, the Proof Analysis Problem for $Q$ asks, given a CNF formula $\varphi$ and a $Q$-proof of a Resolution lower bound for $\varphi$, encoded as $\neg \operatorname{Ref}(\varphi)$, whether $\varphi$ is satisfiable. In contrast to PAP for Resolution, we prove that PAP for Extended Frege (EF) is NP-complete.
Our results yield new insights into proof complexity: (i) every proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas stating Resolution lower bounds; (ii) we provide Ref formulas exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic $T$ we construct unsatisfiable CNF formulas exponentially hard for Resolution but for which $T$ cannot prove even a quadratic lower bound.
△ Less
Submitted 20 June, 2025;
originally announced June 2025.
-
RANa: Retrieval-Augmented Navigation
Authors:
Gianluca Monaci,
Rafael S. Rezende,
Romain Deffayet,
Gabriela Csurka,
Guillaume Bono,
Hervé Déjean,
Stéphane Clinchant,
Christian Wolf
Abstract:
Methods for navigation based on large-scale learning typically treat each episode as a new problem, where the agent is spawned with a clean memory in an unknown environment. While these generalization capabilities to an unknown environment are extremely important, we claim that, in a realistic setting, an agent should have the capacity of exploiting information collected during earlier robot opera…
▽ More
Methods for navigation based on large-scale learning typically treat each episode as a new problem, where the agent is spawned with a clean memory in an unknown environment. While these generalization capabilities to an unknown environment are extremely important, we claim that, in a realistic setting, an agent should have the capacity of exploiting information collected during earlier robot operations. We address this by introducing a new retrieval-augmented agent, trained with RL, capable of querying a database collected from previous episodes in the same environment and learning how to integrate this additional context information. We introduce a unique agent architecture for the general navigation task, evaluated on ImageNav, Instance-ImageNav and ObjectNav. Our retrieval and context encoding methods are data-driven and employ vision foundation models (FM) for both semantic and geometric understanding. We propose new benchmarks for these settings and we show that retrieval allows zero-shot transfer across tasks and environments while significantly improving performance.
△ Less
Submitted 29 July, 2025; v1 submitted 4 April, 2025;
originally announced April 2025.
-
Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
Authors:
Jonas Conneryd,
Susanna F. de Rezende,
Jakob Nordström,
Shuo Pang,
Kilian Risse
Abstract:
We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse Erdős-Rényi random graphs, are $3$-colourable. Using the known relation between size and degree for polynomial calculus proofs, this implies strongly exponential lower bounds on proof size.
We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse Erdős-Rényi random graphs, are $3$-colourable. Using the known relation between size and degree for polynomial calculus proofs, this implies strongly exponential lower bounds on proof size.
△ Less
Submitted 21 March, 2025;
originally announced March 2025.
-
Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman
Authors:
Susanna F. de Rezende,
Noah Fleming,
Duri Andrea Janett,
Jakob Nordström,
Shuo Pang
Abstract:
We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and res…
▽ More
We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and resolution that are truly supercritical, i.e., in terms of formula size rather than number of variables, and we also show supercritical trade-offs between width and size for treelike resolution. Our results build on a new supercritical width-depth trade-off for resolution, obtained by refining and strengthening the compression scheme for the Cop-Robber game in [Grohe, Lichter, Neuen & Schweitzer 2023]. This yields robust supercritical trade-offs for dimension versus iteration number in the Weisfeiler-Leman algorithm, which also translate into trade-offs between number of variables and quantifier depth in first-order logic. Our other results follow from improved lifting theorems that might be of independent interest.
△ Less
Submitted 21 November, 2024;
originally announced November 2024.
-
Clique Is Hard on Average for Sherali-Adams with Bounded Coefficients
Authors:
Susanna F. de Rezende,
Aaron Potechin,
Kilian Risse
Abstract:
We prove that Sherali-Adams with polynomially bounded coefficients requires proofs of size $n^{Ω(d)}$ to rule out the existence of an $n^{Θ(1)}$-clique in Erdős-Rényi random graphs whose maximum clique is of size $d\leq 2\log n$. This lower bound is tight up to the multiplicative constant in the exponent. We obtain this result by introducing a technique inspired by pseudo-calibration which may be…
▽ More
We prove that Sherali-Adams with polynomially bounded coefficients requires proofs of size $n^{Ω(d)}$ to rule out the existence of an $n^{Θ(1)}$-clique in Erdős-Rényi random graphs whose maximum clique is of size $d\leq 2\log n$. This lower bound is tight up to the multiplicative constant in the exponent. We obtain this result by introducing a technique inspired by pseudo-calibration which may be of independent interest. The technique involves defining a measure on monomials that precisely captures the contribution of a monomial to a refutation. This measure intuitively captures progress and should have further applications in proof complexity.
△ Less
Submitted 25 April, 2024;
originally announced April 2024.
-
Weatherproofing Retrieval for Localization with Generative AI and Geometric Consistency
Authors:
Yannis Kalantidis,
Mert Bülent Sarıyıldız,
Rafael S. Rezende,
Philippe Weinzaepfel,
Diane Larlus,
Gabriela Csurka
Abstract:
State-of-the-art visual localization approaches generally rely on a first image retrieval step whose role is crucial. Yet, retrieval often struggles when facing varying conditions, due to e.g. weather or time of day, with dramatic consequences on the visual localization accuracy. In this paper, we improve this retrieval step and tailor it to the final localization task. Among the several changes w…
▽ More
State-of-the-art visual localization approaches generally rely on a first image retrieval step whose role is crucial. Yet, retrieval often struggles when facing varying conditions, due to e.g. weather or time of day, with dramatic consequences on the visual localization accuracy. In this paper, we improve this retrieval step and tailor it to the final localization task. Among the several changes we advocate for, we propose to synthesize variants of the training set images, obtained from generative text-to-image models, in order to automatically expand the training set towards a number of nameable variations that particularly hurt visual localization. After expanding the training set, we propose a training approach that leverages the specificities and the underlying geometry of this mix of real and synthetic images. We experimentally show that those changes translate into large improvements for the most challenging visual localization datasets. Project page: https://europe.naverlabs.com/ret4loc
△ Less
Submitted 14 February, 2024;
originally announced February 2024.
-
AToMiC: An Image/Text Retrieval Test Collection to Support Multimedia Content Creation
Authors:
Jheng-Hong Yang,
Carlos Lassance,
Rafael Sampaio de Rezende,
Krishna Srinivasan,
Miriam Redi,
Stéphane Clinchant,
Jimmy Lin
Abstract:
This paper presents the AToMiC (Authoring Tools for Multimedia Content) dataset, designed to advance research in image/text cross-modal retrieval. While vision-language pretrained transformers have led to significant improvements in retrieval effectiveness, existing research has relied on image-caption datasets that feature only simplistic image-text relationships and underspecified user models of…
▽ More
This paper presents the AToMiC (Authoring Tools for Multimedia Content) dataset, designed to advance research in image/text cross-modal retrieval. While vision-language pretrained transformers have led to significant improvements in retrieval effectiveness, existing research has relied on image-caption datasets that feature only simplistic image-text relationships and underspecified user models of retrieval tasks. To address the gap between these oversimplified settings and real-world applications for multimedia content creation, we introduce a new approach for building retrieval test collections. We leverage hierarchical structures and diverse domains of texts, styles, and types of images, as well as large-scale image-document associations embedded in Wikipedia. We formulate two tasks based on a realistic user model and validate our dataset through retrieval experiments using baseline models. AToMiC offers a testbed for scalable, diverse, and reproducible multimedia retrieval research. Finally, the dataset provides the basis for a dedicated track at the 2023 Text Retrieval Conference (TREC), and is publicly available at https://github.com/TREC-AToMiC/AToMiC.
△ Less
Submitted 4 April, 2023;
originally announced April 2023.
-
ARTEMIS: Attention-based Retrieval with Text-Explicit Matching and Implicit Similarity
Authors:
Ginger Delmas,
Rafael Sampaio de Rezende,
Gabriela Csurka,
Diane Larlus
Abstract:
An intuitive way to search for images is to use queries composed of an example image and a complementary text. While the first provides rich and implicit context for the search, the latter explicitly calls for new traits, or specifies how some elements of the example image should be changed to retrieve the desired target image. Current approaches typically combine the features of each of the two e…
▽ More
An intuitive way to search for images is to use queries composed of an example image and a complementary text. While the first provides rich and implicit context for the search, the latter explicitly calls for new traits, or specifies how some elements of the example image should be changed to retrieve the desired target image. Current approaches typically combine the features of each of the two elements of the query into a single representation, which can then be compared to the ones of the potential target images. Our work aims at shedding new light on the task by looking at it through the prism of two familiar and related frameworks: text-to-image and image-to-image retrieval. Taking inspiration from them, we exploit the specific relation of each query element with the targeted image and derive light-weight attention mechanisms which enable to mediate between the two complementary modalities. We validate our approach on several retrieval benchmarks, querying with images and their associated free-form text modifiers. Our method obtains state-of-the-art results without resorting to side information, multi-level features, heavy pre-training nor large architectures as in previous works.
△ Less
Submitted 16 May, 2022; v1 submitted 15 March, 2022;
originally announced March 2022.
-
Proofs, Circuits, and Communication
Authors:
Susanna F. de Rezende,
Mika Göös,
Robert Robere
Abstract:
We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.
We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.
△ Less
Submitted 17 February, 2022;
originally announced February 2022.
-
Simple and Effective Balance of Contrastive Losses
Authors:
Arnaud Sors,
Rafael Sampaio de Rezende,
Sarah Ibrahimi,
Jean-Marc Andreoli
Abstract:
Contrastive losses have long been a key ingredient of deep metric learning and are now becoming more popular due to the success of self-supervised learning. Recent research has shown the benefit of decomposing such losses into two sub-losses which act in a complementary way when learning the representation network: a positive term and an entropy term. Although the overall loss is thus defined as a…
▽ More
Contrastive losses have long been a key ingredient of deep metric learning and are now becoming more popular due to the success of self-supervised learning. Recent research has shown the benefit of decomposing such losses into two sub-losses which act in a complementary way when learning the representation network: a positive term and an entropy term. Although the overall loss is thus defined as a combination of two terms, the balance of these two terms is often hidden behind implementation details and is largely ignored and sub-optimal in practice. In this work, we approach the balance of contrastive losses as a hyper-parameter optimization problem, and propose a coordinate descent-based search method that efficiently find the hyper-parameters that optimize evaluation performance. In the process, we extend existing balance analyses to the contrastive margin loss, include batch size in the balance, and explain how to aggregate loss elements from the batch to maintain near-optimal performance over a larger range of batch sizes. Extensive experiments with benchmarks from deep metric learning and self-supervised learning show that optimal hyper-parameters are found faster with our method than with other common search methods.
△ Less
Submitted 22 December, 2021;
originally announced December 2021.
-
Learning with Label Noise for Image Retrieval by Selecting Interactions
Authors:
Sarah Ibrahimi,
Arnaud Sors,
Rafael Sampaio de Rezende,
Stéphane Clinchant
Abstract:
Learning with noisy labels is an active research area for image classification. However, the effect of noisy labels on image retrieval has been less studied. In this work, we propose a noise-resistant method for image retrieval named Teacher-based Selection of Interactions, T-SINT, which identifies noisy interactions, ie. elements in the distance matrix, and selects correct positive and negative i…
▽ More
Learning with noisy labels is an active research area for image classification. However, the effect of noisy labels on image retrieval has been less studied. In this work, we propose a noise-resistant method for image retrieval named Teacher-based Selection of Interactions, T-SINT, which identifies noisy interactions, ie. elements in the distance matrix, and selects correct positive and negative interactions to be considered in the retrieval loss by using a teacher-based training setup which contributes to the stability. As a result, it consistently outperforms state-of-the-art methods on high noise rates across benchmark datasets with synthetic noise and more realistic noise.
△ Less
Submitted 21 December, 2021; v1 submitted 20 December, 2021;
originally announced December 2021.
-
Probabilistic Embeddings for Cross-Modal Retrieval
Authors:
Sanghyuk Chun,
Seong Joon Oh,
Rafael Sampaio de Rezende,
Yannis Kalantidis,
Diane Larlus
Abstract:
Cross-modal retrieval methods build a common representation space for samples from multiple modalities, typically from the vision and the language domains. For images and their captions, the multiplicity of the correspondences makes the task particularly challenging. Given an image (respectively a caption), there are multiple captions (respectively images) that equally make sense. In this paper, w…
▽ More
Cross-modal retrieval methods build a common representation space for samples from multiple modalities, typically from the vision and the language domains. For images and their captions, the multiplicity of the correspondences makes the task particularly challenging. Given an image (respectively a caption), there are multiple captions (respectively images) that equally make sense. In this paper, we argue that deterministic functions are not sufficiently powerful to capture such one-to-many correspondences. Instead, we propose to use Probabilistic Cross-Modal Embedding (PCME), where samples from the different modalities are represented as probabilistic distributions in the common embedding space. Since common benchmarks such as COCO suffer from non-exhaustive annotations for cross-modal matches, we propose to additionally evaluate retrieval on the CUB dataset, a smaller yet clean database where all possible image-caption pairs are annotated. We extensively ablate PCME and demonstrate that it not only improves the retrieval performance over its deterministic counterpart but also provides uncertainty estimates that render the embeddings more interpretable. Code is available at https://github.com/naver-ai/pcme
△ Less
Submitted 14 June, 2021; v1 submitted 13 January, 2021;
originally announced January 2021.
-
Clique Is Hard on Average for Regular Resolution
Authors:
Albert Atserias,
Ilario Bonacina,
Susanna F. de Rezende,
Massimo Lauria,
Jakob Nordström,
Alexander Razborov
Abstract:
We prove that for $k \ll \sqrt[4]{n}$ regular resolution requires length $n^{Ω(k)}$ to establish that an Erdős-Rényi graph with appropriately chosen edge density does not contain a $k$-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional $n^{Ω(k)}$ lower bounds on running time for several state-of-the-art algorithms for finding maxim…
▽ More
We prove that for $k \ll \sqrt[4]{n}$ regular resolution requires length $n^{Ω(k)}$ to establish that an Erdős-Rényi graph with appropriately chosen edge density does not contain a $k$-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional $n^{Ω(k)}$ lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.
△ Less
Submitted 17 December, 2020;
originally announced December 2020.
-
StacMR: Scene-Text Aware Cross-Modal Retrieval
Authors:
Andrés Mafla,
Rafael Sampaio de Rezende,
Lluís Gómez,
Diane Larlus,
Dimosthenis Karatzas
Abstract:
Recent models for cross-modal retrieval have benefited from an increasingly rich understanding of visual scenes, afforded by scene graphs and object interactions to mention a few. This has resulted in an improved matching between the visual representation of an image and the textual representation of its caption. Yet, current visual representations overlook a key aspect: the text appearing in imag…
▽ More
Recent models for cross-modal retrieval have benefited from an increasingly rich understanding of visual scenes, afforded by scene graphs and object interactions to mention a few. This has resulted in an improved matching between the visual representation of an image and the textual representation of its caption. Yet, current visual representations overlook a key aspect: the text appearing in images, which may contain crucial information for retrieval. In this paper, we first propose a new dataset that allows exploration of cross-modal retrieval where images contain scene-text instances. Then, armed with this dataset, we describe several approaches which leverage scene text, including a better scene-text aware cross-modal retrieval method which uses specialized representations for text from the captions and text from the visual scene, and reconcile them in a common embedding space. Extensive experiments confirm that cross-modal retrieval approaches benefit from scene text and highlight interesting research questions worth exploring further. Dataset and code are available at http://europe.naverlabs.com/stacmr
△ Less
Submitted 8 December, 2020;
originally announced December 2020.
-
KRW Composition Theorems via Lifting
Authors:
Susanna F. de Rezende,
Or Meir,
Jakob Nordström,
Toniann Pitassi,
Robert Robere
Abstract:
One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., $\mathbf{P}\not\subseteq\mathbf{NC}^1$). Karchmer, Raz, and Wigderson (Computational Complexity 5(3/4), 1995) suggested to approach this problem by proving that depth complexity behaves "as expected" with respect to the composition of functions $f\diamond g$. They showed th…
▽ More
One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., $\mathbf{P}\not\subseteq\mathbf{NC}^1$). Karchmer, Raz, and Wigderson (Computational Complexity 5(3/4), 1995) suggested to approach this problem by proving that depth complexity behaves "as expected" with respect to the composition of functions $f\diamond g$. They showed that the validity of this conjecture would imply that $\mathbf{P}\not\subseteq\mathbf{NC}^1$.
Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function $f$, but only for few inner functions $g$. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions.
In this work, we extend significantly the range of inner functions that can be handled. First, we consider the $\textit{monotone}$ version of the KRW conjecture. We prove it for every monotone inner function $g$ whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the $s\textbf{-}t$-connectivity, clique, and generation functions.
In order to carry this progress back to the $\textit{non-monotone}$ setting, we introduce a new notion of $\textit{semi-monotone}$ composition, which combines the non-monotone complexity of the outer function $f$ with the monotone complexity of the inner function $g$. In this setting, we prove the KRW conjecture for a similar selection of inner functions $g$, but only for a specific choice of the outer function $f$.
△ Less
Submitted 7 May, 2025; v1 submitted 6 July, 2020;
originally announced July 2020.
-
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
Authors:
Susanna F. de Rezende,
Or Meir,
Jakob Nordström,
Robert Robere
Abstract:
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph $G$ can be reversibly pebbled in time $t$ and space $s$ if and only if there is a Nullstellensatz refutation of the pebbling formula over $G$ in size $t+1$ and degree $s$ (independently of the field in which the Nullstellensatz refutation is made)…
▽ More
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph $G$ can be reversibly pebbled in time $t$ and space $s$ if and only if there is a Nullstellensatz refutation of the pebbling formula over $G$ in size $t+1$ and degree $s$ (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.
△ Less
Submitted 8 January, 2020;
originally announced January 2020.
-
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
Authors:
Susanna F. de Rezende,
Or Meir,
Jakob Nordström,
Toniann Pitassi,
Robert Robere,
Marc Vinyals
Abstract:
We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:
* We present the first result that demonstrates a separation in proo…
▽ More
We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:
* We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude.
* We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.
An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.
△ Less
Submitted 7 January, 2020;
originally announced January 2020.
-
Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
Authors:
Susanna F. de Rezende,
Jakob Nordström,
Kilian Risse,
Dmitry Sokolov
Abstract:
We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov…
▽ More
We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. We obtain our results by revisiting Razborov's pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.
△ Less
Submitted 24 March, 2025; v1 submitted 1 December, 2019;
originally announced December 2019.
-
BULNER: BUg Localization with word embeddings and NEtwork Regularization
Authors:
Jacson Rodrigues Barbosa,
Ricardo Marcondes Marcacini,
Ricardo Britto,
Frederico Soares,
Solange Rezende,
Auri M. R. Vincenzi,
Marcio E. Delamaro
Abstract:
Bug localization (BL) from the bug report is the strategic activity of the software maintaining process. Because BL is a costly and tedious activity, BL techniques information retrieval-based and machine learning-based could aid software engineers. We propose a method for BUg Localization with word embeddings and Network Regularization (BULNER). The preliminary results suggest that BULNER has bett…
▽ More
Bug localization (BL) from the bug report is the strategic activity of the software maintaining process. Because BL is a costly and tedious activity, BL techniques information retrieval-based and machine learning-based could aid software engineers. We propose a method for BUg Localization with word embeddings and Network Regularization (BULNER). The preliminary results suggest that BULNER has better performance than two state-of-the-art methods.
△ Less
Submitted 26 August, 2019;
originally announced August 2019.
-
Learning with Average Precision: Training Image Retrieval with a Listwise Loss
Authors:
Jerome Revaud,
Jon Almazan,
Rafael Sampaio de Rezende,
Cesar Roberto de Souza
Abstract:
Image retrieval can be formulated as a ranking problem where the goal is to order database images by decreasing similarity to the query. Recent deep models for image retrieval have outperformed traditional methods by leveraging ranking-tailored loss functions, but important theoretical and practical problems remain. First, rather than directly optimizing the global ranking, they minimize an upper-…
▽ More
Image retrieval can be formulated as a ranking problem where the goal is to order database images by decreasing similarity to the query. Recent deep models for image retrieval have outperformed traditional methods by leveraging ranking-tailored loss functions, but important theoretical and practical problems remain. First, rather than directly optimizing the global ranking, they minimize an upper-bound on the essential loss, which does not necessarily result in an optimal mean average precision (mAP). Second, these methods require significant engineering efforts to work well, e.g. special pre-training and hard-negative mining. In this paper we propose instead to directly optimize the global mAP by leveraging recent advances in listwise loss formulations. Using a histogram binning approximation, the AP can be differentiated and thus employed to end-to-end learning. Compared to existing losses, the proposed method considers thousands of images simultaneously at each iteration and eliminates the need for ad hoc tricks. It also establishes a new state of the art on many standard retrieval benchmarks. Models and evaluation scripts have been made available at https://europe.naverlabs.com/Deep-Image-Retrieval/
△ Less
Submitted 18 June, 2019;
originally announced June 2019.
-
Fuzzy neural networks to create an expert system for detecting attacks by SQL Injection
Authors:
Lucas Oliveira Batista,
Gabriel Adriano de Silva,
Vanessa Souza Araújo,
Vinícius Jonathan Silva Araújo,
Thiago Silva Rezende,
Augusto Junio Guimarães,
Paulo Vitor de Campos Souza
Abstract:
Its constant technological evolution characterizes the contemporary world, and every day the processes, once manual, become computerized. Data are stored in the cyberspace, and as a consequence, one must increase the concern with the security of this environment. Cyber-attacks are represented by a growing worldwide scale and are characterized as one of the significant challenges of the century. Th…
▽ More
Its constant technological evolution characterizes the contemporary world, and every day the processes, once manual, become computerized. Data are stored in the cyberspace, and as a consequence, one must increase the concern with the security of this environment. Cyber-attacks are represented by a growing worldwide scale and are characterized as one of the significant challenges of the century. This article aims to propose a computational system based on intelligent hybrid models, which through fuzzy rules allows the construction of expert systems in cybernetic data attacks, focusing on the SQL Injection attack. The tests were performed with real bases of SQL Injection attacks on government computers, using fuzzy neural networks. According to the results obtained, the feasibility of constructing a system based on fuzzy rules, with the classification accuracy of cybernetic invasions within the margin of the standard deviation (compared to the state-of-the-art model in solving this type of problem) is real. The model helps countries prepare to protect their data networks and information systems, as well as create opportunities for expert systems to automate the identification of attacks in cyberspace.
△ Less
Submitted 9 January, 2019;
originally announced January 2019.
-
Regularized Fuzzy Neural Networks to Aid Effort Forecasting in the Construction and Software Development
Authors:
Paulo Vitor de Campos Souza,
Augusto Junio Guimaraes,
Vanessa Souza Araujo,
Thiago Silva Rezende,
Vinicius Jonathan Silva Araujo
Abstract:
Predicting the time to build software is a very complex task for software engineering managers. There are complex factors that can directly interfere with the productivity of the development team. Factors directly related to the complexity of the system to be developed drastically change the time necessary for the completion of the works with the software factories. This work proposes the use of a…
▽ More
Predicting the time to build software is a very complex task for software engineering managers. There are complex factors that can directly interfere with the productivity of the development team. Factors directly related to the complexity of the system to be developed drastically change the time necessary for the completion of the works with the software factories. This work proposes the use of a hybrid system based on artificial neural networks and fuzzy systems to assist in the construction of an expert system based on rules to support in the prediction of hours destined to the development of software according to the complexity of the elements present in the same. The set of fuzzy rules obtained by the system helps the management and control of software development by providing a base of interpretable estimates based on fuzzy rules. The model was submitted to tests on a real database, and its results were promissory in the construction of an aid mechanism in the predictability of the software construction.
△ Less
Submitted 4 December, 2018;
originally announced December 2018.
-
An experimental comparison of label selection methods for hierarchical document clusters
Authors:
Maria Fernanda Moura,
Fabiano Fernandes dos Santos,
Solange Oliveira Rezende
Abstract:
The focus of this paper is on the evaluation of sixteen labeling methods for hierarchical document clusters over five datasets. All of the methods are independent from clustering algorithms, applied subsequently to the dendrogram construction and based on probabilistic dependence relations among labels and clusters. To reach a fair comparison as well as a standard benchmark, we rewrote and present…
▽ More
The focus of this paper is on the evaluation of sixteen labeling methods for hierarchical document clusters over five datasets. All of the methods are independent from clustering algorithms, applied subsequently to the dendrogram construction and based on probabilistic dependence relations among labels and clusters. To reach a fair comparison as well as a standard benchmark, we rewrote and presented the labeling methods in a similar notation. The experimental results were analyzed through a proposed evaluation methodology based on: (i) data standardization before applying the cluster labeling methods and over the labeling results; (ii) a particular information retrieval process, using the obtained labels and their hierarchical relations to construct the search queries; (iii) evaluation of the retrieval process through precision, recall and F measure; (iv) variance analysis of the retrieval results to better understanding the differences among the labeling methods; and, (v) the emulation of a human judgment through the analysis of a topic observed coherence measure - normalized Pointwise Mutual Information (PMI). Applying the methodology, we are able to highlight the advantages of certain methods: to capture specific information; for a better document hierarchy comprehension at different levels of granularity; and, to capture the most coherent labels through the label selections. Finally, the experimental results demonstrated that the label selection methods which hardly consider hierarchical relations had the best results.
△ Less
Submitted 24 May, 2018;
originally announced May 2018.
-
Exposing Computer Generated Images by Using Deep Convolutional Neural Networks
Authors:
Edmar R. S. de Rezende,
Guilherme C. S. Ruppert,
Antonio Theophilo,
Tiago Carvalho
Abstract:
The recent computer graphics developments have upraised the quality of the generated digital content, astonishing the most skeptical viewer. Games and movies have taken advantage of this fact but, at the same time, these advances have brought serious negative impacts like the ones yielded by fakeimages produced with malicious intents. Digital artists can compose artificial images capable of deceiv…
▽ More
The recent computer graphics developments have upraised the quality of the generated digital content, astonishing the most skeptical viewer. Games and movies have taken advantage of this fact but, at the same time, these advances have brought serious negative impacts like the ones yielded by fakeimages produced with malicious intents. Digital artists can compose artificial images capable of deceiving the great majority of people, turning this into a very dangerous weapon in a timespan currently know as Fake News/Post-Truth" Era. In this work, we propose a new approach for dealing with the problem of detecting computer generated images, through the application of deep convolutional networks and transfer learning techniques. We start from Residual Networks and develop different models adapted to the binary problem of identifying if an image was or not computer generated. Differently from the current state-of-the-art approaches, we don't rely on hand-crafted features, but provide to the model the raw pixel information, achieving the same 0.97 of state-of-the-art methods with two main advantages: our methods show more stable results (depicted by lower variance) and eliminate the laborious and manual step of specialized features extraction and selection.
△ Less
Submitted 28 November, 2017;
originally announced November 2017.
-
SCNet: Learning Semantic Correspondence
Authors:
Kai Han,
Rafael S. Rezende,
Bumsub Ham,
Kwan-Yee K. Wong,
Minsu Cho,
Cordelia Schmid,
Jean Ponce
Abstract:
This paper addresses the problem of establishing semantic correspondences between images depicting different instances of the same object or scene category. Previous approaches focus on either combining a spatial regularizer with hand-crafted features, or learning a correspondence model for appearance only. We propose instead a convolutional neural network architecture, called SCNet, for learning…
▽ More
This paper addresses the problem of establishing semantic correspondences between images depicting different instances of the same object or scene category. Previous approaches focus on either combining a spatial regularizer with hand-crafted features, or learning a correspondence model for appearance only. We propose instead a convolutional neural network architecture, called SCNet, for learning a geometrically plausible model for semantic correspondence. SCNet uses region proposals as matching primitives, and explicitly incorporates geometric consistency in its loss function. It is trained on image pairs obtained from the PASCAL VOC 2007 keypoint dataset, and a comparative evaluation on several standard benchmarks demonstrates that the proposed approach substantially outperforms both recent deep learning architectures and previous methods based on hand-crafted features.
△ Less
Submitted 17 August, 2017; v1 submitted 11 May, 2017;
originally announced May 2017.
-
PAMPO: using pattern matching and pos-tagging for effective Named Entities recognition in Portuguese
Authors:
Conceição Rocha,
Alípio Jorge,
Roberta Sionara,
Paula Brito,
Carlos Pimenta,
Solange Rezende
Abstract:
This paper deals with the entity extraction task (named entity recognition) of a text mining process that aims at unveiling non-trivial semantic structures, such as relationships and interaction between entities or communities. In this paper we present a simple and efficient named entity extraction algorithm. The method, named PAMPO (PAttern Matching and POs tagging based algorithm for NER), relie…
▽ More
This paper deals with the entity extraction task (named entity recognition) of a text mining process that aims at unveiling non-trivial semantic structures, such as relationships and interaction between entities or communities. In this paper we present a simple and efficient named entity extraction algorithm. The method, named PAMPO (PAttern Matching and POs tagging based algorithm for NER), relies on flexible pattern matching, part-of-speech tagging and lexical-based rules. It was developed to process texts written in Portuguese, however it is potentially applicable to other languages as well.
We compare our approach with current alternatives that support Named Entity Recognition (NER) for content written in Portuguese. These are Alchemy, Zemanta and Rembrandt. Evaluation of the efficacy of the entity extraction method on several texts written in Portuguese indicates a considerable improvement on $recall$ and $F_1$ measures.
△ Less
Submitted 30 December, 2016;
originally announced December 2016.
-
Combining Privileged Information to Improve Context-Aware Recommender Systems
Authors:
Camila V. Sundermann,
Marcos A. Domingues,
Ricardo M. Marcacini,
Solange O. Rezende
Abstract:
A recommender system is an information filtering technology which can be used to predict preference ratings of items (products, services, movies, etc) and/or to output a ranking of items that are likely to be of interest to the user. Context-aware recommender systems (CARS) learn and predict the tastes and preferences of users by incorporating available contextual information in the recommendation…
▽ More
A recommender system is an information filtering technology which can be used to predict preference ratings of items (products, services, movies, etc) and/or to output a ranking of items that are likely to be of interest to the user. Context-aware recommender systems (CARS) learn and predict the tastes and preferences of users by incorporating available contextual information in the recommendation process. One of the major challenges in context-aware recommender systems research is the lack of automatic methods to obtain contextual information for these systems. Considering this scenario, in this paper, we propose to use contextual information from topic hierarchies of the items (web pages) to improve the performance of context-aware recommender systems. The topic hierarchies are constructed by an extension of the LUPI-based Incremental Hierarchical Clustering method that considers three types of information: traditional bag-of-words (technical information), and the combination of named entities (privileged information I) with domain terms (privileged information II). We evaluated the contextual information in four context-aware recommender systems. Different weights were assigned to each type of information. The empirical results demonstrated that topic hierarchies with the combination of the two kinds of privileged information can provide better recommendations.
△ Less
Submitted 4 January, 2019; v1 submitted 6 November, 2015;
originally announced November 2015.
-
Using Taxonomies to Facilitate the Analysis of the Association Rules
Authors:
Marcos Aurélio Domingues,
Solange Oliveira Rezende
Abstract:
The Data Mining process enables the end users to analyze, understand and use the extracted knowledge in an intelligent system or to support in the decision-making processes. However, many algorithms used in the process encounter large quantities of patterns, complicating the analysis of the patterns. This fact occurs with association rules, a Data Mining technique that tries to identify intrinsic…
▽ More
The Data Mining process enables the end users to analyze, understand and use the extracted knowledge in an intelligent system or to support in the decision-making processes. However, many algorithms used in the process encounter large quantities of patterns, complicating the analysis of the patterns. This fact occurs with association rules, a Data Mining technique that tries to identify intrinsic patterns in large data sets. A method that can help the analysis of the association rules is the use of taxonomies in the step of post-processing knowledge. In this paper, the GART algorithm is proposed, which uses taxonomies to generalize association rules, and the RulEE-GAR computational module, that enables the analysis of the generalized rules.
△ Less
Submitted 7 December, 2011;
originally announced December 2011.