Ramana Kumar

According to our database, Ramana Kumar authored at least 46 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Evaluating Frontier Models for Dangerous Capabilities.

Mary Phuong, Matthew Aitchison, Elliot Catt, Sarah Cogan, Alexandre Kaskasoli, Victoria Krakovna, David Lindner, Matthew Rahtz, Yannis Assael, Sarah Hodkinson, Heidi Howard, Tom Lieberum, Ramana Kumar, Maria Abi Raad, Albert Webson, Lewis Ho, Sharon Lin, Sebastian Farquhar, Marcus Hutter, Grégoire Delétang, Anian Ruoss, Seliem El-Sayed, Sasha Brown, Anca D. Dragan, Rohin Shah, Allan Dafoe, Toby Shevlane

CoRR, 2024

Discovering Agents (Abstract Reprint).

Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt

Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023

Discovering agents.

Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt

Artif. Intell., September, 2023

Cakes That Bake Cakes: Dynamic Computation in CakeML.

Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens

Proc. ACM Program. Lang., 2023

Explaining grokking through circuit efficiency.

Vikrant Varma, Rohin Shah, Zachary Kenton, János Kramár, Ramana Kumar

CoRR, 2023

Scaling Goal-based Exploration via Pruning Proto-goals.

Akhil Bagaria, Ray Jiang, Ramana Kumar, Tom Schaul

CoRR, 2023

2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox

Dagstuhl Artifacts Ser., 2022

Solving math word problems with process- and outcome-based feedback.

Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, Irina Higgins

CoRR, 2022

Goal Misgeneralization: Why Correct Specifications Aren't Enough For Correct Goals.

Rohin Shah, Vikrant Varma, Ramana Kumar, Mary Phuong, Victoria Krakovna, Jonathan Uesato, Zac Kenton

CoRR, 2022

Safe Deep RL in 3D Environments using Human Feedback.

Matthew Rahtz, Vikrant Varma, Ramana Kumar, Zachary Kenton, Shane Legg, Jan Leike

CoRR, 2022

Candle: A Verified Implementation of HOL Light.

Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML.

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021

Reward tampering problems and solutions in reinforcement learning: a causal influence diagram perspective.

Tom Everitt, Marcus Hutter, Ramana Kumar, Victoria Krakovna

Synth., 2021

TacticToe: Learning to Prove with Tactics.

Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish

J. Autom. Reason., 2021

Formal Methods for the Informal Engineer: Workshop Recommendations.

Gopal Sarma, James Koppel, Gregory Malecha, Patrick Schultz, Eric Drexler, Ramana Kumar, Cody Roux, Philip Zucker

CoRR, 2021

2020

Proof-Producing Synthesis of CakeML from Monadic HOL Functions.

Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan

J. Autom. Reason., 2020

Avoiding Tampering Incentives in Deep RL via Decoupled Approval.

Jonathan Uesato, Ramana Kumar, Victoria Krakovna, Tom Everitt, Richard Ngo, Shane Legg

CoRR, 2020

REALab: An Embedded Perspective on Tampering.

Ramana Kumar, Jonathan Uesato, Richard Ngo, Tom Everitt, Victoria Krakovna, Shane Legg

CoRR, 2020

2019

The verified CakeML compiler backend.

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

J. Funct. Program., 2019

Verified compilation on a verified processor.

Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Modeling AGI Safety Frameworks with Causal Influence Diagrams.

Tom Everitt, Ramana Kumar, Victoria Krakovna, Shane Legg

Proceedings of the Workshop on Artificial Intelligence Safety 2019 co-located with the 28th International Joint Conference on Artificial Intelligence, 2019

2018

Learning to Prove with Tactics.

Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish

CoRR, 2018

Clocked Definitions in HOL.

Ramana Kumar, Magnus O. Myreen

CoRR, 2018

Verified Certificate Checking for Counting Votes.

Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.

Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).

Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Verifying efficient function calls in CakeML.

Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan

Proc. ACM Program. Lang., 2017

Verified Characteristic Formulae for CakeML.

Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish

Proceedings of the Programming Languages and Systems, 2017

Verified compilation of CakeML to multiple machine-code targets.

Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.

Yutaka Nagashima, Ramana Kumar

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

J. Autom. Reason., 2016

A Proof Strategy Language and Proof Script Generation for Isabelle.

Yutaka Nagashima, Ramana Kumar

CoRR, 2016

A new verified compiler backend for CakeML.

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Functional Big-Step Semantics.

Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan

Proceedings of the Programming Languages and Systems, 2016

2015

Pattern Matches in HOL: - A New Representation and Improved Code Generation.

Thomas Tuerk, Magnus O. Myreen, Ramana Kumar

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Proof-Producing Reflection for HOL - With an Application to Model Polymorphism.

Benja Fallenstein, Ramana Kumar

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A verified type system for CakeML.

Yong Kiam Tan, Scott Owens, Ramana Kumar

Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, 2015

2014

CakeML: a verified implementation of ML.

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

HOL with Definitions: Semantics, Soundness, and a Verified Implementation.

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Steps towards Verified Implementations of HOL Light.

Magnus O. Myreen, Scott Owens, Ramana Kumar

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4.

Ramana Kumar

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

Standalone Tactics Using OpenTheory.

Ramana Kumar, Joe Hurd

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Validating QBF Validity in HOL4.

Ramana Kumar, Tjark Weber

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study.

Naghmeh Ghafari, Ramana Kumar, Jeff Joyce, Bernd Dehning, Christos Zamantzas

Proceedings of the Formal Methods for Industrial Critical Systems, 2011

2010

(Nominal) Unification by Recursive Descent with Triangular Substitutions.

Ramana Kumar, Michael Norrish

Proceedings of the Interactive Theorem Proving, First International Conference, 2010