You should take a look at two projects I’ve been working on that are relevant to this: my Formalized Agent Foundations repo which includes LLM-driven Lean formalizations of multiple agent foundations papers, including Logical Induction and Condensation (although not yet Natural Latents) and slightly less relevant but similar in ethos, my Alignment Workspace repo where I’ve been using LLMs to help me do semi-automated agent foundations research (especially trying to extend Logical Induction into a solution to the Learning Normativity agenda.) I’ve been considering formalizing Natural Latents as well, although I’ve only really worked on what I see as the necessary first step, which is an automatic converter between the paper’s diagrammatic theorem statements and Lean. An unfinished first attempt at that idea can be found at this branch of the FAF repo.
Wow, really appreciate the formalization of these papers, including Logical Induction which I helped write. Looks like there was an error in the paper (finite perturbations) although a corrected statement works.
Yes, finite perturbations as originally stated was incorrect because it’s possible to encode infinite information into finitely many days’ worth of perturbations, if you perturb infinitely many prices (so the theorem works if you just touch finitely many total sentences instead of finitely many days, assuming prices are rational.) I’m pretty proud of that formalization especially, it has taken about 2 months of heavy back and forth work between me and the agents! (Non-slop human written README for it coming soon)
You should take a look at two projects I’ve been working on that are relevant to this: my Formalized Agent Foundations repo which includes LLM-driven Lean formalizations of multiple agent foundations papers, including Logical Induction and Condensation (although not yet Natural Latents) and slightly less relevant but similar in ethos, my Alignment Workspace repo where I’ve been using LLMs to help me do semi-automated agent foundations research (especially trying to extend Logical Induction into a solution to the Learning Normativity agenda.) I’ve been considering formalizing Natural Latents as well, although I’ve only really worked on what I see as the necessary first step, which is an automatic converter between the paper’s diagrammatic theorem statements and Lean. An unfinished first attempt at that idea can be found at this branch of the FAF repo.
Wow, really appreciate the formalization of these papers, including Logical Induction which I helped write. Looks like there was an error in the paper (finite perturbations) although a corrected statement works.
Yes, finite perturbations as originally stated was incorrect because it’s possible to encode infinite information into finitely many days’ worth of perturbations, if you perturb infinitely many prices (so the theorem works if you just touch finitely many total sentences instead of finitely many days, assuming prices are rational.) I’m pretty proud of that formalization especially, it has taken about 2 months of heavy back and forth work between me and the agents! (Non-slop human written README for it coming soon)