Search Results

Documents authored by Moss, Eliot

Found 2 Possible Name Variants:

Moss, J. Eliot B.

Document
DOI: 10.4230/LIPIcs.ITP.2022.32
Mechanizing Soundness of Off-Policy Evaluation

Authors: Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
There are reinforcement learning scenarios - e.g., in medicine - where we are compelled to be as confident as possible that a policy change will result in an improvement before implementing it. In such scenarios, we can employ off-policy evaluation (OPE). The basic idea of OPE is to record histories of behaviors under the current policy, and then develop an estimate of the quality of a proposed new policy, seeing what the behavior would have been under the new policy. As we are evaluating the policy without actually using it, we have the "off-policy" of OPE. Applying a concentration inequality to the estimate, we derive a confidence interval for the expected quality of the new policy. If the confidence interval lies above that of the current policy, we can change policies with high confidence that we will do no harm. We focus here on the mathematics of this method, by mechanizing the soundness of off-policy evaluation. A natural side effect of the mechanization is both to clarify all the result’s mathematical assumptions and preconditions, and to further develop HOL4’s library of verified statistical mathematics, including concentration inequalities. Of more significance, the OPE method relies on importance sampling, whose soundness we prove using a measure-theoretic approach. In fact, we generalize the standard result, showing it for contexts comprising both discrete and continuous probability distributions.
Cite as

Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas. Mechanizing Soundness of Off-Policy Evaluation. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{yeager_et_al:LIPIcs.ITP.2022.32,
  author =	{Yeager, Jared and Moss, J. Eliot B. and Norrish, Michael and Thomas, Philip S.},
  title =	{{Mechanizing Soundness of Off-Policy Evaluation}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.32},
  URN =		{urn:nbn:de:0030-drops-167413},
  doi =		{10.4230/LIPIcs.ITP.2022.32},
  annote =	{Keywords: Formal Methods, HOL4, Reinforcement Learning, Off-Policy Evaluation, Concentration Inequality, Hoeffding}
}
Document
DOI: 10.4230/DagRep.5.1.1
Concurrent Computing in the Many-core Era (Dagstuhl Seminar 15021)

Authors: Michael Philippsen, Pascal Felber, Michael L. Scott, and J. Eliot B. Moss

Published in: Dagstuhl Reports, Volume 5, Issue 1 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15021 "Concurrent computing in the many-core era". This seminar is a successor to Dagstuhl Seminars 08241 "Transactional memory: From implementation to application" and 12161 "Abstractions for scalable multicore computing", respectively held in June 2008 and in April 2012. The current seminar built on the previous seminars by notably (1) broadening the scope to concurrency beyond transactional memory and shared-memory multicores abstractions, (2) focusing on the new challenges and potential uses of emerging hardware support for synchronization extensions, and (3) considering the increasing complexity resulting from the explosion in heterogeneity.
Cite as

Michael Philippsen, Pascal Felber, Michael L. Scott, and J. Eliot B. Moss. Concurrent Computing in the Many-core Era (Dagstuhl Seminar 15021). In Dagstuhl Reports, Volume 5, Issue 1, pp. 1-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{philippsen_et_al:DagRep.5.1.1,
  author =	{Philippsen, Michael and Felber, Pascal and Scott, Michael L. and Moss, J. Eliot B.},
  title =	{{Concurrent Computing in the Many-core Era (Dagstuhl Seminar 15021)}},
  pages =	{1--56},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{1},
  editor =	{Philippsen, Michael and Felber, Pascal and Scott, Michael L. and Moss, J. Eliot B.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.1.1},
  URN =		{urn:nbn:de:0030-drops-50105},
  doi =		{10.4230/DagRep.5.1.1},
  annote =	{Keywords: Multi-/many-core processors, Concurrent Programming, Synchronization, Transactional Memory, Programming Languages, Compilation}
}

Moss, Eliot

Document
DOI: 10.4230/DagSemProc.04181.1
The Atomic Manifesto: a Story in Four Quarks

Authors: Cliff Jones, David Lomet, Alexander Romanovsky, Gerhard Weikum, Alan Fekete, Marie-Claude Gaudel, Henry F. Korth, Rogerio de Lemos, Eliot Moss, Ravi Rajwar, Krithi Ramamritham, Brian Randell, and Luis Rodrigues

Published in: Dagstuhl Seminar Proceedings, Volume 4181, Atomicity in System Design and Execution (2004)

Abstract
This report summarizes the viewpoints and insights gathered in the Dagstuhl Seminar on Atomicity in System Design and Execution, which was attended by 32 people from four different scientific communities: database and transaction processing systems, fault tolerance and dependable systems, formal methods for system design and correctness reasoning, and hardware architecture and programming languages. Each community presents its position in interpreting the notion of atomicity and the existing state of the art, and each community identifies scientific challenges that should be addressed in future work. In addition, the report discusses common themes across communities and strategic research problems that require multiple communities to team up for a viable solution. The general theme of how to specify, implement, compose, and reason about extended and relaxed notions of atomicity is viewed as a key piece in coping with the pressing issue of building and maintaining highly dependable systems that comprise many components with complex interaction patterns.
Cite as

Cliff Jones, David Lomet, Alexander Romanovsky, Gerhard Weikum, Alan Fekete, Marie-Claude Gaudel, Henry F. Korth, Rogerio de Lemos, Eliot Moss, Ravi Rajwar, Krithi Ramamritham, Brian Randell, and Luis Rodrigues. The Atomic Manifesto: a Story in Four Quarks. In Atomicity in System Design and Execution. Dagstuhl Seminar Proceedings, Volume 4181, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2004)

Copy BibTex To Clipboard

@InProceedings{jones_et_al:DagSemProc.04181.1,
  author =	{Jones, Cliff and Lomet, David and Romanovsky, Alexander and Weikum, Gerhard and Fekete, Alan and Gaudel, Marie-Claude and Korth, Henry F. and de Lemos, Rogerio and Moss, Eliot and Rajwar, Ravi and Ramamritham, Krithi and Randell, Brian and Rodrigues, Luis},
  title =	{{The Atomic Manifesto: a Story in Four Quarks}},
  booktitle =	{Atomicity in System Design and Execution},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2004},
  volume =	{4181},
  editor =	{Cliff Jones and David Lomet and Alexander Romanovsky and Gerhard Weikum},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04181.1},
  URN =		{urn:nbn:de:0030-drops-93},
  doi =		{10.4230/DagSemProc.04181.1},
  annote =	{Keywords: Atomic Actions , Transaction Processing , Database Systems , Dependability , Fault Tolerance , Formal Methods , Correctness Reasoning}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact