-
Time-varying EEG spectral power predicts evoked and spontaneous fMRI motor brain activity
Authors:
Neil Mehta,
Ines Goncalves,
Alberto Montagna,
Mathis Fleury,
Gustavo Caetano,
Ines Esteves,
Athanasios Vourvopoulos,
Pulkit Grover,
Patricia Figueiredo
Abstract:
Simultaneous EEG-fMRI recordings are increasingly used to investigate brain activity by leveraging the complementary high spatial and high temporal resolution of fMRI and EEG signals respectively. It remains unclear, however, to what degree these two imaging modalities capture shared information about neural activity. Here, we investigate whether it is possible to predict both task-evoked and spon…
▽ More
Simultaneous EEG-fMRI recordings are increasingly used to investigate brain activity by leveraging the complementary high spatial and high temporal resolution of fMRI and EEG signals respectively. It remains unclear, however, to what degree these two imaging modalities capture shared information about neural activity. Here, we investigate whether it is possible to predict both task-evoked and spontaneous fMRI signals of motor brain networks from EEG time-varying spectral power using interpretable models trained for individual subjects with Sparse Group Lasso regularization. Critically, we test the trained models on data acquired from each subject on a different day and obtain statistical validation by comparison with appropriate null models as well as the conventional EEG sensorimotor rhythm. We find significant prediction results in most subjects, although less frequently for resting-state compared to task-based conditions. Furthermore, we interpret the model learned parameters to understand representations of EEG-fMRI coupling in terms of predictive EEG channels, frequencies, and haemodynamic delays. In conclusion, our work provides evidence of the ability to predict fMRI motor brain activity from EEG recordings alone across different days, in both task-evoked and spontaneous conditions, with statistical significance in individual subjects. These results present great potential for translation to EEG neurofeedback applications.
△ Less
Submitted 14 April, 2025;
originally announced April 2025.
-
Lazy Reimplication in Chronological Backtracking
Authors:
Robin Coutelier,
Mathias Fleury,
Laura Kovács
Abstract:
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reim…
▽ More
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.
△ Less
Submitted 13 January, 2025;
originally announced January 2025.
-
Life span of SAT techniques
Authors:
Mathias Fleury,
Daniela Kaufmann
Abstract:
In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) d…
▽ More
In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) disabling features is always harmful; (ii) the life span of the techniques is limited; and (iii) features simulate each other. Our experiments cannot confirm any of the hypothesis.
△ Less
Submitted 2 February, 2024;
originally announced February 2024.
-
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Authors:
Mathias Fleury,
Armin Biere
Abstract:
We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other state-of-the-art multi-threaded SAT solvers to exchange clauses logically. Our approach keeps information about which literals are watched in a clause local to a solving thread but shares the actual immutable literals of a c…
▽ More
We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other state-of-the-art multi-threaded SAT solvers to exchange clauses logically. Our approach keeps information about which literals are watched in a clause local to a solving thread but shares the actual immutable literals of a clause globally among all solving threads. This design gives quite remarkable parallel scalability, allows aggressive clause sharing while keeping memory usage low and produces more compact proofs.
△ Less
Submitted 29 July, 2022; v1 submitted 27 July, 2022;
originally announced July 2022.
-
Alethe: Towards a Generic SMT Proof Format (extended abstract)
Authors:
Hans-Jörg Schurr,
Mathias Fleury,
Haniel Barbosa,
Pascal Fontaine
Abstract:
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the for…
▽ More
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.
△ Less
Submitted 5 July, 2021;
originally announced July 2021.
-
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving
Authors:
Chantal Keller,
Mathias Fleury
Abstract:
This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conference in Pittsburgh, USA. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proo…
▽ More
This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conference in Pittsburgh, USA. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proofs. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation between such tools in larger systems has demonstrated the potential to reduce the amount of manual intervention. Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop series strives to encourage such cooperation by inviting contributions on all aspects of cooperation between reasoning tools, whether automatic or interactive.
△ Less
Submitted 4 July, 2021;
originally announced July 2021.
-
Reconstructing veriT Proofs in Isabelle/HOL
Authors:
Mathias Fleury,
Hans-Jörg Schurr
Abstract:
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theo…
▽ More
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theories solver veriT which is part of the smt tactic. We describe in detail the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals.
△ Less
Submitted 26 August, 2019;
originally announced August 2019.
-
Effectiveness of Crypto-Transcoding for H.264/AVC and HEVC Video Bit-streams
Authors:
Rizwan A. Shah,
Mamoona N. Asghar,
Saima Abdullah,
Martin Fleury,
Neelam Gohar
Abstract:
To avoid delays arising from a need to decrypt a video prior to transcoding and then re-encrypt it afterwards, this paper assesses a selective encryption (SE) content protection scheme. The scheme is suited to both recent standardized codecs, namely H.264/Advanced Video Coding (AVC) and High Efficiency Video Coding (HEVC). Specifically, the paper outlines a joint crypto-transcoding scheme for secu…
▽ More
To avoid delays arising from a need to decrypt a video prior to transcoding and then re-encrypt it afterwards, this paper assesses a selective encryption (SE) content protection scheme. The scheme is suited to both recent standardized codecs, namely H.264/Advanced Video Coding (AVC) and High Efficiency Video Coding (HEVC). Specifically, the paper outlines a joint crypto-transcoding scheme for secure transrating of a video bitstream. That is to say it generates new video bitrates, possibly as part of an HTTP Adaptive Streaming (HAS) content delivery network. The scheme will reduce the bitrate to one or more lower desired bit-rate without consuming time in the encryption/decryption process, which would be the case when full encryption is used. In addition, the decryption key no longer needs to be exposed at intermediate middleboxes, including when transrating is performed in a cloud datacenter. The effectiveness of the scheme is variously evaluated: by examination of the SE generated visual distortion; by the extent of computational and bitrate overheads; and by choice of cipher when encrypting the selected elements within the bitstream. Results indicate that there remains: a content; quantization level (after transrating of an encrypted video); and codec-type dependency to any distortion introduced. A further recommendation is that the Advanced Encryption Standard (AES) is preferred for SE to lightweight XOR encryption, despite it being taken up elsewhere as a real-time encryption method.
△ Less
Submitted 19 February, 2019;
originally announced February 2019.
-
Automatic Electrodes Detection during simultaneous EEG/fMRI acquisition
Authors:
Mathis Fleury,
Pierre Maurel,
Marsel Mano,
Elise Bannier,
Christian Barillot
Abstract:
Simultaneous EEG/fMRI acquisition allows to measure brain activity at high spatial-temporal resolution. The localisation of EEG sources depends on several parameters including the position of the electrodes on the scalp. The position of the MR electrodes during its acquisitions is obtained with the use of the UTE sequence allowing their visualisation. The retrieval of the electrodes consists in ob…
▽ More
Simultaneous EEG/fMRI acquisition allows to measure brain activity at high spatial-temporal resolution. The localisation of EEG sources depends on several parameters including the position of the electrodes on the scalp. The position of the MR electrodes during its acquisitions is obtained with the use of the UTE sequence allowing their visualisation. The retrieval of the electrodes consists in obtaining the volume where the electrodes are located by applying a sphere detection algorithm. We detect around 90% of electrodes for each subject, and our UTE-based electrode detection showed an average position error of 3.7mm for all subjects.
△ Less
Submitted 17 September, 2018;
originally announced September 2018.
-
A Fast Iterative Bayesian Inference Algorithm for Sparse Channel Estimation
Authors:
Niels Lovmand Pedersen,
Carles Navarro Manchón Bernard Henri Fleury
Abstract:
In this paper, we present a Bayesian channel estimation algorithm for multicarrier receivers based on pilot symbol observations. The inherent sparse nature of wireless multipath channels is exploited by modeling the prior distribution of multipath components' gains with a hierarchical representation of the Bessel K probability density function; a highly efficient, fast iterative Bayesian inference…
▽ More
In this paper, we present a Bayesian channel estimation algorithm for multicarrier receivers based on pilot symbol observations. The inherent sparse nature of wireless multipath channels is exploited by modeling the prior distribution of multipath components' gains with a hierarchical representation of the Bessel K probability density function; a highly efficient, fast iterative Bayesian inference method is then applied to the proposed model. The resulting estimator outperforms other state-of-the-art Bayesian and non-Bayesian estimators, either by yielding lower mean squared estimation error or by attaining the same accuracy with improved convergence rate, as shown in our numerical evaluation.
△ Less
Submitted 6 March, 2013;
originally announced March 2013.
