Theta as a Horn Solver

• URL: http://arxiv.org/abs/2510.26430v1
• Date: Thu, 30 Oct 2025 12:24:52 GMT
• Title: Theta as a Horn Solver
• Abstract summary: Theta is a verification framework that has participated in the CHC-COMP competition since 2023.<n>This paper provides a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers.<n>We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained mostly unchanged, Theta's verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta's performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta's actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance.

Related papers

• Concept Regions Matter: Benchmarking CLIP with a New Cluster-Importance Approach [20.898059440239603]
  Cluster-based Concept Importance (CCI) is a novel interpretability method.<n>CCI sets a new state of the art on faithfulness benchmarks.<n>We present a comprehensive evaluation of eighteen CLIP variants.
  arXiv  Detail & Related papers  (2025-11-17T05:01:24Z)
• CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses [0.0]
  Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for verification tasks.<n>This paper introduces a portfolio-based CHC solver that adopts a software verification approach for solving CHCs.
  arXiv  Detail & Related papers  (2025-10-30T12:25:06Z)
• A Technical Report on the Second Place Solution for the CIKM 2025 AnalytiCup Competition [11.41948435879935]
  This work addresses the challenge of multilingual category relevance judgment in e-commerce search.<n>We propose a framework that leverages prompt engineering with Chain-of-Thought task decomposition.<n> Experimental results show that our single-model framework achieves competitive accuracy and high inference efficiency.
  arXiv  Detail & Related papers  (2025-10-25T16:31:21Z)
• Link Prediction for Event Logs in the Process Industry [4.139846693958609]
  Record linking (RL) is a cross-document coreference resolution (CDCR) task enhanced with natural language inference (NLI) and semantic text similarity (STS)<n>We adapt CDCR, traditionally applied in the news domain, into an RL model to operate at the passage level, similar to NLI and STS, while accommodating the process industry's specific text formats.<n>Our work demonstrates how domain adaptation of the state-of-the-art CDCR models, enhanced with reasoning capabilities, can be effectively tailored to the process industry.
  arXiv  Detail & Related papers  (2025-08-12T17:22:29Z)
• Sliding Window Informative Canonical Correlation Analysis [0.0]
  Canonical correlation analysis (CCA) is a technique for finding correlated sets of features between two datasets.<n>We propose a novel extension of CCA to the online, streaming data setting: Sliding Window Informative Canonical Correlation Analysis (SWICCA)
  arXiv  Detail & Related papers  (2025-07-23T20:35:15Z)
• Tuning for Trustworthiness -- Balancing Performance and Explanation Consistency in Neural Network Optimization [49.567092222782435]
  We introduce the novel concept of XAI consistency, defined as the agreement among different feature attribution methods.<n>We create a multi-objective optimization framework that balances predictive performance with explanation.<n>Our research provides a foundation for future investigations into whether models from the trade-off zone-balancing performance loss and XAI consistency-exhibit greater robustness.
  arXiv  Detail & Related papers  (2025-05-12T13:19:14Z)
• EFaR 2023: Efficient Face Recognition Competition [51.77649060180531]
  The paper presents the summary of the Efficient Face Recognition Competition (EFaR) held at the 2023 International Joint Conference on Biometrics (IJCB 2023) The competition received 17 submissions from 6 different teams. The submitted solutions are ranked based on a weighted score of the achieved verification accuracies on a diverse set of benchmarks, as well as the deployability given by the number of floating-point operations and model size.
  arXiv  Detail & Related papers  (2023-08-08T09:58:22Z)
• Better Handling Coreference Resolution in Aspect Level Sentiment Classification by Fine-Tuning Language Models [4.2605449879340656]
  Monitoring customer feedback can be automated with Aspect Level Sentiment Classification (ALSC) Large Language Models (LLMs) are the heart of many state-of-the-art ALSC solutions, but they perform poorly in some scenarios requiring Coreference Resolution (CR) We propose a framework to improve an LLM's performance on CR-containing reviews by fine tuning on highly inferential tasks.
  arXiv  Detail & Related papers  (2023-07-11T12:43:28Z)
• Improving Chinese Spelling Check by Character Pronunciation Prediction: The Effects of Adaptivity and Granularity [76.20568599642799]
  Chinese spelling check (CSC) is a fundamental NLP task that detects and corrects spelling errors in Chinese texts. In this paper, we consider introducing an auxiliary task of Chinese pronunciation prediction ( CPP) to improve CSC. We propose SCOPE which builds on top of a shared encoder two parallel decoders, one for the primary CSC task and the other for a fine-grained auxiliary CPP task.
  arXiv  Detail & Related papers  (2022-10-20T03:42:35Z)
• CTC Alignments Improve Autoregressive Translation [145.90587287444976]
  We argue that CTC does in fact make sense for translation if applied in a joint CTC/attention framework. Our proposed joint CTC/attention models outperform pure-attention baselines across six benchmark translation tasks.
  arXiv  Detail & Related papers  (2022-10-11T07:13:50Z)
• Performance Evaluation of Adversarial Attacks: Discrepancies and Solutions [51.8695223602729]
  adversarial attack methods have been developed to challenge the robustness of machine learning models. We propose a Piece-wise Sampling Curving (PSC) toolkit to effectively address the discrepancy. PSC toolkit offers options for balancing the computational cost and evaluation effectiveness.
  arXiv  Detail & Related papers  (2021-04-22T14:36:51Z)
• Visual Alignment Constraint for Continuous Sign Language Recognition [74.26707067455837]
  Vision-based Continuous Sign Language Recognition aims to recognize unsegmented gestures from image sequences. In this work, we revisit the overfitting problem in recent CTC-based CSLR works and attribute it to the insufficient training of the feature extractor. We propose a Visual Alignment Constraint (VAC) to enhance the feature extractor with more alignment supervision.
  arXiv  Detail & Related papers  (2021-04-06T07:24:58Z)
• CIF-based Collaborative Decoding for End-to-end Contextual Speech Recognition [14.815422751109061]
  We propose a continuous integrate-and-fire (CIF) based model that supports contextual biasing in a more controllable fashion. An extra context processing network is introduced to extract contextual embeddings, integrate acoustically relevant context information and decode the contextual output distribution. Our method brings relative character error rate (CER) reduction of 8.83%/21.13% and relative named entity character error rate (NE-CER) reduction of 40.14%/51.50% when compared with a strong baseline.
  arXiv  Detail & Related papers  (2020-12-17T09:40:11Z)

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.