Search | arXiv e-print repository

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>  <link rel="apple-touch-icon" sizes="180x180" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/apple-touch-icon.png"> <link rel="icon" type="image/png" sizes="32x32" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-32x32.png"> <link rel="icon" type="image/png" sizes="16x16" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-16x16.png"> <link rel="manifest" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/site.webmanifest"> <link rel="mask-icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/safari-pinned-tab.svg" color="#b31b1b"> <link rel="shortcut icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon.ico"> <meta name="msapplication-TileColor" content="#b31b1b"> <meta name="msapplication-config" content="images/icons/browserconfig.xml"> <meta name="theme-color" content="#b31b1b">  <title>Search | arXiv e-print repository</title> <script defer src="https://static.arxiv.org/static/base/1.0.0a5/fontawesome-free-5.11.2-web/js/all.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/base/1.0.0a5/css/arxivstyle.css" /> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ messageStyle: "none", extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"], tex2jax: { inlineMath: [ ['$','$'], ["\$","\$"] ], displayMath: [ ['$$','$$'], ["\\[","\\]"] ], processEscapes: true, ignoreClass: '.*', processClass: 'mathjax.*' }, TeX: { extensions: ["AMSmath.js", "AMSsymbols.js", "noErrors.js"], noErrors: { inlineDelimiters: ["$","$"], multiLine: false, style: { "font-size": "normal", "border": "" } } }, "HTML-CSS": { availableFonts: ["TeX"] } }); </script> <script src='//static.arxiv.org/MathJax-2.7.3/MathJax.js'></script> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/notification.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/bulma-tooltip.min.css" /> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/search.css" /> <script src="https://code.jquery.com/jquery-3.2.1.slim.min.js" integrity="sha256-k2WSCIexGzOj3Euiig+TlR8gA0EmPjuc79OEeY5L45g=" crossorigin="anonymous"></script> <script src="https://static.arxiv.org/static/search/0.5.6/js/fieldset.js"></script> <style> radio#cf-customfield_11400 { display: none; } </style> </head> <body> <header><a href="#main-container" class="is-sr-only">Skip to main content</a>  <div class="attribution level is-marginless" role="banner"> <div class="level-left"> <a class="level-item" href="https://cornell.edu/"><img src="https://static.arxiv.org/static/base/1.0.0a5/images/cornell-reduced-white-SMALL.svg" alt="Cornell University" width="200" aria-label="logo" /></a> </div> <div class="level-right is-marginless"><p class="sponsors level-item is-marginless"><span id="support-ack-url">We gratefully acknowledge support from<br /> the Simons Foundation, <a href="https://info.arxiv.org/about/ourmembers.html">member institutions</a>, and all contributors. <a href="https://info.arxiv.org/about/donate.html">Donate</a></span></p></div> </div>  <div class="identity level is-marginless"> <div class="level-left"> <div class="level-item"> <a class="arxiv" href="https://arxiv.org/" aria-label="arxiv-logo"> <img src="https://static.arxiv.org/static/base/1.0.0a5/images/arxiv-logo-one-color-white.svg" aria-label="logo" alt="arxiv logo" width="85" style="width:85px;"/> </a> </div> </div> <div class="search-block level-right"> <form class="level-item mini-search" method="GET" action="https://arxiv.org/search"> <div class="field has-addons"> <div class="control"> <input class="input is-small" type="text" name="query" placeholder="Search..." aria-label="Search term or terms" /> <p class="help"><a href="https://info.arxiv.org/help">Help</a> | <a href="https://arxiv.org/search/advanced">Advanced Search</a></p> </div> <div class="control"> <div class="select is-small"> <select name="searchtype" aria-label="Field to search"> <option value="all" selected="selected">All fields</option> <option value="title">Title</option> <option value="author">Author</option> <option value="abstract">Abstract</option> <option value="comments">Comments</option> <option value="journal_ref">Journal reference</option> <option value="acm_class">ACM classification</option> <option value="msc_class">MSC classification</option> <option value="report_num">Report number</option> <option value="paper_id">arXiv identifier</option> <option value="doi">DOI</option> <option value="orcid">ORCID</option> <option value="author_id">arXiv author ID</option> <option value="help">Help pages</option> <option value="full_text">Full text</option> </select> </div> </div> <input type="hidden" name="source" value="header"> <button class="button is-small is-cul-darker">Search</button> </div> </form> </div> </div>  <div class="container"> <div class="user-tools is-size-7 has-text-right has-text-weight-bold" role="navigation" aria-label="User menu"> <a href="https://arxiv.org/login">Login</a> </div> </div> </header> <main class="container" id="main-container"> <div class="level is-marginless"> <div class="level-left"> <h1 class="title is-clearfix"> Showing 1–50 of 58 results for author: <span class="mathjax">Bauer, A</span> </h1> </div> <div class="level-right is-hidden-mobile">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> <div class="content"> <form method="GET" action="/search/cs" aria-role="search"> Searching in archive <strong>cs</strong>. <a href="/search/?searchtype=author&query=Bauer%2C+A">Search in all archives.</a> <div class="field has-addons-tablet"> <div class="control is-expanded"> <label for="query" class="hidden-label">Search term or terms</label> <input class="input is-medium" id="query" name="query" placeholder="Search term..." type="text" value="Bauer, A"> </div> <div class="select control is-medium"> <label class="is-hidden" for="searchtype">Field</label> <select class="is-medium" id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> </div> <div class="control"> <button class="button is-link is-medium">Search</button> </div> </div> <div class="field"> <div class="control is-size-7"> <label class="radio"> <input checked id="abstracts-0" name="abstracts" type="radio" value="show"> Show abstracts </label> <label class="radio"> <input id="abstracts-1" name="abstracts" type="radio" value="hide"> Hide abstracts </label> </div> </div> <div class="is-clearfix" style="height: 2.5em"> <div class="is-pulled-right"> <a href="/search/advanced?terms-0-term=Bauer%2C+A&terms-0-field=author&size=50&order=-announced_date_first">Advanced Search</a> </div> </div> <input type="hidden" name="order" value="-announced_date_first"> <input type="hidden" name="size" value="50"> </form> <div class="level breathe-horizontal"> <div class="level-left"> <form method="GET" action="/search/"> <div style="display: none;"> <select id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> <input id="query" name="query" type="text" value="Bauer, A"> <ul id="abstracts"><li><input checked id="abstracts-0" name="abstracts" type="radio" value="show"> <label for="abstracts-0">Show abstracts</label></li><li><input id="abstracts-1" name="abstracts" type="radio" value="hide"> <label for="abstracts-1">Hide abstracts</label></li></ul> </div> <div class="box field is-grouped is-grouped-multiline level-item"> <div class="control"> <span class="select is-small"> <select id="size" name="size"><option value="25">25</option><option selected value="50">50</option><option value="100">100</option><option value="200">200</option></select> </span> <label for="size">results per page</label>. </div> <div class="control"> <label for="order">Sort results by</label> <span class="select is-small"> <select id="order" name="order"><option selected value="-announced_date_first">Announcement date (newest first)</option><option value="announced_date_first">Announcement date (oldest first)</option><option value="-submitted_date">Submission date (newest first)</option><option value="submitted_date">Submission date (oldest first)</option><option value="">Relevance</option></select> </span> </div> <div class="control"> <button class="button is-small is-link">Go</button> </div> </div> </form> </div> </div> <nav class="pagination is-small is-centered breathe-horizontal" role="navigation" aria-label="pagination"> <a href="" class="pagination-previous is-invisible">Previous </a> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=50" class="pagination-next" >Next </a> <ul class="pagination-list"> <li> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=0" class="pagination-link is-current" aria-label="Goto page 1">1 </a> </li> <li> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=50" class="pagination-link " aria-label="Page 2" aria-current="page">2 </a> </li> </ul> </nav> <ol class="breathe-horizontal" start="1"> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2409.17664">arXiv:2409.17664</a> <span> [<a href="https://arxiv.org/pdf/2409.17664">pdf</a>, <a href="https://arxiv.org/ps/2409.17664">ps</a>, <a href="https://arxiv.org/format/2409.17664">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Category Theory">math.CT</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> </div> </div> <p class="title is-5 mathjax"> Comodule Representations of Second-Order Functionals </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ahman%2C+D">Danel Ahman</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2409.17664v1-abstract-short" style="display: inline;"> We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally subsumes classic representations of continuous functionals with well-founded trees. We find other kinds of representations by varying the monad, the comodule, and in… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.17664v1-abstract-full').style.display = 'inline'; document.getElementById('2409.17664v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2409.17664v1-abstract-full" style="display: none;"> We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally subsumes classic representations of continuous functionals with well-founded trees. We find other kinds of representations by varying the monad, the comodule, and in some cases the underlying category of containers. Examples include uniformly continuous or finitely supported functionals, functionals querying their arguments precisely once, or at most once, functionals interacting with an ambient environment through computational effects, as well as functionals trivially representing themselves. Many of these rely on our construction of a monad on containers from a monad on shapes and a weak Mendler-style monad algebra on the universe for positions. We show that comodule representability on the category of propositional containers, which have positions valued in a universe of propositions, is closely related to instance reducibility in constructive mathematics, and through it to Weihrauch reducibility in computability theory. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.17664v1-abstract-full').style.display = 'none'; document.getElementById('2409.17664v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 September, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2409.11946">arXiv:2409.11946</a> <span> [<a href="https://arxiv.org/pdf/2409.11946">pdf</a>, <a href="https://arxiv.org/format/2409.11946">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> An Imperative Language for Verified Exact Real-Number Computation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Park%2C+S">Sewon Park</a>, <a href="/search/cs?searchtype=author&query=Simpson%2C+A">Alex Simpson</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2409.11946v1-abstract-short" style="display: inline;"> We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real numbers as limits of Cauchy sequences. We address the semidecidability of the linear ordering of the reals by incorporating nondeterministic guarded choice, through which decisions based on partial comparison operations… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.11946v1-abstract-full').style.display = 'inline'; document.getElementById('2409.11946v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2409.11946v1-abstract-full" style="display: none;"> We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real numbers as limits of Cauchy sequences. We address the semidecidability of the linear ordering of the reals by incorporating nondeterministic guarded choice, through which decisions based on partial comparison operations on reals can be patched together to give total programs. The interplay between mutable state, nondeterminism, and computation of limits is controlled by the requirement that expressions computing limits and guards modify only local state. We devise a domain-theoretic denotational semantics that uses a variant of Plotkin powerdomain construction tailored to our specific version of nondeterminism. We formulate a Hoare-style specification logic, show that it is sound for the denotational semantics, and illustrate the setup by implementing and proving correct a program for computation of $蟺$ as the least positive zero of $\sin$. The modular character of Clerical allows us to compose the program from smaller parts, each of which is shown to be correct on its own. We provide a proof-of-concept OCaml implementation of Clerical, and formally verify parts of the development, notably the soundness of specification logic, in the Coq proof assistant. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.11946v1-abstract-full').style.display = 'none'; document.getElementById('2409.11946v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 September, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2409.07566">arXiv:2409.07566</a> <span> [<a href="https://arxiv.org/pdf/2409.07566">pdf</a>, <a href="https://arxiv.org/format/2409.07566">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> EchoDFKD: Data-Free Knowledge Distillation for Cardiac Ultrasound Segmentation using Synthetic Data </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Petit%2C+G">Gr茅goire Petit</a>, <a href="/search/cs?searchtype=author&query=Palluau%2C+N">Nathan Palluau</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Axel Bauer</a>, <a href="/search/cs?searchtype=author&query=Dlaska%2C+C">Clemens Dlaska</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2409.07566v1-abstract-short" style="display: inline;"> The application of machine learning to medical ultrasound videos of the heart, i.e., echocardiography, has recently gained traction with the availability of large public datasets. Traditional supervised tasks, such as ejection fraction regression, are now making way for approaches focusing more on the latent structure of data distributions, as well as generative methods. We propose a model trained… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.07566v1-abstract-full').style.display = 'inline'; document.getElementById('2409.07566v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2409.07566v1-abstract-full" style="display: none;"> The application of machine learning to medical ultrasound videos of the heart, i.e., echocardiography, has recently gained traction with the availability of large public datasets. Traditional supervised tasks, such as ejection fraction regression, are now making way for approaches focusing more on the latent structure of data distributions, as well as generative methods. We propose a model trained exclusively by knowledge distillation, either on real or synthetical data, involving retrieving masks suggested by a teacher model. We achieve state-of-the-art (SOTA) values on the task of identifying end-diastolic and end-systolic frames. By training the model only on synthetic data, it reaches segmentation capabilities close to the performance when trained on real data with a significantly reduced number of weights. A comparison with the 5 main existing methods shows that our method outperforms the others in most cases. We also present a new evaluation method that does not require human annotation and instead relies on a large auxiliary model. We show that this method produces scores consistent with those obtained from human annotations. Relying on the integrated knowledge from a vast amount of records, this method overcomes certain inherent limitations of human annotator labeling. Code: https://github.com/GregoirePetit/EchoDFKD <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.07566v1-abstract-full').style.display = 'none'; document.getElementById('2409.07566v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 September, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2407.11432">arXiv:2407.11432</a> <span> [<a href="https://arxiv.org/pdf/2407.11432">pdf</a>, <a href="https://arxiv.org/format/2407.11432">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> Octopus: Experiences with a Hybrid Event-Driven Architecture for Distributed Scientific Computing </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Pan%2C+H">Haochen Pan</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+R">Ryan Chard</a>, <a href="/search/cs?searchtype=author&query=Zhou%2C+S">Sicheng Zhou</a>, <a href="/search/cs?searchtype=author&query=Kamatar%2C+A">Alok Kamatar</a>, <a href="/search/cs?searchtype=author&query=Vescovi%2C+R">Rafael Vescovi</a>, <a href="/search/cs?searchtype=author&query=Hayot-Sasson%2C+V">Val茅rie Hayot-Sasson</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Gonthier%2C+M">Maxime Gonthier</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2407.11432v2-abstract-short" style="display: inline;"> Scientific research increasingly relies on distributed computational resources, storage systems, networks, and instruments, ranging from HPC and cloud systems to edge devices. Event-driven architecture (EDA) benefits applications targeting distributed research infrastructures by enabling the organization, communication, processing, reliability, and security of events generated from many sources. T… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2407.11432v2-abstract-full').style.display = 'inline'; document.getElementById('2407.11432v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2407.11432v2-abstract-full" style="display: none;"> Scientific research increasingly relies on distributed computational resources, storage systems, networks, and instruments, ranging from HPC and cloud systems to edge devices. Event-driven architecture (EDA) benefits applications targeting distributed research infrastructures by enabling the organization, communication, processing, reliability, and security of events generated from many sources. To support the development of scientific EDA, we introduce Octopus, a hybrid, cloud-to-edge event fabric designed to link many local event producers and consumers with cloud-hosted brokers. Octopus can be scaled to meet demand, permits the deployment of highly available Triggers for automatic event processing, and enforces fine-grained access control. We identify requirements in self-driving laboratories, scientific data automation, online task scheduling, epidemic modeling, and dynamic workflow management use cases, and present results demonstrating Octopus' ability to meet those requirements. Octopus supports producing and consuming events at a rate of over 4.2 M and 9.6 M events per second, respectively, from distributed clients. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2407.11432v2-abstract-full').style.display = 'none'; document.getElementById('2407.11432v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 September, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 16 July, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">12 pages and 8 figures. Camera-ready version for FTXS'24 (https://sites.google.com/view/ftxs2024)</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2407.01764">arXiv:2407.01764</a> <span> [<a href="https://arxiv.org/pdf/2407.01764">pdf</a>, <a href="https://arxiv.org/format/2407.01764">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> Object Proxy Patterns for Accelerating Distributed Applications </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Pauloski%2C+J+G">J. Gregory Pauloski</a>, <a href="/search/cs?searchtype=author&query=Hayot-Sasson%2C+V">Valerie Hayot-Sasson</a>, <a href="/search/cs?searchtype=author&query=Ward%2C+L">Logan Ward</a>, <a href="/search/cs?searchtype=author&query=Brace%2C+A">Alexander Brace</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2407.01764v1-abstract-short" style="display: inline;"> Workflow and serverless frameworks have empowered new approaches to distributed application design by abstracting compute resources. However, their typically limited or one-size-fits-all support for advanced data flow patterns leaves optimization to the application programmer -- optimization that becomes more difficult as data become larger. The transparent object proxy, which provides wide-area r… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2407.01764v1-abstract-full').style.display = 'inline'; document.getElementById('2407.01764v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2407.01764v1-abstract-full" style="display: none;"> Workflow and serverless frameworks have empowered new approaches to distributed application design by abstracting compute resources. However, their typically limited or one-size-fits-all support for advanced data flow patterns leaves optimization to the application programmer -- optimization that becomes more difficult as data become larger. The transparent object proxy, which provides wide-area references that can resolve to data regardless of location, has been demonstrated as an effective low-level building block in such situations. Here we propose three high-level proxy-based programming patterns -- distributed futures, streaming, and ownership -- that make the power of the proxy pattern usable for more complex and dynamic distributed program structures. We motivate these patterns via careful review of application requirements and describe implementations of each pattern. We evaluate our implementations through a suite of benchmarks and by applying them in three substantial scientific applications, in which we demonstrate substantial improvements in runtime, throughput, and memory usage. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2407.01764v1-abstract-full').style.display = 'none'; document.getElementById('2407.01764v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 July, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2406.17710">arXiv:2406.17710</a> <span> [<a href="https://arxiv.org/pdf/2406.17710">pdf</a>, <a href="https://arxiv.org/format/2406.17710">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> GreenFaaS: Maximizing Energy Efficiency of HPC Workloads with FaaS </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Kamatar%2C+A">Alok Kamatar</a>, <a href="/search/cs?searchtype=author&query=Hayot-Sasson%2C+V">Valerie Hayot-Sasson</a>, <a href="/search/cs?searchtype=author&query=Babuji%2C+Y">Yadu Babuji</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andre Bauer</a>, <a href="/search/cs?searchtype=author&query=Rattihalli%2C+G">Gourav Rattihalli</a>, <a href="/search/cs?searchtype=author&query=Hogade%2C+N">Ninad Hogade</a>, <a href="/search/cs?searchtype=author&query=Milojicic%2C+D">Dejan Milojicic</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2406.17710v1-abstract-short" style="display: inline;"> Application energy efficiency can be improved by executing each application component on the compute element that consumes the least energy while also satisfying time constraints. In principle, the function as a service (FaaS) paradigm should simplify such optimizations by abstracting away compute location, but existing FaaS systems do not provide for user transparency over application energy cons… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2406.17710v1-abstract-full').style.display = 'inline'; document.getElementById('2406.17710v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2406.17710v1-abstract-full" style="display: none;"> Application energy efficiency can be improved by executing each application component on the compute element that consumes the least energy while also satisfying time constraints. In principle, the function as a service (FaaS) paradigm should simplify such optimizations by abstracting away compute location, but existing FaaS systems do not provide for user transparency over application energy consumption or task placement. Here we present GreenFaaS, a novel open source framework that bridges this gap between energy-efficient applications and FaaS platforms. GreenFaaS can be deployed by end users or providers across systems to monitor energy use, provide task-specific feedback, and schedule tasks in an energy-aware manner. We demonstrate that intelligent placement of tasks can both reduce energy consumption and improve performance. For a synthetic workload, GreenFaaS reduces the energy-delay product by 45% compared to alternatives. Furthermore, running a molecular design application through GreenFaaS can reduce energy consumption by 21% and runtime by 63% by better matching tasks with machines. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2406.17710v1-abstract-full').style.display = 'none'; document.getElementById('2406.17710v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 25 June, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">11 pages, 10 figures</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2405.15828">arXiv:2405.15828</a> <span> [<a href="https://arxiv.org/pdf/2405.15828">pdf</a>, <a href="https://arxiv.org/format/2405.15828">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Digital Libraries">cs.DL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> </div> </div> <p class="title is-5 mathjax"> Oil & Water? Diffusion of AI Within and Across Scientific Fields </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Duede%2C+E">Eamon Duede</a>, <a href="/search/cs?searchtype=author&query=Dolan%2C+W">William Dolan</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a>, <a href="/search/cs?searchtype=author&query=Lakhani%2C+K">Karim Lakhani</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2405.15828v1-abstract-short" style="display: inline;"> This study empirically investigates claims of the increasing ubiquity of artificial intelligence (AI) within roughly 80 million research publications across 20 diverse scientific fields, by examining the change in scholarly engagement with AI from 1985 through 2022. We observe exponential growth, with AI-engaged publications increasing approximately thirteenfold (13x) across all fields, suggesting… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.15828v1-abstract-full').style.display = 'inline'; document.getElementById('2405.15828v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2405.15828v1-abstract-full" style="display: none;"> This study empirically investigates claims of the increasing ubiquity of artificial intelligence (AI) within roughly 80 million research publications across 20 diverse scientific fields, by examining the change in scholarly engagement with AI from 1985 through 2022. We observe exponential growth, with AI-engaged publications increasing approximately thirteenfold (13x) across all fields, suggesting a dramatic shift from niche to mainstream. Moreover, we provide the first empirical examination of the distribution of AI-engaged publications across publication venues within individual fields, with results that reveal a broadening of AI engagement within disciplines. While this broadening engagement suggests a move toward greater disciplinary integration in every field, increased ubiquity is associated with a semantic tension between AI-engaged research and more traditional disciplinary research. Through an analysis of tens of millions of document embeddings, we observe a complex interplay between AI-engaged and non-AI-engaged research within and across fields, suggesting that increasing ubiquity is something of an oil-and-water phenomenon -- AI-engaged work is spreading out over fields, but not mixing well with non-AI-engaged work. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.15828v1-abstract-full').style.display = 'none'; document.getElementById('2405.15828v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 23 May, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2405.11965">arXiv:2405.11965</a> <span> [<a href="https://arxiv.org/pdf/2405.11965">pdf</a>, <a href="https://arxiv.org/ps/2405.11965">ps</a>, <a href="https://arxiv.org/format/2405.11965">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> No Free Lunch: Research Software Testing in Teaching </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Dorner%2C+M">Michael Dorner</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=Angermeir%2C+F">Florian Angermeir</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2405.11965v1-abstract-short" style="display: inline;"> Software is at the core of most scientific discoveries today. Therefore, the quality of research results highly depends on the quality of the research software. Rigorous testing, as we know it from software engineering in the industry, could ensure the quality of the research software but it also requires a substantial effort that is often not rewarded in academia. Therefore, this research explore… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.11965v1-abstract-full').style.display = 'inline'; document.getElementById('2405.11965v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2405.11965v1-abstract-full" style="display: none;"> Software is at the core of most scientific discoveries today. Therefore, the quality of research results highly depends on the quality of the research software. Rigorous testing, as we know it from software engineering in the industry, could ensure the quality of the research software but it also requires a substantial effort that is often not rewarded in academia. Therefore, this research explores the effects of research software testing integrated into teaching on research software. In an in-vivo experiment, we integrated the engineering of a test suite for a large-scale network simulation as group projects into a course on software testing at the Blekinge Institute of Technology, Sweden, and qualitatively measured the effects of this integration on the research software. We found that the research software benefited from the integration through substantially improved documentation and fewer hardware and software dependencies. However, this integration was effortful and although the student teams developed elegant and thoughtful test suites, no code by students went directly into the research software since we were not able to make the integration back into the research software obligatory or even remunerative. Although we strongly believe that integrating research software engineering such as testing into teaching is not only valuable for the research software itself but also for students, the research of the next generation, as they get in touch with research software engineering and bleeding-edge research in their field as part of their education, the uncertainty about the intellectual properties of students' code substantially limits the potential of integrating research software testing into teaching. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.11965v1-abstract-full').style.display = 'none'; document.getElementById('2405.11965v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 20 May, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2402.03480">arXiv:2402.03480</a> <span> [<a href="https://arxiv.org/pdf/2402.03480">pdf</a>, <a href="https://arxiv.org/format/2402.03480">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> Trillion Parameter AI Serving Infrastructure for Scientific Discovery: A Survey and Vision </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Hudson%2C+N">Nathaniel Hudson</a>, <a href="/search/cs?searchtype=author&query=Pauloski%2C+J+G">J. Gregory Pauloski</a>, <a href="/search/cs?searchtype=author&query=Baughman%2C+M">Matt Baughman</a>, <a href="/search/cs?searchtype=author&query=Kamatar%2C+A">Alok Kamatar</a>, <a href="/search/cs?searchtype=author&query=Sakarvadia%2C+M">Mansi Sakarvadia</a>, <a href="/search/cs?searchtype=author&query=Ward%2C+L">Logan Ward</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+R">Ryan Chard</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Levental%2C+M">Maksim Levental</a>, <a href="/search/cs?searchtype=author&query=Wang%2C+W">Wenyi Wang</a>, <a href="/search/cs?searchtype=author&query=Engler%2C+W">Will Engler</a>, <a href="/search/cs?searchtype=author&query=Skelly%2C+O+P">Owen Price Skelly</a>, <a href="/search/cs?searchtype=author&query=Blaiszik%2C+B">Ben Blaiszik</a>, <a href="/search/cs?searchtype=author&query=Stevens%2C+R">Rick Stevens</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2402.03480v1-abstract-short" style="display: inline;"> Deep learning methods are transforming research, enabling new techniques, and ultimately leading to new discoveries. As the demand for more capable AI models continues to grow, we are now entering an era of Trillion Parameter Models (TPM), or models with more than a trillion parameters -- such as Huawei's PanGu-$危$. We describe a vision for the ecosystem of TPM users and providers that caters to t… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2402.03480v1-abstract-full').style.display = 'inline'; document.getElementById('2402.03480v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2402.03480v1-abstract-full" style="display: none;"> Deep learning methods are transforming research, enabling new techniques, and ultimately leading to new discoveries. As the demand for more capable AI models continues to grow, we are now entering an era of Trillion Parameter Models (TPM), or models with more than a trillion parameters -- such as Huawei's PanGu-$危$. We describe a vision for the ecosystem of TPM users and providers that caters to the specific needs of the scientific community. We then outline the significant technical challenges and open problems in system design for serving TPMs to enable scientific research and discovery. Specifically, we describe the requirements of a comprehensive software stack and interfaces to support the diverse and flexible requirements of researchers. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2402.03480v1-abstract-full').style.display = 'none'; document.getElementById('2402.03480v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 5 February, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">10 pages, 3 figures, accepted for publication in the proceedings of the 10th IEEE/ACM International Conference on Big Data Computing, Applications and Technologies (BDCAT2023)</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2401.02524">arXiv:2401.02524</a> <span> [<a href="https://arxiv.org/pdf/2401.02524">pdf</a>, <a href="https://arxiv.org/format/2401.02524">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> Comprehensive Exploration of Synthetic Data Generation: A Survey </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Trapp%2C+S">Simon Trapp</a>, <a href="/search/cs?searchtype=author&query=Stenger%2C+M">Michael Stenger</a>, <a href="/search/cs?searchtype=author&query=Leppich%2C+R">Robert Leppich</a>, <a href="/search/cs?searchtype=author&query=Kounev%2C+S">Samuel Kounev</a>, <a href="/search/cs?searchtype=author&query=Leznik%2C+M">Mark Leznik</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2401.02524v2-abstract-short" style="display: inline;"> Recent years have witnessed a surge in the popularity of Machine Learning (ML), applied across diverse domains. However, progress is impeded by the scarcity of training data due to expensive acquisition and privacy legislation. Synthetic data emerges as a solution, but the abundance of released models and limited overview literature pose challenges for decision-making. This work surveys 417 Synthe… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.02524v2-abstract-full').style.display = 'inline'; document.getElementById('2401.02524v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2401.02524v2-abstract-full" style="display: none;"> Recent years have witnessed a surge in the popularity of Machine Learning (ML), applied across diverse domains. However, progress is impeded by the scarcity of training data due to expensive acquisition and privacy legislation. Synthetic data emerges as a solution, but the abundance of released models and limited overview literature pose challenges for decision-making. This work surveys 417 Synthetic Data Generation (SDG) models over the last decade, providing a comprehensive overview of model types, functionality, and improvements. Common attributes are identified, leading to a classification and trend analysis. The findings reveal increased model performance and complexity, with neural network-based approaches prevailing, except for privacy-preserving data generation. Computer vision dominates, with GANs as primary generative models, while diffusion models, transformers, and RNNs compete. Implications from our performance evaluation highlight the scarcity of common metrics and datasets, making comparisons challenging. Additionally, the neglect of training and computational costs in literature necessitates attention in future research. This work serves as a guide for SDG model selection and identifies crucial areas for future exploration. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.02524v2-abstract-full').style.display = 'none'; document.getElementById('2401.02524v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 February, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 4 January, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Fixed bug in Figure 44</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2312.15825">arXiv:2312.15825</a> <span> [<a href="https://arxiv.org/pdf/2312.15825">pdf</a>, <a href="https://arxiv.org/ps/2312.15825">ps</a>, <a href="https://arxiv.org/format/2312.15825">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computational Engineering, Finance, and Science">cs.CE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Comparative Analysis of Radiomic Features and Gene Expression Profiles in Histopathology Data Using Graph Neural Networks </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Monroy%2C+L+C+R">Luis Carlos Rivera Monroy</a>, <a href="/search/cs?searchtype=author&query=Rist%2C+L">Leonhard Rist</a>, <a href="/search/cs?searchtype=author&query=Eberhardt%2C+M">Martin Eberhardt</a>, <a href="/search/cs?searchtype=author&query=Ostalecki%2C+C">Christian Ostalecki</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=Vera%2C+J">Julio Vera</a>, <a href="/search/cs?searchtype=author&query=Breininger%2C+K">Katharina Breininger</a>, <a href="/search/cs?searchtype=author&query=Maier%2C+A">Andreas Maier</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2312.15825v1-abstract-short" style="display: inline;"> This study leverages graph neural networks to integrate MELC data with Radiomic-extracted features for melanoma classification, focusing on cell-wise analysis. It assesses the effectiveness of gene expression profiles and Radiomic features, revealing that Radiomic features, particularly when combined with UMAP for dimensionality reduction, significantly enhance classification performance. Notably,… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2312.15825v1-abstract-full').style.display = 'inline'; document.getElementById('2312.15825v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2312.15825v1-abstract-full" style="display: none;"> This study leverages graph neural networks to integrate MELC data with Radiomic-extracted features for melanoma classification, focusing on cell-wise analysis. It assesses the effectiveness of gene expression profiles and Radiomic features, revealing that Radiomic features, particularly when combined with UMAP for dimensionality reduction, significantly enhance classification performance. Notably, using Radiomics contributes to increased diagnostic accuracy and computational efficiency, as it allows for the extraction of critical data from fewer stains, thereby reducing operational costs. This methodology marks an advancement in computational dermatology for melanoma cell classification, setting the stage for future research and potential developments. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2312.15825v1-abstract-full').style.display = 'none'; document.getElementById('2312.15825v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 25 December, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Paper accepted at the German Conference on Medical Image Computing 2024</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2310.16270">arXiv:2310.16270</a> <span> [<a href="https://arxiv.org/pdf/2310.16270">pdf</a>, <a href="https://arxiv.org/format/2310.16270">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computation and Language">cs.CL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Attention Lens: A Tool for Mechanistically Interpreting the Attention Head Information Retrieval Mechanism </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Sakarvadia%2C+M">Mansi Sakarvadia</a>, <a href="/search/cs?searchtype=author&query=Khan%2C+A">Arham Khan</a>, <a href="/search/cs?searchtype=author&query=Ajith%2C+A">Aswathy Ajith</a>, <a href="/search/cs?searchtype=author&query=Grzenda%2C+D">Daniel Grzenda</a>, <a href="/search/cs?searchtype=author&query=Hudson%2C+N">Nathaniel Hudson</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2310.16270v1-abstract-short" style="display: inline;"> Transformer-based Large Language Models (LLMs) are the state-of-the-art for natural language tasks. Recent work has attempted to decode, by reverse engineering the role of linear layers, the internal mechanisms by which LLMs arrive at their final predictions for text completion tasks. Yet little is known about the specific role of attention heads in producing the final token prediction. We propose… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.16270v1-abstract-full').style.display = 'inline'; document.getElementById('2310.16270v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2310.16270v1-abstract-full" style="display: none;"> Transformer-based Large Language Models (LLMs) are the state-of-the-art for natural language tasks. Recent work has attempted to decode, by reverse engineering the role of linear layers, the internal mechanisms by which LLMs arrive at their final predictions for text completion tasks. Yet little is known about the specific role of attention heads in producing the final token prediction. We propose Attention Lens, a tool that enables researchers to translate the outputs of attention heads into vocabulary tokens via learned attention-head-specific transformations called lenses. Preliminary findings from our trained lenses indicate that attention heads play highly specialized roles in language models. The code for Attention Lens is available at github.com/msakarvadia/AttentionLens. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.16270v1-abstract-full').style.display = 'none'; document.getElementById('2310.16270v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 October, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2310.16005">arXiv:2310.16005</a> <span> [<a href="https://arxiv.org/pdf/2310.16005">pdf</a>, <a href="https://arxiv.org/format/2310.16005">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> MLFMF: Data Sets for Machine Learning for Mathematical Formalization </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Petkovi%C4%87%2C+M">Matej Petkovi膰</a>, <a href="/search/cs?searchtype=author&query=Todorovski%2C+L">Ljup膷o Todorovski</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2310.16005v1-abstract-short" style="display: inline;"> We introduce MLFMF, a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. Each data set is derived from a library of formalized mathema… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.16005v1-abstract-full').style.display = 'inline'; document.getElementById('2310.16005v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2310.16005v1-abstract-full" style="display: none;"> We introduce MLFMF, a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean~4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-unimath, and the TypeTopology library. Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry. We report baseline results using standard graph and word embeddings, tree ensembles, and instance-based learning algorithms. The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. The methodology used to extract the networks and the s-expressions readily applies to other libraries, and is applicable to other proof assistants. With more than $250\,000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.16005v1-abstract-full').style.display = 'none'; document.getElementById('2310.16005v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 October, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">NeurIPS 2023</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2310.08234">arXiv:2310.08234</a> <span> [<a href="https://arxiv.org/pdf/2310.08234">pdf</a>, <a href="https://arxiv.org/format/2310.08234">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1109/REW57809.2023.00019">10.1109/REW57809.2023.00019 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> CiRA: An Open-Source Python Package for Automated Generation of Test Case Descriptions from Natural Language Requirements </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Frattini%2C+J">Julian Frattini</a>, <a href="/search/cs?searchtype=author&query=Fischbach%2C+J">Jannik Fischbach</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2310.08234v1-abstract-short" style="display: inline;"> Deriving acceptance tests from high-level, natural language requirements that achieve full coverage is a major manual challenge at the interface between requirements engineering and testing. Conditional requirements (e.g., "If A or B then C.") imply causal relationships which - when extracted - allow to generate these acceptance tests automatically. This paper presents a tool from the CiRA (Causal… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.08234v1-abstract-full').style.display = 'inline'; document.getElementById('2310.08234v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2310.08234v1-abstract-full" style="display: none;"> Deriving acceptance tests from high-level, natural language requirements that achieve full coverage is a major manual challenge at the interface between requirements engineering and testing. Conditional requirements (e.g., "If A or B then C.") imply causal relationships which - when extracted - allow to generate these acceptance tests automatically. This paper presents a tool from the CiRA (Causality In Requirements Artifacts) initiative, which automatically processes conditional natural language requirements and generates a minimal set of test case descriptions achieving full coverage. We evaluate the tool on a publicly available data set of 61 requirements from the requirements specification of the German Corona-Warn-App. The tool infers the correct test variables in 84.5% and correct variable configurations in 92.3% of all cases, which corroborates the feasibility of our approach. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.08234v1-abstract-full').style.display = 'none'; document.getElementById('2310.08234v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 12 October, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Tenth International Workshop on Artificial Intelligence and Requirements Engineering</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2309.15871">arXiv:2309.15871</a> <span> [<a href="https://arxiv.org/pdf/2309.15871">pdf</a>, <a href="https://arxiv.org/format/2309.15871">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Telescope: An Automated Hybrid Forecasting Approach on a Level-Playing Field </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Leznik%2C+M">Mark Leznik</a>, <a href="/search/cs?searchtype=author&query=Stenger%2C+M">Michael Stenger</a>, <a href="/search/cs?searchtype=author&query=Leppich%2C+R">Robert Leppich</a>, <a href="/search/cs?searchtype=author&query=Herbst%2C+N">Nikolas Herbst</a>, <a href="/search/cs?searchtype=author&query=Kounev%2C+S">Samuel Kounev</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2309.15871v1-abstract-short" style="display: inline;"> In many areas of decision-making, forecasting is an essential pillar. Consequently, many different forecasting methods have been proposed. From our experience, recently presented forecasting methods are computationally intensive, poorly automated, tailored to a particular data set, or they lack a predictable time-to-result. To this end, we introduce Telescope, a novel machine learning-based foreca… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2309.15871v1-abstract-full').style.display = 'inline'; document.getElementById('2309.15871v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2309.15871v1-abstract-full" style="display: none;"> In many areas of decision-making, forecasting is an essential pillar. Consequently, many different forecasting methods have been proposed. From our experience, recently presented forecasting methods are computationally intensive, poorly automated, tailored to a particular data set, or they lack a predictable time-to-result. To this end, we introduce Telescope, a novel machine learning-based forecasting approach that automatically retrieves relevant information from a given time series and splits it into parts, handling each of them separately. In contrast to deep learning methods, our approach doesn't require parameterization or the need to train and fit a multitude of parameters. It operates with just one time series and provides forecasts within seconds without any additional setup. Our experiments show that Telescope outperforms recent methods by providing accurate and reliable forecasts while making no assumptions about the analyzed time series. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2309.15871v1-abstract-full').style.display = 'none'; document.getElementById('2309.15871v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 September, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2309.05605">arXiv:2309.05605</a> <span> [<a href="https://arxiv.org/pdf/2309.05605">pdf</a>, <a href="https://arxiv.org/format/2309.05605">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computation and Language">cs.CL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Memory Injections: Correcting Multi-Hop Reasoning Failures during Inference in Transformer-Based Language Models </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Sakarvadia%2C+M">Mansi Sakarvadia</a>, <a href="/search/cs?searchtype=author&query=Ajith%2C+A">Aswathy Ajith</a>, <a href="/search/cs?searchtype=author&query=Khan%2C+A">Arham Khan</a>, <a href="/search/cs?searchtype=author&query=Grzenda%2C+D">Daniel Grzenda</a>, <a href="/search/cs?searchtype=author&query=Hudson%2C+N">Nathaniel Hudson</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Chard%2C+K">Kyle Chard</a>, <a href="/search/cs?searchtype=author&query=Foster%2C+I">Ian Foster</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2309.05605v3-abstract-short" style="display: inline;"> Answering multi-hop reasoning questions requires retrieving and synthesizing information from diverse sources. Large Language Models (LLMs) struggle to perform such reasoning consistently. Here we propose an approach to pinpoint and rectify multi-hop reasoning failures through targeted memory injections on LLM attention heads. First, we analyze the per-layer activations of GPT-2 models in response… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2309.05605v3-abstract-full').style.display = 'inline'; document.getElementById('2309.05605v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2309.05605v3-abstract-full" style="display: none;"> Answering multi-hop reasoning questions requires retrieving and synthesizing information from diverse sources. Large Language Models (LLMs) struggle to perform such reasoning consistently. Here we propose an approach to pinpoint and rectify multi-hop reasoning failures through targeted memory injections on LLM attention heads. First, we analyze the per-layer activations of GPT-2 models in response to single and multi-hop prompts. We then propose a mechanism that allows users to inject pertinent prompt-specific information, which we refer to as "memories," at critical LLM locations during inference. By thus enabling the LLM to incorporate additional relevant information during inference, we enhance the quality of multi-hop prompt completions. We show empirically that a simple, efficient, and targeted memory injection into a key attention layer can often increase the probability of the desired next token in multi-hop tasks, by up to 424%. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2309.05605v3-abstract-full').style.display = 'none'; document.getElementById('2309.05605v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 February, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 11 September, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Oral Presentation at BlackboxNLP Workshop at EMNLP 2023</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2206.11723">arXiv:2206.11723</a> <span> [<a href="https://arxiv.org/pdf/2206.11723">pdf</a>, <a href="https://arxiv.org/format/2206.11723">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Self-Supervised Training with Autoencoders for Visual Anomaly Detection </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Nakajima%2C+S">Shinichi Nakajima</a>, <a href="/search/cs?searchtype=author&query=M%C3%BCller%2C+K">Klaus-Robert M眉ller</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2206.11723v8-abstract-short" style="display: inline;"> We focus on a specific use case in anomaly detection where the distribution of normal samples is supported by a lower-dimensional manifold. Here, regularized autoencoders provide a popular approach by learning the identity mapping on the set of normal examples, while trying to prevent good reconstruction on points outside of the manifold. Typically, this goal is implemented by controlling the capa… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2206.11723v8-abstract-full').style.display = 'inline'; document.getElementById('2206.11723v8-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2206.11723v8-abstract-full" style="display: none;"> We focus on a specific use case in anomaly detection where the distribution of normal samples is supported by a lower-dimensional manifold. Here, regularized autoencoders provide a popular approach by learning the identity mapping on the set of normal examples, while trying to prevent good reconstruction on points outside of the manifold. Typically, this goal is implemented by controlling the capacity of the model, either directly by reducing the size of the bottleneck layer or implicitly by imposing some sparsity (or contraction) constraints on parts of the corresponding network. However, neither of these techniques does explicitly penalize the reconstruction of anomalous signals often resulting in poor detection. We tackle this problem by adapting a self-supervised learning regime that exploits discriminative information during training but focuses on the submanifold of normal examples. Informally, our training objective regularizes the model to produce locally consistent reconstructions, while replacing irregularities by acting as a filter that removes anomalous patterns. To support this intuition, we perform a rigorous formal analysis of the proposed method and provide a number of interesting insights. In particular, we show that the resulting model resembles a non-linear orthogonal projection of partially corrupted images onto the submanifold of uncorrupted samples. On the other hand, we identify the orthogonal projection as an optimal solution for a number of regularized autoencoders including the contractive and denoising variants. We support our theoretical analysis by empirical evaluation of the resulting detection and localization performance of the proposed method. In particular, we achieve a new state-of-the-art result on the MVTec AD dataset -- a challenging benchmark for visual anomaly detection in the manufacturing domain. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2206.11723v8-abstract-full').style.display = 'none'; document.getElementById('2206.11723v8-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 13 May, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 23 June, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2022. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2205.06720">arXiv:2205.06720</a> <span> [<a href="https://arxiv.org/pdf/2205.06720">pdf</a>, <a href="https://arxiv.org/format/2205.06720">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> On the Importance of Architecture and Feature Selection in Differentially Private Machine Learning </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bao%2C+W">Wenxuan Bao</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+L+A">Luke A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Bindschaedler%2C+V">Vincent Bindschaedler</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2205.06720v1-abstract-short" style="display: inline;"> We study a pitfall in the typical workflow for differentially private machine learning. The use of differentially private learning algorithms in a "drop-in" fashion -- without accounting for the impact of differential privacy (DP) noise when choosing what feature engineering operations to use, what features to select, or what neural network architecture to use -- yields overly complex and poorly p… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2205.06720v1-abstract-full').style.display = 'inline'; document.getElementById('2205.06720v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2205.06720v1-abstract-full" style="display: none;"> We study a pitfall in the typical workflow for differentially private machine learning. The use of differentially private learning algorithms in a "drop-in" fashion -- without accounting for the impact of differential privacy (DP) noise when choosing what feature engineering operations to use, what features to select, or what neural network architecture to use -- yields overly complex and poorly performing models. In other words, by anticipating the impact of DP noise, a simpler and more accurate alternative model could have been trained for the same privacy guarantee. We systematically study this phenomenon through theory and experiments. On the theory front, we provide an explanatory framework and prove that the phenomenon arises naturally from the addition of noise to satisfy differential privacy. On the experimental front, we demonstrate how the phenomenon manifests in practice using various datasets, types of models, tasks, and neural network architectures. We also analyze the factors that contribute to the problem and distill our experimental insights into concrete takeaways that practitioners can follow when training models with differential privacy. Finally, we propose privacy-aware algorithms for feature selection and neural network architecture search. We analyze their differential privacy properties and evaluate them empirically. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2205.06720v1-abstract-full').style.display = 'none'; document.getElementById('2205.06720v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 13 May, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2022. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2203.05408">arXiv:2203.05408</a> <span> [<a href="https://arxiv.org/pdf/2203.05408">pdf</a>, <a href="https://arxiv.org/format/2203.05408">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Sound">cs.SD</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Audio and Speech Processing">eess.AS</span> </div> </div> <p class="title is-5 mathjax"> Attacks as Defenses: Designing Robust Audio CAPTCHAs Using Attacks on Automatic Speech Recognition Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Abdullah%2C+H">Hadi Abdullah</a>, <a href="/search/cs?searchtype=author&query=Karlekar%2C+A">Aditya Karlekar</a>, <a href="/search/cs?searchtype=author&query=Prasad%2C+S">Saurabh Prasad</a>, <a href="/search/cs?searchtype=author&query=Rahman%2C+M+S">Muhammad Sajidur Rahman</a>, <a href="/search/cs?searchtype=author&query=Blue%2C+L">Logan Blue</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+L+A">Luke A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Bindschaedler%2C+V">Vincent Bindschaedler</a>, <a href="/search/cs?searchtype=author&query=Traynor%2C+P">Patrick Traynor</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2203.05408v1-abstract-short" style="display: inline;"> Audio CAPTCHAs are supposed to provide a strong defense for online resources; however, advances in speech-to-text mechanisms have rendered these defenses ineffective. Audio CAPTCHAs cannot simply be abandoned, as they are specifically named by the W3C as important enablers of accessibility. Accordingly, demonstrably more robust audio CAPTCHAs are important to the future of a secure and accessible… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2203.05408v1-abstract-full').style.display = 'inline'; document.getElementById('2203.05408v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2203.05408v1-abstract-full" style="display: none;"> Audio CAPTCHAs are supposed to provide a strong defense for online resources; however, advances in speech-to-text mechanisms have rendered these defenses ineffective. Audio CAPTCHAs cannot simply be abandoned, as they are specifically named by the W3C as important enablers of accessibility. Accordingly, demonstrably more robust audio CAPTCHAs are important to the future of a secure and accessible Web. We look to recent literature on attacks on speech-to-text systems for inspiration for the construction of robust, principle-driven audio defenses. We begin by comparing 20 recent attack papers, classifying and measuring their suitability to serve as the basis of new "robust to transcription" but "easy for humans to understand" CAPTCHAs. After showing that none of these attacks alone are sufficient, we propose a new mechanism that is both comparatively intelligible (evaluated through a user study) and hard to automatically transcribe (i.e., $P({\rm transcription}) = 4 \times 10^{-5}$). Finally, we demonstrate that our audio samples have a high probability of being detected as CAPTCHAs when given to speech-to-text systems ($P({\rm evasion}) = 1.77 \times 10^{-4}$). In so doing, we not only demonstrate a CAPTCHA that is approximately four orders of magnitude more difficult to crack, but that such systems can be designed based on the insights gained from attack papers using the differences between the ways that humans and computers process audio. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2203.05408v1-abstract-full').style.display = 'none'; document.getElementById('2203.05408v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 10 March, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2022. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2112.00539">arXiv:2112.00539</a> <span> [<a href="https://arxiv.org/pdf/2112.00539">pdf</a>, <a href="https://arxiv.org/format/2112.00539">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Finitary type theories with and without contexts </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Haselwarter%2C+P+G">Philipp G. Haselwarter</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2112.00539v1-abstract-short" style="display: inline;"> We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-L枚f type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presup… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2112.00539v1-abstract-full').style.display = 'inline'; document.getElementById('2112.00539v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2112.00539v1-abstract-full" style="display: none;"> We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-L枚f type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2112.00539v1-abstract-full').style.display = 'none'; document.getElementById('2112.00539v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 December, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 03B38; 03F50; 68V15; 03F07 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2110.07009">arXiv:2110.07009</a> <span> [<a href="https://arxiv.org/pdf/2110.07009">pdf</a>, <a href="https://arxiv.org/format/2110.07009">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Leveraging Generative Models for Covert Messaging: Challenges and Tradeoffs for "Dead-Drop" Deployments </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+L+A">Luke A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Howes%2C+J+K">James K. Howes IV</a>, <a href="/search/cs?searchtype=author&query=Markelon%2C+S+A">Sam A. Markelon</a>, <a href="/search/cs?searchtype=author&query=Bindschaedler%2C+V">Vincent Bindschaedler</a>, <a href="/search/cs?searchtype=author&query=Shrimpton%2C+T">Thomas Shrimpton</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2110.07009v4-abstract-short" style="display: inline;"> State of the art generative models of human-produced content are the focus of many recent papers that explore their use for steganographic communication. In particular, generative models of natural language text. Loosely, these works (invertibly) encode message-carrying bits into a sequence of samples from the model, ultimately yielding a plausible natural language covertext. By focusing on this n… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2110.07009v4-abstract-full').style.display = 'inline'; document.getElementById('2110.07009v4-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2110.07009v4-abstract-full" style="display: none;"> State of the art generative models of human-produced content are the focus of many recent papers that explore their use for steganographic communication. In particular, generative models of natural language text. Loosely, these works (invertibly) encode message-carrying bits into a sequence of samples from the model, ultimately yielding a plausible natural language covertext. By focusing on this narrow steganographic piece, prior work has largely ignored the significant algorithmic challenges, and performance-security tradeoffs, that arise when one actually tries to build a messaging pipeline around it. We make these challenges concrete, by considering the natural application of such a pipeline: namely, "dead-drop" covert messaging over large, public internet platforms (e.g. social media sites). We explicate the challenges and describe approaches to overcome them, surfacing in the process important performance and security tradeoffs that must be carefully tuned. We implement a system around this model-based format-transforming encryption pipeline, and give an empirical analysis of its performance and (heuristic) security. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2110.07009v4-abstract-full').style.display = 'none'; document.getElementById('2110.07009v4-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 15 August, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 13 October, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2107.10139">arXiv:2107.10139</a> <span> [<a href="https://arxiv.org/pdf/2107.10139">pdf</a>, <a href="https://arxiv.org/format/2107.10139">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> </div> </div> <p class="title is-5 mathjax"> Generative Models for Security: Attacks, Defenses, and Opportunities </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+L+A">Luke A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Bindschaedler%2C+V">Vincent Bindschaedler</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2107.10139v2-abstract-short" style="display: inline;"> Generative models learn the distribution of data from a sample dataset and can then generate new data instances. Recent advances in deep learning has brought forth improvements in generative model architectures, and some state-of-the-art models can (in some cases) produce outputs realistic enough to fool humans. We survey recent research at the intersection of security and privacy and generative… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2107.10139v2-abstract-full').style.display = 'inline'; document.getElementById('2107.10139v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2107.10139v2-abstract-full" style="display: none;"> Generative models learn the distribution of data from a sample dataset and can then generate new data instances. Recent advances in deep learning has brought forth improvements in generative model architectures, and some state-of-the-art models can (in some cases) produce outputs realistic enough to fool humans. We survey recent research at the intersection of security and privacy and generative models. In particular, we discuss the use of generative models in adversarial machine learning, in helping automate or enhance existing attacks, and as building blocks for defenses in contexts such as intrusion detection, biometrics spoofing, and malware obfuscation. We also describe the use of generative models in diverse applications such as fairness in machine learning, privacy-preserving data synthesis, and steganography. Finally, we discuss new threats due to generative models: the creation of synthetic media such as deepfakes that can be used for disinformation. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2107.10139v2-abstract-full').style.display = 'none'; document.getElementById('2107.10139v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 29 July, 2021; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 21 July, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2105.07811">arXiv:2105.07811</a> <span> [<a href="https://arxiv.org/pdf/2105.07811">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Applications">stat.AP</span> </div> </div> <p class="title is-5 mathjax"> Mundus vult decipi, ergo decipiatur: Visual Communication of Uncertainty in Election Polls </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Klima%2C+A">Andr茅 Klima</a>, <a href="/search/cs?searchtype=author&query=Gau%C3%9F%2C+J">Jana Gau脽</a>, <a href="/search/cs?searchtype=author&query=K%C3%BCmpel%2C+H">Hannah K眉mpel</a>, <a href="/search/cs?searchtype=author&query=Bender%2C+A">Andreas Bender</a>, <a href="/search/cs?searchtype=author&query=K%C3%BCchenhoff%2C+H">Helmut K眉chenhoff</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2105.07811v1-abstract-short" style="display: inline;"> Election poll reporting often focuses on mean values and only subordinately discusses the underlying uncertainty. Subsequent interpretations are too often phrased as certain. Moreover, media coverage rarely adequately takes into account the differences between now- and forecasts. These challenges were ubiquitous in the context of the 2016 and 2020 U.S. presidential elections, but are also present… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2105.07811v1-abstract-full').style.display = 'inline'; document.getElementById('2105.07811v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2105.07811v1-abstract-full" style="display: none;"> Election poll reporting often focuses on mean values and only subordinately discusses the underlying uncertainty. Subsequent interpretations are too often phrased as certain. Moreover, media coverage rarely adequately takes into account the differences between now- and forecasts. These challenges were ubiquitous in the context of the 2016 and 2020 U.S. presidential elections, but are also present in multi-party systems like Germany. We discuss potential sources of bias in nowcasting and forecasting and review the current standards in the visual presentation of survey-based nowcasts. Concepts are presented to attenuate the issue of falsely perceived accuracy. We discuss multiple visual presentation techniques for central aspects in poll reporting. One key idea is the use of Probabilities of Events instead of party shares. The presented ideas offer modern and improved ways to communicate (changes in) the electoral mood for the general media. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2105.07811v1-abstract-full').style.display = 'none'; document.getElementById('2105.07811v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 April, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2103.07397">arXiv:2103.07397</a> <span> [<a href="https://arxiv.org/pdf/2103.07397">pdf</a>, <a href="https://arxiv.org/format/2103.07397">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.46298/lmcs-18(1:17)2022">10.46298/lmcs-18(1:17)2022 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> An extensible equality checking algorithm for dependent type theories </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Komel%2C+A+P">Anja Petkovi膰 Komel</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2103.07397v4-abstract-short" style="display: inline;"> We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for rec… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.07397v4-abstract-full').style.display = 'inline'; document.getElementById('2103.07397v4-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2103.07397v4-abstract-full" style="display: none;"> We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.07397v4-abstract-full').style.display = 'none'; document.getElementById('2103.07397v4-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 January, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 12 March, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 03B38 (Primary); 68Q42 (Secondary) <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> F.4.1 </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Logical Methods in Computer Science, Volume 18, Issue 1 (January 19, 2022) lmcs:7268 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2101.11775">arXiv:2101.11775</a> <span> [<a href="https://arxiv.org/pdf/2101.11775">pdf</a>, <a href="https://arxiv.org/ps/2101.11775">ps</a>, <a href="https://arxiv.org/format/2101.11775">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> </div> </div> <p class="title is-5 mathjax"> Moral and Social Ramifications of Autonomous Vehicles </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Dubljevi%C4%87%2C+V">Veljko Dubljevi膰</a>, <a href="/search/cs?searchtype=author&query=Douglas%2C+S">Sean Douglas</a>, <a href="/search/cs?searchtype=author&query=Milojevich%2C+J">Jovan Milojevich</a>, <a href="/search/cs?searchtype=author&query=Ajmeri%2C+N">Nirav Ajmeri</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+W+A">William A. Bauer</a>, <a href="/search/cs?searchtype=author&query=List%2C+G+F">George F. List</a>, <a href="/search/cs?searchtype=author&query=Singh%2C+M+P">Munindar P. Singh</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2101.11775v2-abstract-short" style="display: inline;"> Autonomous Vehicles (AVs) raise important social and ethical concerns, especially about accountability, dignity, and justice. We focus on the specific concerns arising from how AV technology will affect the lives and livelihoods of professional and semi-professional drivers. Whereas previous studies of such concerns have focused on the opinions of experts, we seek to understand these ethical and s… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2101.11775v2-abstract-full').style.display = 'inline'; document.getElementById('2101.11775v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2101.11775v2-abstract-full" style="display: none;"> Autonomous Vehicles (AVs) raise important social and ethical concerns, especially about accountability, dignity, and justice. We focus on the specific concerns arising from how AV technology will affect the lives and livelihoods of professional and semi-professional drivers. Whereas previous studies of such concerns have focused on the opinions of experts, we seek to understand these ethical and societal challenges from the perspectives of the drivers themselves. To this end, we adopted a qualitative research methodology based on semi-structured interviews. This is an established social science methodology that helps understand the core concerns of stakeholders in depth by avoiding the biases of superficial methods such as surveys. We find that whereas drivers agree with the experts that AVs will significantly impact transportation systems, they are apprehensive about the prospects for their livelihoods and dismiss the suggestions that driving jobs are unsatisfying and their profession does not merit protection. By showing how drivers differ from the experts, our study has ramifications beyond AVs to AI and other advanced technologies. Our findings suggest that qualitative research applied to the relevant, especially disempowered, stakeholders is essential to ensuring that new technologies are introduced ethically. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2101.11775v2-abstract-full').style.display = 'none'; document.getElementById('2101.11775v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 29 January, 2021; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 27 January, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2009.05539">arXiv:2009.05539</a> <span> [<a href="https://arxiv.org/pdf/2009.05539">pdf</a>, <a href="https://arxiv.org/format/2009.05539">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> A general definition of dependent type theories </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Haselwarter%2C+P+G">Philipp G. Haselwarter</a>, <a href="/search/cs?searchtype=author&query=Lumsdaine%2C+P+L">Peter LeFanu Lumsdaine</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2009.05539v1-abstract-short" style="display: inline;"> We define a general class of dependent type theories, encompassing Martin-L枚f's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive rea… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2009.05539v1-abstract-full').style.display = 'inline'; document.getElementById('2009.05539v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2009.05539v1-abstract-full" style="display: none;"> We define a general class of dependent type theories, encompassing Martin-L枚f's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2009.05539v1-abstract-full').style.display = 'none'; document.getElementById('2009.05539v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 September, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2020. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 03B38 (Primary) 03F50 (Secondary) </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1912.12090">arXiv:1912.12090</a> <span> [<a href="https://arxiv.org/pdf/1912.12090">pdf</a>, <a href="https://arxiv.org/format/1912.12090">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Discrete Mathematics">cs.DM</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Polynomial-Time Exact MAP Inference on Discrete Models with Global Dependencies </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Nakajima%2C+S">Shinichi Nakajima</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1912.12090v3-abstract-short" style="display: inline;"> Considering the worst-case scenario, junction tree algorithm remains the most general solution for exact MAP inference with polynomial run-time guarantees. Unfortunately, its main tractability assumption requires the treewidth of a corresponding MRF to be bounded strongly limiting the range of admissible applications. In fact, many practical problems in the area of structured prediction require mo… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1912.12090v3-abstract-full').style.display = 'inline'; document.getElementById('1912.12090v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1912.12090v3-abstract-full" style="display: none;"> Considering the worst-case scenario, junction tree algorithm remains the most general solution for exact MAP inference with polynomial run-time guarantees. Unfortunately, its main tractability assumption requires the treewidth of a corresponding MRF to be bounded strongly limiting the range of admissible applications. In fact, many practical problems in the area of structured prediction require modelling of global dependencies by either directly introducing global factors or enforcing global constraints on the prediction variables. That, however, always results in a fully-connected graph making exact inference by means of this algorithm intractable. Previous work [1]-[4] focusing on the problem of loss-augmented inference has demonstrated how efficient inference can be performed on models with specific global factors representing non-decomposable loss functions within the training regime of SSVMs. In this paper, we extend the framework for an efficient exact inference proposed in in [3] by allowing much finer interactions between the energy of the core model and the sufficient statistics of the global terms with no additional computation costs. We demonstrate the usefulness of our method in several use cases, including one that cannot be handled by any of the previous approaches. Finally, we propose a new graph transformation technique via node cloning which ensures a polynomial run-time for solving our target problem independently of the form of a corresponding clique tree. This is important for the efficiency of the main algorithm and greatly improves upon the theoretical guarantees of the previous works. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1912.12090v3-abstract-full').style.display = 'none'; document.getElementById('1912.12090v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 February, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 27 December, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2019. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1910.11629">arXiv:1910.11629</a> <span> [<a href="https://arxiv.org/pdf/1910.11629">pdf</a>, <a href="https://arxiv.org/format/1910.11629">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1007/978-3-030-44914-8_2">10.1007/978-3-030-44914-8_2 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Runners in action </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ahman%2C+D">Danel Ahman</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1910.11629v2-abstract-short" style="display: inline;"> Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate "virtual machines". We capture the core ideas of programming with runners in an equational calculus $位_{\mathsf{coop}}$,… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.11629v2-abstract-full').style.display = 'inline'; document.getElementById('1910.11629v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1910.11629v2-abstract-full" style="display: none;"> Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate "virtual machines". We capture the core ideas of programming with runners in an equational calculus $位_{\mathsf{coop}}$, which we equip with a sound and coherent denotational semantics that guarantees the linear use of resources and execution of finalisation code. We accompany $位_{\mathsf{coop}}$ with examples of runners in action, provide a prototype language implementation in OCaml, as well as a Haskell library based on $位_{\mathsf{coop}}$. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.11629v2-abstract-full').style.display = 'none'; document.getElementById('1910.11629v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 April, 2020; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 25 October, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">ESOP 2020 final version + online appendix</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1910.09840">arXiv:1910.09840</a> <span> [<a href="https://arxiv.org/pdf/1910.09840">pdf</a>, <a href="https://arxiv.org/ps/1910.09840">ps</a>, <a href="https://arxiv.org/format/1910.09840">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">stat.ML</span> </div> </div> <p class="title is-5 mathjax"> Towards Best Practice in Explaining Neural Network Decisions with LRP </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Kohlbrenner%2C+M">Maximilian Kohlbrenner</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Nakajima%2C+S">Shinichi Nakajima</a>, <a href="/search/cs?searchtype=author&query=Binder%2C+A">Alexander Binder</a>, <a href="/search/cs?searchtype=author&query=Samek%2C+W">Wojciech Samek</a>, <a href="/search/cs?searchtype=author&query=Lapuschkin%2C+S">Sebastian Lapuschkin</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1910.09840v3-abstract-short" style="display: inline;"> Within the last decade, neural network based predictors have demonstrated impressive - and at times super-human - capabilities. This performance is often paid for with an intransparent prediction process and thus has sparked numerous contributions in the novel field of explainable artificial intelligence (XAI). In this paper, we focus on a popular and widely used method of XAI, the Layer-wise Rele… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.09840v3-abstract-full').style.display = 'inline'; document.getElementById('1910.09840v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1910.09840v3-abstract-full" style="display: none;"> Within the last decade, neural network based predictors have demonstrated impressive - and at times super-human - capabilities. This performance is often paid for with an intransparent prediction process and thus has sparked numerous contributions in the novel field of explainable artificial intelligence (XAI). In this paper, we focus on a popular and widely used method of XAI, the Layer-wise Relevance Propagation (LRP). Since its initial proposition LRP has evolved as a method, and a best practice for applying the method has tacitly emerged, based however on humanly observed evidence alone. In this paper we investigate - and for the first time quantify - the effect of this current best practice on feedforward neural networks in a visual object detection setting. The results verify that the layer-dependent approach to LRP applied in recent literature better represents the model's reasoning, and at the same time increases the object localization and class discriminativity of LRP. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.09840v3-abstract-full').style.display = 'none'; document.getElementById('1910.09840v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 13 July, 2020; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 22 October, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">7 pages, 4 figures, 1 table. fixed table row compared to v2. Presented virtually at IJCNN 2020</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1905.10270">arXiv:1905.10270</a> <span> [<a href="https://arxiv.org/pdf/1905.10270">pdf</a>, <a href="https://arxiv.org/format/1905.10270">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> Performance-Feedback Autoscaling with Budget Constraints for Cloud-based Workloads of Workflows </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ilyushkin%2C+A">Alexey Ilyushkin</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andr茅 Bauer</a>, <a href="/search/cs?searchtype=author&query=Papadopoulos%2C+A+V">Alessandro V. Papadopoulos</a>, <a href="/search/cs?searchtype=author&query=Deelman%2C+E">Ewa Deelman</a>, <a href="/search/cs?searchtype=author&query=Iosup%2C+A">Alexandru Iosup</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1905.10270v2-abstract-short" style="display: inline;"> The growing popularity of workflows in the cloud domain promoted the development of sophisticated autoscaling policies that allow automatic allocation and deallocation of resources. However, many state-of-the-art autoscaling policies for workflows are mostly plan-based or designed for batches (ensembles) of workflows. This reduces their flexibility when dealing with workloads of workflows, as the… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1905.10270v2-abstract-full').style.display = 'inline'; document.getElementById('1905.10270v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1905.10270v2-abstract-full" style="display: none;"> The growing popularity of workflows in the cloud domain promoted the development of sophisticated autoscaling policies that allow automatic allocation and deallocation of resources. However, many state-of-the-art autoscaling policies for workflows are mostly plan-based or designed for batches (ensembles) of workflows. This reduces their flexibility when dealing with workloads of workflows, as the workloads are often subject to unpredictable resource demand fluctuations. Moreover, autoscaling in clouds almost always imposes budget constraints that should be satisfied. The budget-aware autoscalers for workflows usually require task runtime estimates to be provided beforehand, which is not always possible when dealing with workloads due to their dynamic nature. To address these issues, we propose a novel Performance-Feedback Autoscaler (PFA) that is budget-aware and does not require task runtime estimates for its operation. Instead, it uses the performance-feedback loop that monitors the average throughput on each resource type. We implement PFA in the popular Apache Airflow workflow management system, and compare the performance of our autoscaler with other two state-of-the-art autoscalers, and with the optimal solution obtained with the Mixed Integer Programming approach. Our results show that PFA outperforms other considered online autoscalers, as it effectively minimizes the average job slowdown by up to 47% while still satisfying the budget constraints. Moreover, PFA shows by up to 76% lower average runtime than the competitors. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1905.10270v2-abstract-full').style.display = 'none'; document.getElementById('1905.10270v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 23 July, 2019; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 24 May, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Technical Report</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1807.05923">arXiv:1807.05923</a> <span> [<a href="https://arxiv.org/pdf/1807.05923">pdf</a>, <a href="https://arxiv.org/ps/1807.05923">ps</a>, <a href="https://arxiv.org/format/1807.05923">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> What is algebraic about algebraic effects and handlers? </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1807.05923v2-abstract-short" style="display: inline;"> This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1807.05923v2-abstract-full').style.display = 'inline'; document.getElementById('1807.05923v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1807.05923v2-abstract-full" style="display: none;"> This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra. We draw an uninterrupted line of thought between algebra and computational effects. We begin on the mathematical side of things, by reviewing the classic notions of universal algebra: signatures, algebraic theories, and their models. We then generalize and adapt the theory so that it applies to computational effects. In the last step we replace traditional mathematical notation with one that is closer to programming languages. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1807.05923v2-abstract-full').style.display = 'none'; document.getElementById('1807.05923v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 12 March, 2019; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 16 July, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 08A70 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1804.00427">arXiv:1804.00427</a> <span> [<a href="https://arxiv.org/pdf/1804.00427">pdf</a>, <a href="https://arxiv.org/format/1804.00427">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.23638/LMCS-15(2:14)2019">10.23638/LMCS-15(2:14)2019 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Every metric space is separable in function realizability </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Swan%2C+A">Andrew Swan</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1804.00427v6-abstract-short" style="display: inline;"> We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equ… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1804.00427v6-abstract-full').style.display = 'inline'; document.getElementById('1804.00427v6-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1804.00427v6-abstract-full" style="display: none;"> We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1804.00427v6-abstract-full').style.display = 'none'; document.getElementById('1804.00427v6-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 May, 2019; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 2 April, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 54E35; 03F60; 03F55 </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Logical Methods in Computer Science, Volume 15, Issue 2 (May 23, 2019) lmcs:4651 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1802.06217">arXiv:1802.06217</a> <span> [<a href="https://arxiv.org/pdf/1802.06217">pdf</a>, <a href="https://arxiv.org/ps/1802.06217">ps</a>, <a href="https://arxiv.org/format/1802.06217">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Design and Implementation of the Andromeda Proof Assistant </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Gilbert%2C+G">Ga毛tan Gilbert</a>, <a href="/search/cs?searchtype=author&query=Haselwarter%2C+P+G">Philipp G. Haselwarter</a>, <a href="/search/cs?searchtype=author&query=Pretnar%2C+M">Matija Pretnar</a>, <a href="/search/cs?searchtype=author&query=Stone%2C+C+A">Christopher A. Stone</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1802.06217v1-abstract-short" style="display: inline;"> Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1802.06217v1-abstract-full').style.display = 'inline'; document.getElementById('1802.06217v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1802.06217v1-abstract-full" style="display: none;"> Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. %even if the AML code (or interpreter) is untrusted. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped $位$-calculus, and by implementing a simple automated system for managing a universe of types. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1802.06217v1-abstract-full').style.display = 'none'; document.getElementById('1802.06217v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 17 February, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 03B15 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1709.01562">arXiv:1709.01562</a> <span> [<a href="https://arxiv.org/pdf/1709.01562">pdf</a>, <a href="https://arxiv.org/format/1709.01562">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computation and Language">cs.CL</span> </div> </div> <p class="title is-5 mathjax"> Optimizing for Measure of Performance in Max-Margin Parsing </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Nakajima%2C+S">Shinichi Nakajima</a>, <a href="/search/cs?searchtype=author&query=G%C3%B6rnitz%2C+N">Nico G枚rnitz</a>, <a href="/search/cs?searchtype=author&query=M%C3%BCller%2C+K">Klaus-Robert M眉ller</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1709.01562v2-abstract-short" style="display: inline;"> Many statistical learning problems in the area of natural language processing including sequence tagging, sequence segmentation and syntactic parsing has been successfully approached by means of structured prediction methods. An appealing property of the corresponding discriminative learning algorithms is their ability to integrate the loss function of interest directly into the optimization proce… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1709.01562v2-abstract-full').style.display = 'inline'; document.getElementById('1709.01562v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1709.01562v2-abstract-full" style="display: none;"> Many statistical learning problems in the area of natural language processing including sequence tagging, sequence segmentation and syntactic parsing has been successfully approached by means of structured prediction methods. An appealing property of the corresponding discriminative learning algorithms is their ability to integrate the loss function of interest directly into the optimization process, which potentially can increase the resulting performance accuracy. Here, we demonstrate on the example of constituency parsing how to optimize for F1-score in the max-margin framework of structural SVM. In particular, the optimization is with respect to the original (not binarized) trees. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1709.01562v2-abstract-full').style.display = 'none'; document.getElementById('1709.01562v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 8 September, 2017; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 5 September, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2017. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1708.03314">arXiv:1708.03314</a> <span> [<a href="https://arxiv.org/pdf/1708.03314">pdf</a>, <a href="https://arxiv.org/format/1708.03314">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Data Structures and Algorithms">cs.DS</span> </div> </div> <p class="title is-5 mathjax"> Partial Optimality of Dual Decomposition for MAP Inference in Pairwise MRFs </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Alexander Bauer</a>, <a href="/search/cs?searchtype=author&query=Nakajima%2C+S">Shinichi Nakajima</a>, <a href="/search/cs?searchtype=author&query=G%C3%B6rnitz%2C+N">Nico G枚rnitz</a>, <a href="/search/cs?searchtype=author&query=M%C3%BCller%2C+K">Klaus-Robert M眉ller</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1708.03314v1-abstract-short" style="display: inline;"> Markov random fields (MRFs) are a powerful tool for modelling statistical dependencies for a set of random variables using a graphical representation. An important computational problem related to MRFs, called maximum a posteriori (MAP) inference, is finding a joint variable assignment with the maximal probability. It is well known that the two popular optimisation techniques for this task, linear… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1708.03314v1-abstract-full').style.display = 'inline'; document.getElementById('1708.03314v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1708.03314v1-abstract-full" style="display: none;"> Markov random fields (MRFs) are a powerful tool for modelling statistical dependencies for a set of random variables using a graphical representation. An important computational problem related to MRFs, called maximum a posteriori (MAP) inference, is finding a joint variable assignment with the maximal probability. It is well known that the two popular optimisation techniques for this task, linear programming (LP) relaxation and dual decomposition (DD), have a strong connection both providing an optimal solution to the MAP problem when a corresponding LP relaxation is tight. However, less is known about their relationship in the opposite and more realistic case. In this paper, we explain how the fully integral assignments obtained via DD partially agree with the optimal fractional assignments via LP relaxation when the latter is not tight. In particular, for binary pairwise MRFs the corresponding result suggests that both methods share the partial optimality property of their solutions. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1708.03314v1-abstract-full').style.display = 'none'; document.getElementById('1708.03314v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 August, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> August 2017. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1610.04591">arXiv:1610.04591</a> <span> [<a href="https://arxiv.org/pdf/1610.04591">pdf</a>, <a href="https://arxiv.org/format/1610.04591">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic">math.LO</span> </div> </div> <p class="title is-5 mathjax"> The HoTT Library: A formalization of homotopy type theory in Coq </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Gross%2C+J">Jason Gross</a>, <a href="/search/cs?searchtype=author&query=Lumsdaine%2C+P+L">Peter LeFanu Lumsdaine</a>, <a href="/search/cs?searchtype=author&query=Shulman%2C+M">Mike Shulman</a>, <a href="/search/cs?searchtype=author&query=Sozeau%2C+M">Matthieu Sozeau</a>, <a href="/search/cs?searchtype=author&query=Spitters%2C+B">Bas Spitters</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1610.04591v2-abstract-short" style="display: inline;"> We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1610.04591v2-abstract-full').style.display = 'inline'; document.getElementById('1610.04591v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1610.04591v2-abstract-full" style="display: none;"> We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1610.04591v2-abstract-full').style.display = 'none'; document.getElementById('1610.04591v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 December, 2016; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 14 October, 2016; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2016. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 03B70; 03B15; 55U35 <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> F.4.1 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1602.02022">arXiv:1602.02022</a> <span> [<a href="https://arxiv.org/pdf/1602.02022">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computational Geometry">cs.CG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Graphics">cs.GR</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1117/12.877660">10.1117/12.877660 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Preoperative Volume Determination for Pituitary Adenoma </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Zukic%2C+D">Dzenan Zukic</a>, <a href="/search/cs?searchtype=author&query=Egger%2C+J">Jan Egger</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Kuhnt%2C+D">Daniela Kuhnt</a>, <a href="/search/cs?searchtype=author&query=Carl%2C+B">Barbara Carl</a>, <a href="/search/cs?searchtype=author&query=Freisleben%2C+B">Bernd Freisleben</a>, <a href="/search/cs?searchtype=author&query=Kolb%2C+A">Andreas Kolb</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1602.02022v1-abstract-short" style="display: inline;"> The most common sellar lesion is the pituitary adenoma, and sellar tumors are approximately 10-15% of all intracranial neoplasms. Manual slice-by-slice segmentation takes quite some time that can be reduced by using the appropriate algorithms. In this contribution, we present a segmentation method for pituitary adenoma. The method is based on an algorithm that we have applied recently to segmentin… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1602.02022v1-abstract-full').style.display = 'inline'; document.getElementById('1602.02022v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1602.02022v1-abstract-full" style="display: none;"> The most common sellar lesion is the pituitary adenoma, and sellar tumors are approximately 10-15% of all intracranial neoplasms. Manual slice-by-slice segmentation takes quite some time that can be reduced by using the appropriate algorithms. In this contribution, we present a segmentation method for pituitary adenoma. The method is based on an algorithm that we have applied recently to segmenting glioblastoma multiforme. A modification of this scheme is used for adenoma segmentation that is much harder to perform, due to lack of contrast-enhanced boundaries. In our experimental evaluation, neurosurgeons performed manual slice-by-slice segmentation of ten magnetic resonance imaging (MRI) cases. The segmentations were compared to the segmentation results of the proposed method using the Dice Similarity Coefficient (DSC). The average DSC for all datasets was 75.92% +/- 7.24%. A manual segmentation took about four minutes and our algorithm required about one second. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1602.02022v1-abstract-full').style.display = 'none'; document.getElementById('1602.02022v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 5 February, 2016; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2016. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">7 pages, 6 figures, 1 table, 16 references in Proc. SPIE 7963, Medical Imaging 2011: Computer-Aided Diagnosis, 79632T (9 March 2011). arXiv admin note: text overlap with arXiv:1103.1778</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1505.06237">arXiv:1505.06237</a> <span> [<a href="https://arxiv.org/pdf/1505.06237">pdf</a>, <a href="https://arxiv.org/format/1505.06237">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> Tunnel Surface 3D Reconstruction from Unoriented Image Sequences </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Arnold Bauer</a>, <a href="/search/cs?searchtype=author&query=Gutjahr%2C+K">Karlheinz Gutjahr</a>, <a href="/search/cs?searchtype=author&query=Paar%2C+G">Gerhard Paar</a>, <a href="/search/cs?searchtype=author&query=Kontrus%2C+H">Heiner Kontrus</a>, <a href="/search/cs?searchtype=author&query=Glatzl%2C+R">Robert Glatzl</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1505.06237v1-abstract-short" style="display: inline;"> The 3D documentation of the tunnel surface during construction requires fast and robust measurement systems. In the solution proposed in this paper, during tunnel advance a single camera is taking pictures of the tunnel surface from several positions. The recorded images are automatically processed to gain a 3D tunnel surface model. Image acquisition is realized by the tunneling/advance/driving pe… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1505.06237v1-abstract-full').style.display = 'inline'; document.getElementById('1505.06237v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1505.06237v1-abstract-full" style="display: none;"> The 3D documentation of the tunnel surface during construction requires fast and robust measurement systems. In the solution proposed in this paper, during tunnel advance a single camera is taking pictures of the tunnel surface from several positions. The recorded images are automatically processed to gain a 3D tunnel surface model. Image acquisition is realized by the tunneling/advance/driving personnel close to the tunnel face (= the front end of the advance). Based on the following fully automatic analysis/evaluation, a decision on the quality of the outbreak can be made within a few minutes. This paper describes the image recording system and conditions as well as the stereo-photogrammetry based workflow for the continuously merged dense 3D reconstruction of the entire advance region. Geo-reference is realized by means of signalized targets that are automatically detected in the images. We report on the results of recent testing under real construction conditions, and conclude with prospects for further development in terms of on-site performance. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1505.06237v1-abstract-full').style.display = 'none'; document.getElementById('1505.06237v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 May, 2015; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2015. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Presented at OAGM Workshop, 2015 (arXiv:1505.01065)</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Report number:</span> OAGM/2015/10 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1406.2041">arXiv:1406.2041</a> <span> [<a href="https://arxiv.org/pdf/1406.2041">pdf</a>, <a href="https://arxiv.org/format/1406.2041">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> </div> </div> <p class="title is-5 mathjax"> Platform-Centric Android Monitoring---Modular and Efficient </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Kuester%2C+J">Jan-Christoph Kuester</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1406.2041v1-abstract-short" style="display: inline;"> We present an add-on for the Android platform, capable of intercepting nearly all interactions between apps or apps with the platform, including arguments of method invocations in a human-readable format. A preliminary performance evaluation shows that the performance penalty of our solution is roughly comparable with similar tools in that area. The advantage of our solution, however, is that it i… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1406.2041v1-abstract-full').style.display = 'inline'; document.getElementById('1406.2041v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1406.2041v1-abstract-full" style="display: none;"> We present an add-on for the Android platform, capable of intercepting nearly all interactions between apps or apps with the platform, including arguments of method invocations in a human-readable format. A preliminary performance evaluation shows that the performance penalty of our solution is roughly comparable with similar tools in that area. The advantage of our solution, however, is that it is truly modular in the sense that we do not actually modify the Android platform itself, and can include it even with an already running system. Possible uses of such an add-on are manifold; we discuss one from the area of runtime verification that aims at improving system security. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1406.2041v1-abstract-full').style.display = 'none'; document.getElementById('1406.2041v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 8 June, 2014; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2014. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1310.6092">arXiv:1310.6092</a> <span> [<a href="https://arxiv.org/pdf/1310.6092">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> A Ray-based Approach for Boundary Estimation of Fiber Bundles Derived from Diffusion Tensor Imaging </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Barbieri%2C+S">Sebastiano Barbieri</a>, <a href="/search/cs?searchtype=author&query=Klein%2C+J">Jan Klein</a>, <a href="/search/cs?searchtype=author&query=Egger%2C+J">Jan Egger</a>, <a href="/search/cs?searchtype=author&query=Kuhnt%2C+D">Daniela Kuhnt</a>, <a href="/search/cs?searchtype=author&query=Freisleben%2C+B">Bernd Freisleben</a>, <a href="/search/cs?searchtype=author&query=Hahn%2C+H+K">Horst K. Hahn</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1310.6092v1-abstract-short" style="display: inline;"> Diffusion Tensor Imaging (DTI) is a non-invasive imaging technique that allows estimation of the location of white matter tracts in-vivo, based on the measurement of water diffusion properties. For each voxel, a second-order tensor can be calculated by using diffusion-weighted sequences (DWI) that are sensitive to the random motion of water molecules. Given at least 6 diffusion-weighted images wit… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.6092v1-abstract-full').style.display = 'inline'; document.getElementById('1310.6092v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1310.6092v1-abstract-full" style="display: none;"> Diffusion Tensor Imaging (DTI) is a non-invasive imaging technique that allows estimation of the location of white matter tracts in-vivo, based on the measurement of water diffusion properties. For each voxel, a second-order tensor can be calculated by using diffusion-weighted sequences (DWI) that are sensitive to the random motion of water molecules. Given at least 6 diffusion-weighted images with different gradients and one unweighted image, the coefficients of the symmetric diffusion tensor matrix can be calculated. Deriving the eigensystem of the tensor, the eigenvectors and eigenvalues can be calculated to describe the three main directions of diffusion and its magnitude. Using DTI data, fiber bundles can be determined, to gain information about eloquent brain structures. Especially in neurosurgery, information about location and dimension of eloquent structures like the corticospinal tract or the visual pathways is of major interest. Therefore, the fiber bundle boundary has to be determined. In this paper, a novel ray-based approach for boundary estimation of tubular structures is presented. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.6092v1-abstract-full').style.display = 'none'; document.getElementById('1310.6092v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 October, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2013. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">5 pages, 2 figures, 7 references</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Int J CARS, Vol. 5, Suppl. 1, pp. 47-48, Springer Press, June 2010 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1310.5755">arXiv:1310.5755</a> <span> [<a href="https://arxiv.org/pdf/1310.5755">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Medical Physics">physics.med-ph</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Tissues and Organs">q-bio.TO</span> </div> </div> <p class="title is-5 mathjax"> Determination, Calculation and Representation of the Upper and Lower Sealing Zones During Virtual Stenting of Aneurysms </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Egger%2C+J">Jan Egger</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Gro%C3%9Fkopf%2C+S">Stefan Gro脽kopf</a>, <a href="/search/cs?searchtype=author&query=Biermann%2C+C">Christina Biermann</a>, <a href="/search/cs?searchtype=author&query=Freisleben%2C+B">Bernd Freisleben</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1310.5755v1-abstract-short" style="display: inline;"> In this contribution, a novel method for stent simulation in preoperative computed tomography angiography (CTA) acquisitions of patients is presented where the sealing zones are automatically calculated and visualized. The method is eligible for non-bifurcated and bifurcated stents (Y-stents). Results of the proposed stent simulation with an automatic calculation of the sealing zones for specific… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.5755v1-abstract-full').style.display = 'inline'; document.getElementById('1310.5755v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1310.5755v1-abstract-full" style="display: none;"> In this contribution, a novel method for stent simulation in preoperative computed tomography angiography (CTA) acquisitions of patients is presented where the sealing zones are automatically calculated and visualized. The method is eligible for non-bifurcated and bifurcated stents (Y-stents). Results of the proposed stent simulation with an automatic calculation of the sealing zones for specific diseases (abdominal aortic aneurysms (AAA), thoracic aortic aneurysms (TAA), iliac aneurysms) are presented. The contribution is organized as follows. Section 2 presents the proposed approach. In Section 3, experimental results are discussed. Section 4 concludes the contribution and outlines areas for future work. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.5755v1-abstract-full').style.display = 'none'; document.getElementById('1310.5755v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 21 October, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2013. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">4 pages, 2 figures, 10 references</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Int J CARS, Vol. 5, Suppl. 1, pp. 13-14, Springer Press, June 2010 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1306.6316">arXiv:1306.6316</a> <span> [<a href="https://arxiv.org/pdf/1306.6316">pdf</a>, <a href="https://arxiv.org/ps/1306.6316">ps</a>, <a href="https://arxiv.org/format/1306.6316">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.2168/LMCS-10(4:9)2014">10.2168/LMCS-10(4:9)2014 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> An Effect System for Algebraic Effects and Handlers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Pretnar%2C+M">Matija Pretnar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1306.6316v3-abstract-short" style="display: inline;"> We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it ade… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.6316v3-abstract-full').style.display = 'inline'; document.getElementById('1306.6316v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1306.6316v3-abstract-full" style="display: none;"> We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.6316v3-abstract-full').style.display = 'none'; document.getElementById('1306.6316v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 December, 2014; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 26 June, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2013. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Logical Methods in Computer Science, Volume 10, Issue 4 (December 10, 2014) lmcs:1153 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1303.3645">arXiv:1303.3645</a> <span> [<a href="https://arxiv.org/pdf/1303.3645">pdf</a>, <a href="https://arxiv.org/format/1303.3645">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Formal Languages and Automata Theory">cs.FL</span> </div> </div> <p class="title is-5 mathjax"> From propositional to first-order monitoring </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=K%C3%BCster%2C+J">Jan-Christoph K眉ster</a>, <a href="/search/cs?searchtype=author&query=Vegliach%2C+G">Gil Vegliach</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1303.3645v1-abstract-short" style="display: inline;"> The main purpose of this paper is to introduce a first-order temporal logic, LTLFO, and a corresponding monitor construction based on a new type of automaton, called spawning automaton. Specifically, we show that monitoring a specification in LTLFO boils down to an undecidable decision problem. The proof of this result revolves around specific ideas on what we consider a "proper" monitor. As the… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1303.3645v1-abstract-full').style.display = 'inline'; document.getElementById('1303.3645v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1303.3645v1-abstract-full" style="display: none;"> The main purpose of this paper is to introduce a first-order temporal logic, LTLFO, and a corresponding monitor construction based on a new type of automaton, called spawning automaton. Specifically, we show that monitoring a specification in LTLFO boils down to an undecidable decision problem. The proof of this result revolves around specific ideas on what we consider a "proper" monitor. As these ideas are general, we outline them first in the setting of standard LTL, before lifting them to the setting of first-order logic and LTLFO. Although due to the above result one cannot hope to obtain a complete monitor for LTLFO, we prove the soundness of our automata-based construction and give experimental results from an implementation. These seem to substantiate our hypothesis that the automata-based construction leads to efficient runtime monitors whose size does not grow with increasing trace lengths (as is often observed in similar approaches). However, we also discuss formulae for which growth is unavoidable, irrespective of the chosen monitoring approach. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1303.3645v1-abstract-full').style.display = 'none'; document.getElementById('1303.3645v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 14 March, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2013. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1207.2461">arXiv:1207.2461</a> <span> [<a href="https://arxiv.org/pdf/1207.2461">pdf</a>, <a href="https://arxiv.org/ps/1207.2461">ps</a>, <a href="https://arxiv.org/format/1207.2461">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Reasoning with Data-Centric Business Processes </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=Baumgartner%2C+P">Peter Baumgartner</a>, <a href="/search/cs?searchtype=author&query=Norrish%2C+M">Michael Norrish</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1207.2461v1-abstract-short" style="display: inline;"> We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states. Specifically, we model business processes in terms of smaller fragments, whose possible interactions are constrained by first-order logic formulae. In turn, process… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1207.2461v1-abstract-full').style.display = 'inline'; document.getElementById('1207.2461v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1207.2461v1-abstract-full" style="display: none;"> We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states. Specifically, we model business processes in terms of smaller fragments, whose possible interactions are constrained by first-order logic formulae. In turn, process fragments are connected graphs annotated with instructions to modify data. Correctness properties concerning the evolution of data with respect to processes can be stated in a first-order branching-time logic over built-in theories, such as linear integer arithmetic, records and arrays. Solving general model checking problems over this logic is considerably harder than model checking when a concrete initial state is given. To this end, we present a tableau procedure that reduces these model checking problems to first-order logic over arithmetic. The resulting proof obligations are passed on to appropriate "off-the-shelf" theorem provers. We also detail our modelling approach, describe the reasoning components and report on first experiments. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1207.2461v1-abstract-full').style.display = 'none'; document.getElementById('1207.2461v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 July, 2012; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2012. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1204.3362">arXiv:1204.3362</a> <span> [<a href="https://arxiv.org/pdf/1204.3362">pdf</a>, <a href="https://arxiv.org/ps/1204.3362">ps</a>, <a href="https://arxiv.org/format/1204.3362">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Information Retrieval">cs.IR</span> </div> </div> <p class="title is-5 mathjax"> Event based classification of Web 2.0 text streams </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=Wolff%2C+C">Christian Wolff</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1204.3362v2-abstract-short" style="display: inline;"> Web 2.0 applications like Twitter or Facebook create a continuous stream of information. This demands new ways of analysis in order to offer insight into this stream right at the moment of the creation of the information, because lots of this data is only relevant within a short period of time. To address this problem real time search engines have recently received increased attention. They take i… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1204.3362v2-abstract-full').style.display = 'inline'; document.getElementById('1204.3362v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1204.3362v2-abstract-full" style="display: none;"> Web 2.0 applications like Twitter or Facebook create a continuous stream of information. This demands new ways of analysis in order to offer insight into this stream right at the moment of the creation of the information, because lots of this data is only relevant within a short period of time. To address this problem real time search engines have recently received increased attention. They take into account the continuous flow of information differently than traditional web search by incorporating temporal and social features, that describe the context of the information during its creation. Standard approaches where data first get stored and then is processed from a peristent storage suffer from latency. We want to address the fluent and rapid nature of text stream by providing an event based approach that analyses directly the stream of information. In a first step we want to define the difference between real time search and traditional search to clarify the demands in modern text filtering. In a second step we want to show how event based features can be used to support the tasks of real time search engines. Using the example of Twitter we present in this paper a way how to combine an event based approach with text mining and information filtering concepts in order to classify incoming information based on stream features. We calculate stream dependant features and feed them into a neural network in order to classify the text streams. We show the separative capabilities of event based features as the foundation for a real time search engine. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1204.3362v2-abstract-full').style.display = 'none'; document.getElementById('1204.3362v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 June, 2013; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 16 April, 2012; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2012. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">11 pages, 3 figures, 2 tables</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> H.3.3; I.5.4 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1203.1539">arXiv:1203.1539</a> <span> [<a href="https://arxiv.org/pdf/1203.1539">pdf</a>, <a href="https://arxiv.org/ps/1203.1539">ps</a>, <a href="https://arxiv.org/format/1203.1539">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1016/j.jlamp.2014.02.001">10.1016/j.jlamp.2014.02.001 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Programming with Algebraic Effects and Handlers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andrej Bauer</a>, <a href="/search/cs?searchtype=author&query=Pretnar%2C+M">Matija Pretnar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1203.1539v1-abstract-short" style="display: inline;"> Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semanti… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1203.1539v1-abstract-full').style.display = 'inline'; document.getElementById('1203.1539v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1203.1539v1-abstract-full" style="display: none;"> Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1203.1539v1-abstract-full').style.display = 'none'; document.getElementById('1203.1539v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 March, 2012; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2012. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.3.3; F.3.3 </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Journal of Logical and Algebraic Methods in Programming. Volume 84, Issue 1, January 2015, Pages 108-123 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1111.5133">arXiv:1111.5133</a> <span> [<a href="https://arxiv.org/pdf/1111.5133">pdf</a>, <a href="https://arxiv.org/ps/1111.5133">ps</a>, <a href="https://arxiv.org/format/1111.5133">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Decentralised LTL Monitoring </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+A">Andreas Bauer</a>, <a href="/search/cs?searchtype=author&query=Falcone%2C+Y">Yli猫s Falcone</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1111.5133v3-abstract-short" style="display: inline;"> Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behaviour as opposed to many components displaying many local behaviours that together constitute the system's global behaviour. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the s… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1111.5133v3-abstract-full').style.display = 'inline'; document.getElementById('1111.5133v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1111.5133v3-abstract-full" style="display: none;"> Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behaviour as opposed to many components displaying many local behaviours that together constitute the system's global behaviour. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system's global behaviour in terms of an LTL formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components' local behaviours are observable. In this case, the LTL specification needs to be decomposed into sub-formulae which, in turn, need to be distributed amongst the components' locally attached monitors, each of which sees only a distinct part of the global behaviour. The main contribution of this paper is an algorithm for distributing and monitoring LTL formulae, such that satisfac- tion or violation of specifications can be detected by local monitors alone. We present an implementation and show that our algorithm introduces only a minimum delay in detecting satisfaction/violation of a specification. Moreover, our practical results show that the communication overhead introduced by the local monitors is considerably lower than the number of messages that would need to be sent to a central data collection point. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1111.5133v3-abstract-full').style.display = 'none'; document.getElementById('1111.5133v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 15 March, 2012; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 22 November, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> November 2011. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1104.1556">arXiv:1104.1556</a> <span> [<a href="https://arxiv.org/pdf/1104.1556">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> Benchmarking the Quality of Diffusion-Weighted Images </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Klein%2C+J">Jan Klein</a>, <a href="/search/cs?searchtype=author&query=Barbieri%2C+S">Sebastiano Barbieri</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a>, <a href="/search/cs?searchtype=author&query=Hahn%2C+H+K">Horst K. Hahn</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1104.1556v3-abstract-short" style="display: inline;"> We present a novel method that allows for measuring the quality of diffusion-weighted MR images dependent on the image resolution and the image noise. For this purpose, we introduce a new thresholding technique so that noise and the signal can automatically be estimated from a single data set. Thus, no user interaction as well as no double acquisition technique, which requires a time-consuming pro… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1104.1556v3-abstract-full').style.display = 'inline'; document.getElementById('1104.1556v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1104.1556v3-abstract-full" style="display: none;"> We present a novel method that allows for measuring the quality of diffusion-weighted MR images dependent on the image resolution and the image noise. For this purpose, we introduce a new thresholding technique so that noise and the signal can automatically be estimated from a single data set. Thus, no user interaction as well as no double acquisition technique, which requires a time-consuming proper geometrical registration, is needed. As a coarser image resolution or slice thickness leads to a higher signal-to-noise ratio (SNR), our benchmark determines a resolution-independent quality measure so that images with different resolutions can be adequately compared. To evaluate our method, a set of diffusion-weighted images from different vendors is used. It is shown that the quality can efficiently be determined and that the automatically computed SNR is comparable to the SNR which is measured manually in a manually selected region of interest. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1104.1556v3-abstract-full').style.display = 'none'; document.getElementById('1104.1556v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 May, 2011; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 8 April, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2011. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1103.1952">arXiv:1103.1952</a> <span> [<a href="https://arxiv.org/pdf/1103.1952">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> Ray-Based and Graph-Based Methods for Fiber Bundle Boundary Estimation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Egger%2C+J">Jan Egger</a>, <a href="/search/cs?searchtype=author&query=Kuhnt%2C+D">Daniela Kuhnt</a>, <a href="/search/cs?searchtype=author&query=Barbieri%2C+S">Sebastiano Barbieri</a>, <a href="/search/cs?searchtype=author&query=Klein%2C+J">Jan Klein</a>, <a href="/search/cs?searchtype=author&query=Hahn%2C+H+K">Horst K. Hahn</a>, <a href="/search/cs?searchtype=author&query=Freisleben%2C+B">Bernd Freisleben</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1103.1952v1-abstract-short" style="display: inline;"> Diffusion Tensor Imaging (DTI) provides the possibility of estimating the location and course of eloquent structures in the human brain. Knowledge about this is of high importance for preoperative planning of neurosurgical interventions and for intraoperative guidance by neuronavigation in order to minimize postoperative neurological deficits. Therefore, the segmentation of these structures as clo… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1103.1952v1-abstract-full').style.display = 'inline'; document.getElementById('1103.1952v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1103.1952v1-abstract-full" style="display: none;"> Diffusion Tensor Imaging (DTI) provides the possibility of estimating the location and course of eloquent structures in the human brain. Knowledge about this is of high importance for preoperative planning of neurosurgical interventions and for intraoperative guidance by neuronavigation in order to minimize postoperative neurological deficits. Therefore, the segmentation of these structures as closed, three-dimensional object is necessary. In this contribution, two methods for fiber bundle segmentation between two defined regions are compared using software phantoms (abstract model and anatomical phantom modeling the right corticospinal tract). One method uses evaluation points from sampled rays as candidates for boundary points, the other method sets up a directed and weighted (depending on a scalar measure) graph and performs a min-cut for optimal segmentation results. Comparison is done by using the Dice Similarity Coefficient (DSC), a measure for spatial overlap of different segmentation results. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1103.1952v1-abstract-full').style.display = 'none'; document.getElementById('1103.1952v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 10 March, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2011. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">4 pages, 6 figures, BIOSIGNAL, Berlin, 2010</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1103.1778">arXiv:1103.1778</a> <span> [<a href="https://arxiv.org/pdf/1103.1778">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computational Engineering, Finance, and Science">cs.CE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Medical Physics">physics.med-ph</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Tissues and Organs">q-bio.TO</span> </div> </div> <p class="title is-5 mathjax"> Pituitary Adenoma Segmentation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Egger%2C+J">Jan Egger</a>, <a href="/search/cs?searchtype=author&query=Bauer%2C+M+H+A">Miriam H. A. Bauer</a>, <a href="/search/cs?searchtype=author&query=Kuhnt%2C+D">Daniela Kuhnt</a>, <a href="/search/cs?searchtype=author&query=Freisleben%2C+B">Bernd Freisleben</a>, <a href="/search/cs?searchtype=author&query=Nimsky%2C+C">Christopher Nimsky</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1103.1778v1-abstract-short" style="display: inline;"> Sellar tumors are approximately 10-15% among all intracranial neoplasms. The most common sellar lesion is the pituitary adenoma. Manual segmentation is a time-consuming process that can be shortened by using adequate algorithms. In this contribution, we present a segmentation method for pituitary adenoma. The method is based on an algorithm we developed recently in previous work where the novel se… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1103.1778v1-abstract-full').style.display = 'inline'; document.getElementById('1103.1778v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1103.1778v1-abstract-full" style="display: none;"> Sellar tumors are approximately 10-15% among all intracranial neoplasms. The most common sellar lesion is the pituitary adenoma. Manual segmentation is a time-consuming process that can be shortened by using adequate algorithms. In this contribution, we present a segmentation method for pituitary adenoma. The method is based on an algorithm we developed recently in previous work where the novel segmentation scheme was successfully used for segmentation of glioblastoma multiforme and provided an average Dice Similarity Coefficient (DSC) of 77%. This scheme is used for automatic adenoma segmentation. In our experimental evaluation, neurosurgeons with strong experiences in the treatment of pituitary adenoma performed manual slice-by-slice segmentation of 10 magnetic resonance imaging (MRI) cases. Afterwards, the segmentations were compared with the segmentation results of the proposed method via the DSC. The average DSC for all data sets was 77.49% +/- 4.52%. Compared with a manual segmentation that took, on the average, 3.91 +/- 0.54 minutes, the overall segmentation in our implementation required less than 4 seconds. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1103.1778v1-abstract-full').style.display = 'none'; document.getElementById('1103.1778v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 9 March, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2011. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">4 pages, 5 figures, BIOSIGNAL, Berlin, 2010</span> </p> </li> </ol> <nav class="pagination is-small is-centered breathe-horizontal" role="navigation" aria-label="pagination"> <a href="" class="pagination-previous is-invisible">Previous </a> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=50" class="pagination-next" >Next </a> <ul class="pagination-list"> <li> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=0" class="pagination-link is-current" aria-label="Goto page 1">1 </a> </li> <li> <a href="/search/?searchtype=author&query=Bauer%2C+A&start=50" class="pagination-link " aria-label="Page 2" aria-current="page">2 </a> </li> </ul> </nav> <div class="is-hidden-tablet">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> </main> <footer> <div class="columns is-desktop" role="navigation" aria-label="Secondary">  <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/about">About</a></li> <li><a href="https://info.arxiv.org/help">Help</a></li> </ul> </div> <div class="column"> <ul class="nav-spaced"> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>contact arXiv</title><desc>Click here to contact arXiv</desc><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg> <a href="https://info.arxiv.org/help/contact.html"> Contact</a> </li> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>subscribe to arXiv mailings</title><desc>Click here to subscribe</desc><path d="M476 3.2L12.5 270.6c-18.1 10.4-15.8 35.6 2.2 43.2L121 358.4l287.3-253.2c5.5-4.9 13.3 2.6 8.6 8.3L176 407v80.5c0 23.6 28.5 32.9 42.5 15.8L282 426l124.6 52.2c14.2 6 30.4-2.9 33-18.2l72-432C515 7.8 493.3-6.8 476 3.2z"/></svg> <a href="https://info.arxiv.org/help/subscribe"> Subscribe</a> </li> </ul> </div> </div> </div>   <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/license/index.html">Copyright</a></li> <li><a href="https://info.arxiv.org/help/policies/privacy_policy.html">Privacy Policy</a></li> </ul> </div> <div class="column sorry-app-links"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/web_accessibility.html">Web Accessibility Assistance</a></li> <li> <p class="help"> <a class="a11y-main-link" href="https://status.arxiv.org" target="_blank">arXiv Operational Status <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 256 512" class="icon filter-dark_grey" role="presentation"><path d="M224.3 273l-136 136c-9.4 9.4-24.6 9.4-33.9 0l-22.6-22.6c-9.4-9.4-9.4-24.6 0-33.9l96.4-96.4-96.4-96.4c-9.4-9.4-9.4-24.6 0-33.9L54.3 103c9.4-9.4 24.6-9.4 33.9 0l136 136c9.5 9.4 9.5 24.6.1 34z"/></svg></a><br> Get status notifications via <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/email/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg>email</a> or <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/slack/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512" class="icon filter-black" role="presentation"><path d="M94.12 315.1c0 25.9-21.16 47.06-47.06 47.06S0 341 0 315.1c0-25.9 21.16-47.06 47.06-47.06h47.06v47.06zm23.72 0c0-25.9 21.16-47.06 47.06-47.06s47.06 21.16 47.06 47.06v117.84c0 25.9-21.16 47.06-47.06 47.06s-47.06-21.16-47.06-47.06V315.1zm47.06-188.98c-25.9 0-47.06-21.16-47.06-47.06S139 32 164.9 32s47.06 21.16 47.06 47.06v47.06H164.9zm0 23.72c25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06H47.06C21.16 243.96 0 222.8 0 196.9s21.16-47.06 47.06-47.06H164.9zm188.98 47.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06h-47.06V196.9zm-23.72 0c0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06V79.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06V196.9zM283.1 385.88c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06v-47.06h47.06zm0-23.72c-25.9 0-47.06-21.16-47.06-47.06 0-25.9 21.16-47.06 47.06-47.06h117.84c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06H283.1z"/></svg>slack</a> </p> </li> </ul> </div> </div> </div>  </div> </footer> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/member_acknowledgement.js"></script> </body> </html>

CINXE.COM

Search | arXiv e-print repository