![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
DeepMind has formalized a theoretical result related to AI safety in Lean
Lean theorem prover seems to be the most convenient and practical (good enough for mathematicians to use it in real work, I am seeing plenty of such stories lately; there is a bit of controversy on whether to use Lean 3 or Lean 4).
The best quote according to "leanprover" twitter:
>Our favorite quote from the paper: "Monadic syntax is excellent for expressing stochastic algorithms, and working over finitely supported distributions avoids the need for integrability side conditions during proofs."
Links are in the comments.
The best quote according to "leanprover" twitter:
>Our favorite quote from the paper: "Monadic syntax is excellent for expressing stochastic algorithms, and working over finitely supported distributions avoids the need for integrability side conditions during proofs."
Links are in the comments.
no subject
https://arxiv.org/abs/2311.14125, "Scalable AI Safety via Doubly-Efficient Debate"
https://github.com/google-deepmind/debate
no subject
Ничего себе новости!
no subject
Теренсе Тао тоже всё время работает и с Lean, и с GPT-4, я читаю, время от времени, его https://mathstodon.xyz/@tao