arXiv subjects

Bryan Tan

Publications and source records attributed to Bryan Tan.

4 recordsLinked to original sources

arXiv2026

SemEval-2026 Task 7: Everyday Knowledge Across Diverse Languages and Cultures

We present our shared task on evaluating the adaptability of LLMs and NLP systems across multiple languages and cultures. The task data consist of an extended version of our manually constructed BLEnD benchmark (Myung et al. 2024), covering more than 30 language-culture pairs, predominantly representing low-resource languages spoken across multiple continents. As the task is designed strictly for evaluation, participants were not permitted to use the data for training, fine-tuning, few-shot learning, or any other form of model modification. Our task includes two tracks: (a) Short-Answer Questions (SAQ) and (b) Multiple-Choice Questions (MCQ). Participants were required to predict labels and were allowed to submit any NLP system and adopt diverse modelling strategies, provided that the benchmark was used solely for evaluation. The task attracted more than 140 registered participants, and we received final submissions from 62 teams, along with 19 system description papers. We report the results and present an analysis of the best-performing systems and the most commonly adopted approaches. Furthermore, we discuss shared insights into open questions and challenges related to evaluation, misalignment, and methodological perspectives on model behaviour in low-resource languages and for under-represented cultures.

cs.CL↗

arXiv2023

Datapath Verification via Word-Level E-Graph Rewriting

Formal verification of datapath circuits is challenging as they are subject to intense optimization effort in the design phase. Industrial vendors and design companies deploy equivalence checking against a golden or existing reference design to satisfy correctness concerns. State-of-the-art datapath equivalence checking tools deploy a suite of techniques, including rewriting. We propose a rewriting framework deploying bitwidth dependent rewrites based on the e-graph data structure, providing a powerful assistant to existing tools. The e-graph can generate a path of rewrites between the reference and implementation designs that can be checked by a trusted industry tool. We will demonstrate how the intermediate proofs generated by the assistant enable convergence in a state of the art tool, without which the industrial tool runs for 24 hours without making progress. The intermediate proofs automatically introduced by the assistant also reduce the total proof runtime by up to 6x.

cs.LO↗

arXiv2023

Certifying Zero-Knowledge Circuits with Refinement Types

Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application through a rich refinement type system. One of the key challenges in formally verifying ZK applications is that they require reasoning about polynomial equations over large prime fields that go beyond the capabilities of automated theorem provers. Coda mitigates this challenge by generating a set of Coq lemmas that can be proven in an interactive manner with the help of a tactic library. We have used Coda to re-implement 79 arithmetic circuits from widely-used Circom libraries and applications. Our evaluation shows that Coda makes it possible to specify important and formally verify correctness properties of these circuits. Our evaluation also revealed 6 previously-unknown vulnerabilities in the original Circom projects.

cs.CR↗

arXiv2021

Fast Parallel Hypertree Decompositions in Logarithmic Recursion Depth

Modern trends in data collection are bringing current mainstream techniques for database query processing to their limits. Consequently, various novel approaches for efficient query processing are being actively studied. One such approach is based on hypertree decompositions (HDs), which have been shown to carry great potential to process complex queries more efficiently and with stronger theoretical guarantees. However, using HDs for query execution relies on the difficult task of computing decompositions of the query structure, which guides the efficient execution of the query. From theoretical results we know that the performance of purely sequential methods is inherently limited, yet the problem is susceptible to parallelisation. In this paper we propose the first algorithm for computing hypertree decompositions that is well-suited for parallelisation. The proposed algorithm log-k-decomp requires only a logarithmic number of recursion levels and additionally allows for highly parallelised pruning of the search space by restriction to balanced separators. We provide detailed experimental evaluation over the HyperBench benchmark and demonstrate that our approach is highly effective especially for complex queries.

cs.DB↗