Showing 1–12 of 12 results for author: Fuhs, C

Investigating Confidence Estimation Measures for Speaker Diarization

Authors: Anurag Chowdhury, Abhinav Misra, Mark C. Fuhs, Monika Woszczyna

Abstract: Speaker diarization systems segment a conversation recording based on the speakers' identity. Such systems can misclassify the speaker of a portion of audio due to a variety of factors, such as speech pattern variation, background noise, and overlap** speech. These errors propagate to, and can adversely affect, downstream systems that rely on the speaker's identity, such as speaker-adapted speec… ▽ More Speaker diarization systems segment a conversation recording based on the speakers' identity. Such systems can misclassify the speaker of a portion of audio due to a variety of factors, such as speech pattern variation, background noise, and overlap** speech. These errors propagate to, and can adversely affect, downstream systems that rely on the speaker's identity, such as speaker-adapted speech recognition. One of the ways to mitigate these errors is to provide segment-level diarization confidence scores to downstream systems. In this work, we investigate multiple methods for generating diarization confidence scores, including those derived from the original diarization system and those derived from an external model. Our experiments across multiple datasets and diarization systems demonstrate that the most competitive confidence score methods can isolate ~30% of the diarization errors within segments with the lowest ~10% of confidence scores. △ Less

Submitted 24 June, 2024; originally announced June 2024.

Comments: Accepted in INTERSPEECH 2024

Transcription-Free Fine-Tuning of Speech Separation Models for Noisy and Reverberant Multi-Speaker Automatic Speech Recognition

Authors: William Ravenscroft, George Close, Stefan Goetze, Thomas Hain, Mohammad Soleymanpour, Anurag Chowdhury, Mark C. Fuhs

Abstract: One solution to automatic speech recognition (ASR) of overlap** speakers is to separate speech and then perform ASR on the separated signals. Commonly, the separator produces artefacts which often degrade ASR performance. Addressing this issue typically requires reference transcriptions to jointly train the separation and ASR networks. This is often not viable for training on real-world in-domai… ▽ More One solution to automatic speech recognition (ASR) of overlap** speakers is to separate speech and then perform ASR on the separated signals. Commonly, the separator produces artefacts which often degrade ASR performance. Addressing this issue typically requires reference transcriptions to jointly train the separation and ASR networks. This is often not viable for training on real-world in-domain audio where reference transcript information is not always available. This paper proposes a transcription-free method for joint training using only audio signals. The proposed method uses embedding differences of pre-trained ASR encoders as a loss with a proposed modification to permutation invariant training (PIT) called guided PIT (GPIT). The method achieves a 6.4% improvement in word error rate (WER) measures over a signal-level loss and also shows enhancement improvements in perceptual measures such as short-time objective intelligibility (STOI). △ Less

Submitted 13 June, 2024; originally announced June 2024.

Comments: 5 pages, 3 Figures, 3 Tables, Accepted for Interspeech 2024

On Complexity Bounds and Confluence of Parallel Term Rewriting

Authors: Thaïs Baudon, Carsten Fuhs, Laure Gonnord

Abstract: We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. Our appro… ▽ More We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. Our approach to find lower bounds requires confluence of the parallel-innermost rewrite relation, thus we also provide effective sufficient criteria for proving confluence. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature. △ Less

Submitted 29 May, 2023; originally announced May 2023.

Comments: Under submission to Fundamenta Informaticae. arXiv admin note: substantial text overlap with arXiv:2208.01005

Analysing Parallel Complexity of Term Rewriting

Authors: Thaïs Baudon, Carsten Fuhs, Laure Gonnord

Abstract: We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. The appli… ▽ More We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature. △ Less

Submitted 1 August, 2022; originally announced August 2022.

Comments: Extended authors' accepted manuscript for a paper accepted for publication in the Proceedings of the 32nd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2022). 27 pages

A Calculus for Modular Loop Acceleration and Non-Termination Proofs

Authors: Florian Frohn, Carsten Fuhs

Abstract: Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. In contrast, we present a calculus that allows for combini… ▽ More Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. Some of these acceleration techniques apply only to non-terminating loops. Thus, combining them with our novel calculus results in a new, modular approach for proving non-termination. An empirical evaluation demonstrates the applicability of our approach, both for loop acceleration and for proving non-termination. △ Less

