-
Verification of a Smart Contract for a Simple Casino
Authors:
Mark Utting,
Liam Kent
Abstract:
We describe the verification of an existing smart contract for a simple casino application, using the Whiley specification and programming language, with a fully automated verification engine based on Boogie and Z3. After finding and fixing several specification and code issues in the smart contract, we are able to verify all the operations of the smart contract.
We describe the verification of an existing smart contract for a simple casino application, using the Whiley specification and programming language, with a fully automated verification engine based on Boogie and Z3. After finding and fixing several specification and code issues in the smart contract, we are able to verify all the operations of the smart contract.
△ Less
Submitted 28 June, 2021;
originally announced June 2021.
-
Unsupervised Instance Selection with Low-Label, Supervised Learning for Outlier Detection
Authors:
Trent J. Bradberry,
Christopher H. Hase,
LeAnna Kent,
Joel A. Góngora
Abstract:
The laborious process of labeling data often bottlenecks projects that aim to leverage the power of supervised machine learning. Active Learning (AL) has been established as a technique to ameliorate this condition through an iterative framework that queries a human annotator for labels of instances with the most uncertain class assignment. Via this mechanism, AL produces a binary classifier train…
▽ More
The laborious process of labeling data often bottlenecks projects that aim to leverage the power of supervised machine learning. Active Learning (AL) has been established as a technique to ameliorate this condition through an iterative framework that queries a human annotator for labels of instances with the most uncertain class assignment. Via this mechanism, AL produces a binary classifier trained on less labeled data but with little, if any, loss in predictive performance. Despite its advantages, AL can have difficulty with class-imbalanced datasets and results in an inefficient labeling process. To address these drawbacks, we investigate our unsupervised instance selection (UNISEL) technique followed by a Random Forest (RF) classifier on 10 outlier detection datasets under low-label conditions. These results are compared to AL performed on the same datasets. Further, we investigate the combination of UNISEL and AL. Results indicate that UNISEL followed by an RF performs comparably to AL with an RF and that the combination of UNISEL and AL demonstrates superior performance. The practical implications of these findings in terms of time savings and generalizability afforded by UNISEL are discussed.
△ Less
Submitted 17 March, 2022; v1 submitted 26 April, 2021;
originally announced April 2021.
-
Towards automatic extractive text summarization of A-133 Single Audit reports with machine learning
Authors:
Vivian T. Chou,
LeAnna Kent,
Joel A. Góngora,
Sam Ballerini,
Carl D. Hoover
Abstract:
The rapid growth of text data has motivated the development of machine-learning based automatic text summarization strategies that concisely capture the essential ideas in a larger text. This study aimed to devise an extractive summarization method for A-133 Single Audits, which assess if recipients of federal grants are compliant with program requirements for use of federal funding. Currently, th…
▽ More
The rapid growth of text data has motivated the development of machine-learning based automatic text summarization strategies that concisely capture the essential ideas in a larger text. This study aimed to devise an extractive summarization method for A-133 Single Audits, which assess if recipients of federal grants are compliant with program requirements for use of federal funding. Currently, these voluminous audits must be manually analyzed by officials for oversight, risk management, and prioritization purposes. Automated summarization has the potential to streamline these processes. Analysis focused on the "Findings" section of ~20,000 Single Audits spanning 2016-2018. Following text preprocessing and GloVe embedding, sentence-level k-means clustering was performed to partition sentences by topic and to establish the importance of each sentence. For each audit, key summary sentences were extracted by proximity to cluster centroids. Summaries were judged by non-expert human evaluation and compared to human-generated summaries using the ROUGE metric. Though the goal was to fully automate summarization of A-133 audits, human input was required at various stages due to large variability in audit writing style, content, and context. Examples of human inputs include the number of clusters, the choice to keep or discard certain clusters based on their content relevance, and the definition of a top sentence. Overall, this approach made progress towards automated extractive summaries of A-133 audits, with future work to focus on full automation and improving summary consistency. This work highlights the inherent difficulty and subjective nature of automated summarization in a real-world application.
△ Less
Submitted 8 November, 2019;
originally announced November 2019.
