Verifying a Realistic Mutable Hash Table

• URL: http://arxiv.org/abs/2107.08824v6
• Date: Tue, 30 Jan 2024 14:57:45 GMT
• Title: Verifying a Realistic Mutable Hash Table
• Abstract summary: We verify the mutable LongMap from the standard Scala library, a hash table using open addressing within a single array. We introduce a new reference swapping construct in Stainless that allows us to apply the decorator pattern without introducing aliasing. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a reference implementation, we write an immutable map based on a list of tuples. We then show that LongMap's operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference swapping construct in Stainless. This allows us to apply the decorator pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure.

Related papers

• Beyond Post-Quantization: Native Hash Learning with a Dedicated HASH Token [20.81211439061764]
  HashViT is a Vision Transformer framework for native hash token learning.<n>It is optimized with a unified objective that combines learnable semantic center supervision, class-token similarity distillation, and quantization regularization.<n>Experiments on three widely used benchmarks demonstrate that HashViT achieves state-of-the-art or highly competitive retrieval performance.
  arXiv  Detail & Related papers  (2026-07-03T13:46:18Z)
• MapReplay: Trace-Driven Benchmark Generation for Java HashMap [1.198637189064676]
  We propose MapReplay, a benchmarking methodology that combines the realism of application benchmarks with the efficiency of microbenchmarks.<n>Applying MapReplay to DaCapo-Chopin and Renaissance, the resulting suite, MapReplayBench, reproduces application-level performance trends.
  arXiv  Detail & Related papers  (2026-03-14T16:46:09Z)
• GraphHash: Graph Clustering Enables Parameter Efficiency in Recommender Systems [51.64666652517944]
  This paper introduces GraphHash, the first graph-based approach that leverages modularity-based bipartite graph clustering to reduce embedding table sizes. By employing fast clustering algorithms, GraphHash serves as a computationally efficient proxy for message-passing during preprocessing. In experiments, GraphHash substantially outperforms diverse hashing baselines on both retrieval and click-through-rate prediction tasks.
  arXiv  Detail & Related papers  (2024-12-23T03:37:58Z)
• Verified invertible lexer using regular expressions and DFAs [0.0]
  In this project, we explore the concept of invertibility applied to serialisation and lexing frameworks. While serialisation is the process of taking a data structure and writing it to a bit array, lexing is the process of reading a stream of characters and splitting them into tokens.
  arXiv  Detail & Related papers  (2024-12-18T08:03:17Z)
• Contrastive Instruction Tuning [61.97704869248903]
  We propose Contrastive Instruction Tuning to maximize the similarity between semantically equivalent instruction-instance pairs. Experiments on the PromptBench benchmark show that CoIN consistently improves LLMs' robustness to unseen instructions with variations across character, word, sentence, and semantic levels by an average of +2.5% in accuracy.
  arXiv  Detail & Related papers  (2024-02-17T00:09:32Z)
• ClusterTabNet: Supervised clustering method for table detection and table structure recognition [0.0]
  We present a novel deep-learning-based method to cluster words in documents which we apply to detect and recognize tables given the OCR output. We interpret table structure bottom-up as a graph of relations between pairs of words and use a transformer encoder model to predict its adjacency matrix. Compared to the current state-of-the-art detection methods such as DETR and Faster R-CNN, our method achieves similar or better accuracy, while requiring a significantly smaller model.
  arXiv  Detail & Related papers  (2024-02-12T09:10:24Z)
• ASH: A Modern Framework for Parallel Spatial Hashing in 3D Perception [91.24236600199542]
  ASH is a modern and high-performance framework for parallel spatial hashing on GPU. ASH achieves higher performance, supports richer functionality, and requires fewer lines of code. ASH and its example applications are open sourced in Open3D.
  arXiv  Detail & Related papers  (2021-10-01T16:25:40Z)
• CIMON: Towards High-quality Hash Codes [63.37321228830102]
  We propose a new method named textbfComprehensive stextbfImilarity textbfMining and ctextbfOnsistency leartextbfNing (CIMON) First, we use global refinement and similarity statistical distribution to obtain reliable and smooth guidance. Second, both semantic and contrastive consistency learning are introduced to derive both disturb-invariant and discriminative hash codes.
  arXiv  Detail & Related papers  (2020-10-15T14:47:14Z)
• Unsupervised Semantic Hashing with Pairwise Reconstruction [22.641786533525245]
  We present Pairwise Reconstruction (PairRec), which is a discrete variational autoencoder based hashing model. We experimentally compare PairRec to traditional and state-of-the-art approaches, and obtain significant performance improvements in the task of document similarity search.
  arXiv  Detail & Related papers  (2020-07-01T10:54:27Z)
• ToTTo: A Controlled Table-To-Text Generation Dataset [61.83159452483026]
  ToTTo is an open-domain English table-to-text dataset with over 120,000 training examples. We introduce a dataset construction process where annotators directly revise existing candidate sentences from Wikipedia. While usually fluent, existing methods often hallucinate phrases that are not supported by the table.
  arXiv  Detail & Related papers  (2020-04-29T17:53:45Z)
• Active Learning for Coreference Resolution using Discrete Annotation [76.36423696634584]
  We improve upon pairwise annotation for active learning in coreference resolution. We ask annotators to identify mention antecedents if a presented mention pair is deemed not coreferent. In experiments with existing benchmark coreference datasets, we show that the signal from this additional question leads to significant performance gains per human-annotation hour.
  arXiv  Detail & Related papers  (2020-04-28T17:17:11Z)
• Increasing the Inference and Learning Speed of Tsetlin Machines with Clause Indexing [9.440900386313215]
  The Tsetlin Machine (TM) is a machine learning algorithm founded on the classical Tsetlin Automaton (TA) and game theory. We report up to 15 times faster classification and three times faster learning on MNIST and Fashion-MNIST image classification, and IMDb sentiment analysis.
  arXiv  Detail & Related papers  (2020-04-07T08:16:07Z)
• Weakly-Supervised Salient Object Detection via Scribble Annotations [54.40518383782725]
  We propose a weakly-supervised salient object detection model to learn saliency from scribble labels. We present a new metric, termed saliency structure measure, to measure the structure alignment of the predicted saliency maps. Our method not only outperforms existing weakly-supervised/unsupervised methods, but also is on par with several fully-supervised state-of-the-art models.
  arXiv  Detail & Related papers  (2020-03-17T12:59:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.