Submitted 8 June, 2022; v1 submitted 27 November, 2021; originally announced November 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2001.01516

A static higher-order dependency pair framework

Authors: Carsten Fuhs, Cynthia Kop

Abstract: We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applica… ▽ More We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA. △ Less

Submitted 4 April, 2019; v1 submitted 15 February, 2019; originally announced February 2019.

Comments: Extended version of a paper which is to appear in the proceedings of ESOP 2019 (28th European Symposium on Programming). arXiv admin note: text overlap with arXiv:1805.09390

The unified higher-order dependency pair framework

Authors: Carsten Fuhs, Cynthia Kop

Abstract: In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the dynamic approach. Both approaches offer distinct advantages and disadvantages. However, a grand unifying theory is thus far missing, and both approaches lack the modularity present in the dependency pair framework commonl… ▽ More In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the dynamic approach. Both approaches offer distinct advantages and disadvantages. However, a grand unifying theory is thus far missing, and both approaches lack the modularity present in the dependency pair framework commonly used in first-order rewriting. Moreover, neither approach can be used to prove non-termination. In this paper, we aim to address this gap by defining a higher-order dependency pair framework, integrating both approaches into a shared formal setup. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA. △ Less

Submitted 23 May, 2018; originally announced May 2018.

Verifying Procedural Programs via Constrained Rewriting Induction

Authors: Carsten Fuhs, Cynthia Kop, Naoki Nishida

Abstract: This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and pro… ▽ More This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations, so in contrast to other works, we do not require an explicit specification in a separate specification language. △ Less

Submitted 25 February, 2017; v1 submitted 30 August, 2014; originally announced September 2014.

ACM Class: D.2.4; I.2.3

First-Order Formative Rules

Authors: Carsten Fuhs, Cynthia Kop

Abstract: This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow drop** some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the tech… ▽ More This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow drop** some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique. △ Less

Submitted 30 April, 2014; originally announced April 2014.

Comments: Extended version of a paper which is to appear in the proceedings of RTA-TLCA 2014 (Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications)

Polynomial Interpretations for Higher-Order Rewriting

Authors: Carsten Fuhs, Cynthia Kop

Abstract: The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-orde… ▽ More The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA. △ Less

Submitted 26 March, 2012; originally announced March 2012.

SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

Authors: Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amram, Carsten Fuhs, Jürgen Giesl

Abstract: We describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a non-trivial extension of the well-known size-change termination method. While deciding termination for systems of monotonicity constraints is PSPACE complete, we focus on a well-defined and significant subset, which we call MCNP, desig… ▽ More We describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a non-trivial extension of the well-known size-change termination method. While deciding termination for systems of monotonicity constraints is PSPACE complete, we focus on a well-defined and significant subset, which we call MCNP, designed to be amenable to a SAT-based solution. Our technique is based on the search for a special type of ranking function defined in terms of bounded differences between multisets of integer values. We describe the application of our approach as the back-end for the termination analysis of Java Bytecode (JBC). At the front-end, systems of monotonicity constraints are obtained by abstracting information, using two different termination analyzers: AProVE and COSTA. Preliminary results reveal that our approach provides a good trade-off between precision and cost of analysis. △ Less

Submitted 29 July, 2011; originally announced July 2011.

Journal ref: Theory and Practice of Logic Programming, 27th International Conference on Logic Programming (ICLP'11) Special Issue, volume 11, issue 4-5, pages 503-520, 2011

Optimal Base Encodings for Pseudo-Boolean Constraints

Authors: Michael Codish, Yoav Fekete, Carsten Fuhs, Peter Schneider-Kamp

Abstract: This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MINISAT+. Experimentation indicates that our algorithm scales to bases involving numbers up to 1,000,000, improving on the restriction… ▽ More This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MINISAT+. Experimentation indicates that our algorithm scales to bases involving numbers up to 1,000,000, improving on the restriction in MINISAT+ to prime numbers up to 17. We show that, while for many examples primes up to 17 do suffice, encoding with respect to optimal bases reduces the CNF sizes and improves the subsequent SAT solving time for many examples. △ Less

Submitted 1 January, 2011; v1 submitted 28 July, 2010; originally announced July 2010.