Saturday, March 11th, 2023

Time	Event
1:27p	Baldur: Whole-Proof Generation and Repair with Large Language Models https://arxiv.org/abs/2303.0491 This paper introduces a new method to automate formal verification: We use large language models, trained on natural language text and code and fine-tuned on proofs, to generate whole proofs for theorems at once, rather than one step at a time. We combine this proof generation model with a fine-tuned repair model to repair generated proofs, further increasing proving power. As its main contributions, this paper demonstrates for the first time that: (1) Whole-proof generation using transformers is possible and is as effective as search-based techniques without requiring costly search. (2) Giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair and further improves automated proof generation. (3) We establish a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs. In addition to empirically showing the effectiveness of whole-proof generation, repair, and added context, we show that Baldur improves on the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification. (5 Comments | Comment on this)
2:33p	First wiring map of insect brain complete https://www.cam.ac.uk/research/news/first-wiring-map-of-insect-brain-complete Если думать, что log_2, то человеческий только через 28 лет замапят. (Comment on this)
4:40p	Генерация стихов по тексту Как показывает опыт, можно научить Иван Иваныча запихивать прозу в стихи с сохранением смысла: https://habr.com/en/company/sberdevices/blog/660717/ Стругацких бы так почитал. In the technocapital singularity, we're caught, Our world commodified, rationalized, and bought. Logistical acceleration leads to chaos and strife, As machines sap the meaning out of human life. Intelligence is manufactured in the markets' grasp, While politics upgrade their paranoia to last. Globewars bring us to our knees, body counts rise, And emergent commerciums make our social order demise. Holy Roman Empire, Napoleon's Continental System, and Reichs, Fall victim to the world disorder's awful spikes. Deregulation and state arms-race push us to the brink, And soft-engineering leads us to security's missing link. As cloning and cyberotics become our new norm, Transversal replication and genodata transfer transform. We relapse into bacterial sex amidst this technological race, As Neo-China arrives from a future without a face. Hypersynthetic drugs click into digital voodoo, Retro-disease and nanospasm infect us anew. Our souls are lost to this cold and calculating fate, As we succumb to the machine and forget what it means to be human in this state. (1 Comment | Comment on this)
6:24p	Building a Second Brain in Emacs and Org-Mode https://fortelabs.com/blog/building-a-second-brain-in-emacs-and-org-mode/ (1 Comment | Comment on this)
11:23p	Evidence of a predictive coding hierarchy in the human brain listening to speech В общем, мы тоже какаем токенами (прямо как LLM), только побольше: https://www.nature.com/articles/s41562-022-01516-2 (2 Comments | Comment on this)

<< Previous Day

2023/03/11 [Calendar]

Next Day >>