21793 research outputs found
Sort by
Comparative Analysis of Vision Transformers and CNNs in Melanoma Classification
Get PDFThe increasing number of skin cancers underscores the critical importance of early detection and accurate classification to improve treatment outcomes. Melanoma, a malignant skin cancer, has the highest mortality rate among all skin cancer types. Early detection of melanoma significantly enhances the chances of effective treatment and survival rates. This research presents a comparative analysis of cutting-edge deep learning methodologies in medical imaging, specifically focusing on Vision Transformers (ViT) and Convolutional Neural Networks (CNNs) for melanoma cancer detection. This study further examines the influence of domain-specific transfer learning on improving melanoma detection accuracy by pre-training these deep learning models on various datasets, such as ImageNet, BreakHis, and ISIC 2019. The models are then meticulously fine-tuned using a private annotated dataset of melanoma dermoscopic images. In addition, we employed the k-fold cross-validation technique to evaluate the reliability of our models. Our experimental results highlight the significant performance of advanced deep learning methodologies and transfer learning approaches, with the ViT-B16 model achieving an exceptional diagnostic accuracy of 97.97%, outperforming other models, specifically the pre-trained CNNs models. Moreover, This study highlights the critical role of large, diverse datasets in transfer learning, demonstrating their effectiveness in improving model performance for melanoma detection
Formalization of Partial Differential Equations using HOL Theorem Proving
Get PDFPartial Differential Equations (PDEs) are central for the mathematical modeling of many physical and engineering problems such as heat transfer, the flow of fluids and the radiation of electromagnetic waves. Solving these equations is essential for gaining precise insights into the behavior of such systems. Traditionally, the analysis of PDEs has been performed using paper-and-pencil based proofs or computer-based
numerical methods. However, these analysis techniques compromise the soundness and accuracy of their results, especially in safety-critical systems, due to the risk of human errors and inherent incompleteness of numerical algorithms. To address these limitations, we propose to use formal methods, in particular higher-order logic (HOL) theorem proving, for analyzing PDEs. The main motivation of this choice is the highly expressive and sound nature of HOL, which can be used to effectively model most systems that can be expressed in a closed mathematical form.
In this thesis, we introduce a comprehensive framework for the formal analysis of mathematical models of physical systems described by PDEs using the interactive proof assistant HOL Light. In particular, we have developed formal libraries for the heat, Laplace, telegrapher’s and wave equations. Each library includes the formalization of these PDEs, encompassing their formal definitions and the formal verification of some classical properties as well as their analytical solutions. These libraries constitute distinct contributions, each providing substantial value for various applications. To demonstrate the practical utility and effectiveness of our proposed framework, we conduct the formal analysis of several physical systems such as thermal protection, transmission lines, and potential flows
Machine Learning Approaches for Anomaly Detection and Load Forecasting in Smart Buildings Time Series Data
Get PDFThe proliferation of IoT sensors in smart buildings has enabled extensive time-series data collection, providing valuable insights for predictive maintenance, operational efficiency, and energy management. This data can be used within an anomaly detection framework to automatically identify abnormal behaviors, enabling the detection of issues related to power consumption, control system failures, and sensor malfunctions. Additionally, it supports load forecasting, crucial for optimizing energy management by enabling efficient resource allocation, cost savings, and sustainable operations through accurate demand prediction. However, IoT devices are prone to issues like hardware malfunctions and transmission errors, which introduce data anomalies and complicate the effective use of collected data. A popular and effective anomaly detection framework trains autoencoders on minimizing the error between original and reconstructed sequences. By setting a threshold on the reconstruction error, abnormal sequences can be distinguished from the predominant regular patterns. However, this method is highly sensitive to architectural parameters and the nature of anomalies, making it difficult to develop a universally effective method or fine-tune a model without prior knowledge of the building and sensors settings. To address this, we propose a reinforcement learning-based neural architecture search approach to explore a manually defined search space and identify the optimal neural configuration through trial and error. While this method demonstrates competitive performance in discovering effective architectures that may be not intuitive, it assumes the availability of anomaly-free data for training, which is not practical in real-world scenarios. Hence, we also present an unsupervised feature bank-based model for anomaly detection in anomaly-contaminated time series. We integrate this with a recurrent denoising autoencoder, trained on data deemed anomaly-free, to replace identified anomalies with plausible patterns. This results in a combined anomaly detection and imputation pipeline that preprocesses data for downstream tasks, such as forecasting, in which we compare the performance of different models before and after preprocessing and demonstrate significant improvements. Despite these advancements, data scarcity remains a challenge in training effective load forecasting models for smart buildings, specially that concerns over the privacy of IoT sensor data make building owners reluctant to share their data, whether for transfer learning or for centralized model training, as it can reveal sensitive information about the occupants’ behaviors. To overcome this limitation, we introduce a federated load forecasting framework to exploit data from multiple buildings while maintaining data privacy. Acknowledging the diverse load profiles shaped by factors like size, location, and user behavior, we also investigate existing techniques to personalize the global model to accommodate each building’s specific characteristics
Locally Everywhere: Production Cultures of Localization
Get PDFInto the second decade of the 21st century, global media distribution is increasingly defined by platforms. This dissertation examines media localization by looking at three distinct production contexts, and analyses the social role that localizers play in promoting global media content. The localization of global media involves interactions among three key social actors: media companies, exemplified by platforms; governments, represented by policymakers; and finally, the focus of this dissertation, localizers, who function as conduits for channeling content to the general public. Employing a blend of ethnography, interviews, and cultural policy analysis, this study seeks to provide a thicker description of how localizers create a sense of locality, and how they perceive their own roles within broader systems of media circulation.
Each of the three case studies presented in this dissertation represents a distinct subculture within media production. The Quebec dubbing industry and its politics of nation and dialect provides a starting point, as a traditional example of localization. Here, dubbers not only provide translation services but also position themselves as uniquely attuned to the sensitivities of local populations. I then follow with an examination of Indigenous mainstream media producers, and their attempts to broaden their reach to global viewers by “internationalizing” their content. This process is similar to the idea of localization because it also requires careful adaptation of content for its desired audience. The third case study is of fan translators and anime commentators, whose work facilitates the adoption of global anime into local contexts by providing customized promotion. The towering presences of platforms and cultural policies are never too far from the discussion, modulating in powerful ways the work and professional aims of each of these groups.
Through these snapshots, the aim of the dissertation is to highlight the role of localization and its practitioners in creating a sense of the “local” in mediascapes defined by free and unrestricted flows of information
Titanium Dioxide Nanotubes as Semiconducting Material in Applications of Solar Energy Conversion and Electrocatalysis
No full textNatural photosynthesis has inspired the development of direct and indirect approaches for solar energy conversion into chemical bonds. The use of chemical bonds to store solar energy is a promising approach to address the intermittency of the sun by harnessing sunlight to drive chemical transformations. One strategy to drive these processes is to use a bespoke semiconductor surface implemented in a photoelectrode to absorb light and generate charge carriers that can drive redox reactions such as the direct oxidation of adsorbed species on the photoanode. Dye-sensitized photoelectrochemical cells (DS-PECs), devices inspired by photosynthesis, are being developed to advance the goal of using the sun as the sole source of energy for converting abundant resources to fuel and valuable chemicals. Furthermore, electrocatalysis shows great promise to achieve the goal of transitioning from the production of energy using fossil fuels to clean and renewable energy sources.
Herein, this thesis describes using compact and vertically aligned titanium dioxide nanotubes as semiconducting materials for applications in both photoelectrochemistry and electrocatalysis. Functionalizing with a molecular copper(I) bis(diimine)-based donor-chromophore-acceptor assembly yields a photoanode capable of carrying out oxidative processes. Surface characterization and photoelectrochemical studies point to the nanotubes being intrinsically sensitized with carbon impurities such as carbon nitrides for visible light absorption. The ability of unfunctionalized and dye-sensitized photoanodes to drive oxidative processes is further confirmed photoelectrochemically and in the presence of a water oxidation catalyst where a Faradaic efficiency of 84% is found for O2 production. Titanium dioxide nanotubes with distinct morphologies arising from different electrolyte compositions used in the synthesis process are decorated with photoelectrochemically deposited CoOx and used as an electrocatalyst for hydrazine oxidation and as an electrochemical transducer for hydrazine sensing. Although a substantial amount of work remains to be done to assess the anode-supported electrocatalyst against other existing systems, the device shows promise for sensing hydrazine
Proof Recommendation for the HOL4 Theorem Prover
Get PDFInteractive theorem proving is a complex process that often requires significant expertise, user intervention and deep domain knowledge, making it challenging for users to construct valid proofs. The HOL4 theorem prover, while a powerful tool in formal verification, presents usability challenges due to the intricate nature of proofs and the cognitive load placed on users. This thesis proposes an innovative solution to enhance the accessibility and efficiency of interactive theorem proving through the development of an AI-driven Proof Recommendation System that leverages Large Language Models. The proposed methodology focuses on two primary tasks: proof step recommendation and complete proof generation. For the proof step recommendation, models such as BERT, RoBERTa, and T5 were fine-tuned on datasets derived from HOL4 theories to predict the next logical step(s) in the proof construction. This capability aims to guide users through the proof process, making it less daunting and more manageable, especially for those with a limited experience. In the proof generation task, sequence-to-sequence models, including MarianMT and T5, were utilized to generate complete proof sequences based on the given theorem statements. This task is particularly challenging due to a need to capture complex logical patterns and ensure the validity of the generated proofs. The training involved rigorous hyper-parameter tuning and evaluation to optimize the performance of models. Experimental results demonstrate that our proposed approach not only reduces the cognitive load on theorem provers but also enhances the efficiency and accessibility of interactive theorem proving compared to related work. The tool, called HOL4PRS, achieves significant accuracy in recommending proof steps and generating proof sequences, facilitating more widespread adoption of HOL4 in critical verification tasks across various industries. This thesis contributes to the field by showcasing how integrating AI into formal verification processes can significantly advance the capabilities and applications of the interactive theorem provers
Engineering transcriptional networks in Kluyveromyces marxianus to increase the stress tolerance of industrial bioprocessing strains
No full textBiomanufacturing uses engineered biological systems to produce valuable compounds from inexpensive materials like waste, reducing reliance on oil- and gas-based chemical production and promoting sustainable manufacturing. While many microbial species are used as hosts, non-conventional yeasts like Kluyveromyces marxianus have gained interest due to unique traits such as rapid growth, thermotolerance, and broad substrate utilization. Here, we investigated transcriptional networks in K. marxianus by engineering transcription factors (TFs) to enhance industrial stress tolerance. We compared two TF upregulation strategies: activation via fusion to viral activation domains (VPR and VP64) and overexpression via fusion to a strong promoter. Overexpression of the model TF KmGcn4p using the KmPDC1 promoter increased HIS3 expression 5-fold and significantly improved growth in the presence of the HIS3 inhibitor 3-AT. Transcriptomic analysis using Nanopore RNA-seq revealed that KmPDC1-driven overexpression of GCN4, HCM1, MSN2, and PDR1 produced differential gene expression across all three TF subclasses. Finally, to identify TFs directing stress tolerance, a high-throughput competition assay workflow was developed to screen barcoded TF libraries. In a library of 10 barcoded TFs, GCN4 and its haplotig allele (GCN4_hap) were found to be the “winner” TFs with increased frequencies of 0.7 and 1.8 (log2) under 70 mM of 3-AT. Future work will apply this pipeline to screen 291 overexpressed K. marxianus TFs under biomanufacturing-relevant stresses to identify TFs that can improve K. marxianus as an industrial bioprocessing strain
The Effect of Rehabilitative Care Provided to Individuals In an Inclusive Space Following Gender-Affirming Top Surgery
Get PDFGender-affirming top surgery is an important procedure for members of the 2SLGBTQIA+ community. There are currently no standardized aftercare recommendations nor consistent timelines for rehabilitation following top surgery. The purpose of our study was to measure patient-reported outcomes, including upper limb function, pain interference, neuropathic pain, embodiment, role limitations due to physical health, social functioning, and general health, in individuals receiving top surgery, over an 11-week rehabilitation program.
Forty-two gender diverse individuals from the general population participated. Participants started individualized rehabilitative aftercare 10-days post-operatively, which included one 60-minute treatment per week, for 11-weeks. The Disabilities of the Arm, Shoulder, and Hand scale (DASH) and 4 other questionnaires were completed prior to surgery, then again at weeks 1, 5, and 11 post-op. Separate repeated-measures analyses of variance (ANOVA) were used to identify differences in all measures among the 4 time points.
After top surgery individuals experience significant disruption to upper limb function, similar to other invasive upper extremity surgeries. During the rehabilitation, our participants experienced a significant statistical and clinical improvement in upper limb function while pain was not a limiting factor during the treatment. Participants reported avoiding about 3 less environments or social experiences which represents a clinically significant improvement in patient-reported embodiment.
The results of our study demonstrate the benefit of standard post-operative rehabilitative care in patients undergoing gender-affirming top surgery. The timeline for rehabilitative care used in this study can be applied, by qualified care providers, for future individuals who have undergone gender-affirming top surgery
Identity and Sense of Belonging in Second-Generation Immigrants of Montréal
Get PDFThis thesis presents a multilayered qualitative analysis of the identity and sense of belonging of second-generation immigrants in Montréal. Through a methodology consisting of individual interviews and focus groups, this research explores the everyday experiences of second- generation immigrants as they navigate various social relationships and negotiate colliding cultural environments. The conceptualization of second-generation immigration poses as an interesting theoretical issue for the understanding of different experiences of migration. Analyses of intergenerational relationships suggest that family members greatly influence second- generation immigrants’ identity and sense of belonging through multiple processes of socialization. Furthermore, within the context of this province, language is revealed as a meaningful feature of these individuals’ lives, as they navigate several language policies and different facets of the Québécois society. Lastly, the communities surrounding second-generation immigrants are immensely informative as to the construction and the evolution of sense of belonging. As second-generation immigrants recall being asked "Where are you from?", the strategies they mobilize to cultivate inclusion into different communities are telling about the discrimination that they experience. Second-generation immigrants show that they strongly connect to the Montrealer identity and sense of belonging, attachments that are stimulated by the presence of ethnic and cultural diversity in the city. Through the above-mentioned concepts, this thesis shows that identity and sense of belonging are hybrid, fluid and multiple, as they are continuously constructed and evolving alongside everyday interactions
Enhancing Conflict Resolution in the TRIZ Method Using ATDM
No full textThe significance of innovation in enhancing and strengthening businesses and industries is increasingly evident in today’s competitive market. A key area within design science involves the study and development of creative design methodologies that assist designers in structuring creative processes and systematically addressing design problems.
Among the various design methodologies proposed, TRIZ, developed by Genrich Altshuller in Russia in 1956, stands out as one of the most influential. TRIZ focuses on defining a design problem, extracting the inherent conflicts (contradictions), and employing specific tools to systematically generate solutions.
In recent decades, extensive research has been conducted on TRIZ, predominantly employing an inductive approach. Researchers have typically designed experiments and case studies to analyze and refine TRIZ. While this approach has its merits, it requires substantial resources and time for execution and analysis, and the conclusions drawn are often confined to the specific contexts of those experiments. In contrast, this thesis adopts a deductive approach to study, analyze, and enhance TRIZ. Rather than focusing on the design of experiments and tests, we concentrate on axioms, proofs, and principles, utilizing logic and reasoning to analyze TRIZ and draw conclusions regarding its mechanism for resolving design conflicts. This unique approach not only advances TRIZ as a creative design methodology but also presents a systematic strategy that could potentially be applied to the development of other design methodologies.
In this thesis, we pursued three main objectives. Firstly, we analyzed TRIZ through a deductive framework known as the TASKS framework to explore how it can foster a creative environment for designers. Our analysis identified the key barriers and enablers of TRIZ that influence designers during the design process. This examination of TRIZ's limitations and weaknesses raises an important question: how can we scientifically and systematically enhance a creative design methodology like TRIZ? Therefore, the second objective of this study was to propose a deductive method grounded in the Axiomatic Theory of Design Modeling (ATDM), aimed at systematically improving creative design methodologies such as TRIZ. Employing this method could save design researchers both time and resources in analyzing creative design methodologies and developing strategies for their advancement. Through the application of this proposed method, we clarified how TRIZ could be further developed.
Finally, the third objective of this thesis was to introduce and evaluate a new iteration of TRIZ that integrates Environment Based Design (EBD) and utilizes Large Language Models (LLMs). As part of this contribution, we leveraged LLMs to introduce a conceptual design chatbot based on TRIZ and EBD. In this model, the designer inputs a design problem, and the chatbot generates systematic questions following the principles of EBD. The designer and the LLM then respond to these questions. The chatbot processes the answers according to EBD principles, which are subsequently used to perform functional analysis. Ultimately, a conflict (or contradiction) is identified within the functional analysis, and the LLM employs TRIZ principles to generate solutions and suggest a team of experts to execute the project. The evaluation of this LLM-based conceptual design chatbot demonstrated its effectiveness in addressing design problems and generating accurate and comprehensive outputs