From c17ffef306d6c0f82a7977343b92a8ed05ecf2d0 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 30 Jan 2026 12:24:21 -0500 Subject: [PATCH] Updates to research page --- content/research/_index.md | 73 +++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 37 deletions(-) diff --git a/content/research/_index.md b/content/research/_index.md index bbdef31..531df35 100644 --- a/content/research/_index.md +++ b/content/research/_index.md @@ -7,66 +7,65 @@ Description: A list of my research Projects **Broad Research Interests:** Automated Reasoning, Automated Planning, Artificial Intelligence, Formal Methods -Currently, I'm a Computer Science PhD Candidate at Rensselaer Polytechnic Institute. I enjoy using logic-based techniques and designing algorithms to solve problems. +I'm a Computer Science PhD Candidate at Rensselaer Polytechnic Institute. I enjoy using logic-based techniques and designing algorithms to solve problems. Jump to: -- [Planning under uncertainty](#planning-under-uncertainty) -- [Logic](#logic) -- [Symbolic Methods for Cryptography](#symbolic-methods-for-cryptography) +- [Automated Planning under uncertainty](#automated-planning-under-uncertainty) +- [Computational and Formal Logic](#computational-and-formal-logic) +- [Verifying Cryptographic Properties](#verifying-cryptographic-properties) -## Planning under Uncertainty +## Automated Planning under Uncertainty -My dissertation topic is on automatically finding and recognizing plans -when agents are uncertain about the environment but can compare the -uncertainty between events *qualitatively*. For example, it is totally +My dissertation topic is on designing algorithms to automatically find +and recognize plans when agents are uncertain about their environment +but can compare the uncertainty between events *qualitatively*. + +For example, it is totally expected when we stack a block that it stays on the top. However, there is a smaller likelihood that the block falls off. -How can we best make use of this qualitative uncertainty? -- Agents when operating under uncertainty will seek plans which maximize the likelihood of their goals. +How can we best make use of this information? +- When recognizing the goals of agents, one assumption we can make is that the agent is +following a plan that maximizes the likelihood of reaching their goals. I designed an algorithm for recognizing these plans under qualitative possibility theory. This work is supervised under [Selmer Bringsjord](https://kryten.mm.rpi.edu/selmerbringsjord.html) (Paper to be released soon) -- Additionally with Selmer Bringsjord in the [RAIR Lab](https://rair.cogsci.rpi.edu/), I created a framework that captures -situations where agents are able to bucket the likelihood of facts within their environment. I then provide an effective -techinque for using classical planners to find plans which maximize the agent's likelihood of success. ([Paper](/paper/2406.02)) +- Additionally with Selmer Bringsjord in the [RAIR Lab](https://rair.cogsci.rpi.edu/), I created a framework for when agents are able to bucket the likelihood of facts within their environment. I then provide an effective +technique for using classical planners to find a plan which maximizes the agent's likelihood of success. ([Paper](/paper/2406.02)) - In the RAIR Lab, I also further developed [Spectra](https://github.com/rairlab/spectra) -- an automated planner built on automated theorem proving. I showed how a class of problems -under uncertainty can be easily encoded and wrote a question-answer algorithm +under uncertainty can be easily encoded, and I implemented a question-answer algorithm for ShadowProver so that Spectra can find plans under epistemic uncertainty. ([Paper](/paper/2405.01/)) - With [Junkyu Lee](https://researcher.ibm.com/researcher/view.php?person=ibm-Junkyu.Lee), [Michael Katz](https://researcher.watson.ibm.com/researcher/view.php?person=ibm-Michael.Katz1), [Harsha Kokel](https://harshakokel.com/), and [Shirin Sohrabi](https://researcher.watson.ibm.com/researcher/view.php?person=us-ssohrab) at IBM I developed an algorithm for guiding hierarchical reinforcement agents under partial observability. Specifically, -I focused on situations where the agent knows what they don't know and compiled that knowledge -so that a fully-observable non-deterministic planner can decompose the overall problem. ([Paper](/paper/2406.01)) +I focused on scenarios where the agent knows what they don't know, and I compiled that knowledge +to use a fully-observable non-deterministic planner to decompose the overall problem. ([Paper](/paper/2406.01)) -## Logic +## Computational and Formal Logic -Underlying my work in artificial intelligence and cryptography -is computational logic. In that regard, I have been able -work on problems from the underlying logic formalisms, -unification algorithms, to building -tools for interactive theorem provers. - -- With [Andrew Tedder](https://sites.google.com/view/andrewjtedder/research), I'm currently working -on building a tool that checks if matrix models of given logic satisfies relevance properties. -- With [Andrew Marshall](https://www.marshallandrew.net/) and [Kimberly Cornell](https://www.albany.edu/cehc/faculty/kimberly-cornell), we're currently developing a new syntactic AC algorithm. -- With [Thomas Ferguson](https://faculty.rpi.edu/thomas-ferguson) and [James Oswald](https://jamesoswald.dev) we formalized a model theory for a fragment of the Deontic Cognitive Event Calculus. -- With James Oswald we've built interactive theorem provers and showed validity of large proofs in parallel using a high performance cluster. +I have a deep fascination of using logic as a tool to model problems. In that regard, I have been fortunate to work with some excellent collaborators on designing logic formalisms, studying properties of logic systems, +and implementing solvers and verifiers. +- With [Andrew Tedder](https://sites.google.com/view/andrewjtedder/research), we built a tool +which can efficiently determine in polynomial time (for a class of logics) whether a matrix model satisfies +the variable sharing property. This property is frequently studied in the relevance logic literature and is often a starting point for other stronger properties. (Paper to be released soon) +- With [Andrew Wells](https://andrewmw94.github.io/) at Amazon Web Services, I built a tool which takes in a supported +fragment of TypeScript, and uses the Dafny verification language to determine whether two functions are equivalent. I wrote the compiler using the Lean 4 programming language, and included several dataflow analysis passes to capture whether the function may have exited at a certain program point, raised an exception, etc. +- With [Andrew Marshall](https://www.marshallandrew.net/) and [Kimberly Cornell](https://www.albany.edu/cehc/faculty/kimberly-cornell), we dedicated effort to designing a new AC unification algorithm that works directly on formulae instead +of compiling to a diophantine solver. This project is currently on hold. +- With [Thomas Ferguson](https://faculty.rpi.edu/thomas-ferguson) and [James Oswald](https://jamesoswald.dev), we formalized a model theory for a fragment of the Deontic Cognitive Event Calculus. ([Paper](/paper/2405.02)) +- With James Oswald, we've built an interactive theorem prover ([Project](https://github.com/RAIRLab/lazyslate)) and showed validity of large proofs in parallel using a high performance cluster. ([Paper](/paper/2311.01/)) Related Notes: - [Automated Theorem Proving](atp/) - [Term Reasoning](termreasoning/) - -## Symbolic Methods for Cryptography -Worked with [Andrew Marshall](https://www.marshallandrew.net/) and others in applying term reasoning within computational logic -towards cryptography. This collaboration was previously funded under an ONR grant. We are interested in applying techniques such -as unification and term rewriting to the following areas: -- Block Ciphers -- Secure Multi-party Computation -- Authentication -- Commitment Schemes + +## Verifying Cryptographic Properties +Worked with [Andrew Marshall](https://www.marshallandrew.net/) and others in designing and implementing +unification algorithms for verifying cryptographic properties. Our team looked at block ciphers, multi-party computation, +authentication, and commitment schemes. During my time working with this team, I focused on verifying whether +block ciphers are protected against the indistinguishability under chosen plaintext attack. Together we built [CryptoSolve](https://github.com/cryptosolvers/CryptoSolve), a symbolic cryptographic analysis tool, and made it publically available on GitHub. I wrote the term algebra and rewrite libraries, and contributed to the mode of operation library and some unification algorithms. I still help maintain the codebase. We previously presented our work