This episode explores DafnyBench, a benchmark for testing whether large language models can help with one of formal verification’s hardest practical bottlenecks: reconstructing the missing assertions and loop invariants that make Dafny programs verifiable. It explains how formal verification differs from ordinary testing and from theorem proving, and why the paper deliberately frames the task as restoring proof hints in existing verified programs rather than synthesizing correct software from scratch. The discussion digs into benchmark design, including the dataset of 782 single-file Dafny programs, the rule that models must infer both the content and placement of missing hints, and the importance of excluding shortcut tricks like disabling verification. It also highlights a crucial result nuance: 208 files already verify after hint removal, so the reported top score of about 67.8% is more informative when translated into genuine recovery performance on the subset that actually needs new annotations.

Sources:

1. DafnyBench: A Benchmark for Formal Software Verification — Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark, 2024

http://arxiv.org/abs/2406.08467

2. Clover: Closed-Loop Verifiable Code Generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2024

https://scholar.google.com/scholar?q=Clover%3A+Closed-Loop+Verifiable+Code+Generation

3. Towards AI-Assisted Synthesis of Verified Dafny Methods — Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, James Noble, 2024

https://scholar.google.com/scholar?q=Towards+AI-Assisted+Synthesis+of+Verified+Dafny+Methods

4. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models — Kaiyu Yang et al., 2023

https://scholar.google.com/scholar?q=LeanDojo%3A+Theorem+Proving+with+Retrieval-Augmented+Language+Models

5. LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code — Naman Jain et al., 2024

https://scholar.google.com/scholar?q=LiveCodeBench%3A+Holistic+and+Contamination+Free+Evaluation+of+Large+Language+Models+for+Code

6. Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification — Xu Xu et al., 2025

https://scholar.google.com/scholar?q=Local+Success+Does+Not+Compose%3A+Benchmarking+Large+Language+Models+for+Compositional+Formal+Verification

7. A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification — Norbert Tihanyi et al., 2023

https://scholar.google.com/scholar?q=A+New+Era+in+Software+Security%3A+Towards+Self-Healing+Software+via+Large+Language+Models+and+Formal+Verification

8. AI Post Transformers: LLM Agents Reason About Code Without Running It — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-15-llm-agents-reason-about-code-without-run-2a1876.mp3

9. AI Post Transformers: SkillsBench for Evaluating Agent Skills — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-14-skillsbench-for-evaluating-agent-skills-58bb1e.mp3

This episode explores DeepMind’s From AGI to ASI as a foresight report that treats human-level general intelligence not as the endpoint, but as a possible stepping stone toward systems that could outperform entire organizations in planning, research, engineering, and coordination. It breaks down how the paper defines AGI and the much more ambitious idea of ASI, then examines the conceptual tools behind that framing, including universal intelligence, AIXI as an idealized reference point, recursive self-improvement, collective intelligence, and the notion of effective compute. The discussion also probes the paper’s method, arguing that it is a structured synthesis of trends and bottlenecks rather than empirical proof, and questions how much precision is needed before such forecasts become meaningful. Listeners would find it interesting because it connects abstract AI theory, concrete scaling dynamics, and real uncertainty about whether progress in models, compute, and autonomy could compound into organization-level superintelligence.

Sources:

1. From AGI to ASI — Tim Genewein, Matija Franklin, Alexander Lerchner, Laurent Orseau, Samuel Albanie, Adam Bales, Cole Wyeth, Stephanie Chan, Iason Gabriel, Joel Z. Leibo, Allan Dafoe, Marcus Hutter, Thore Graepel, Shane Legg, 2026

http://arxiv.org/abs/2606.12683

2. From AGI to ASI (https://arxiv.org/abs/2606.12683) — Tim Genewein, Matija Franklin, Alexander Lerchner, Marcus Hutter, Shane Legg, et al., 2026

https://scholar.google.com/scholar?q=From+AGI+to+ASI+%28https%3A%2F%2Farxiv.org%2Fabs%2F2606.12683%29

3. Can Intelligence Explode? (https://arxiv.org/abs/1202.6177) — Marcus Hutter, 2012

https://scholar.google.com/scholar?q=Can+Intelligence+Explode%3F+%28https%3A%2F%2Farxiv.org%2Fabs%2F1202.6177%29

4. Research Priorities for Robust and Beneficial Artificial Intelligence (https://arxiv.org/abs/1602.03506) — Stuart Russell, Daniel Dewey, Max Tegmark, 2015

https://scholar.google.com/scholar?q=Research+Priorities+for+Robust+and+Beneficial+Artificial+Intelligence+%28https%3A%2F%2Farxiv.org%2Fabs%2F1602.03506%29

5. Emerging Practices in Frontier AI Safety Frameworks (https://arxiv.org/abs/2503.04746) — Marie Davidsen Buhl, Ben Bucknall, Tammy Masterson, 2025

https://scholar.google.com/scholar?q=Emerging+Practices+in+Frontier+AI+Safety+Frameworks+%28https%3A%2F%2Farxiv.org%2Fabs%2F2503.04746%29

6. A Theory of Universal Artificial Intelligence based on Algorithmic Complexity (https://arxiv.org/abs/cs/0004001) — Marcus Hutter, 2000

https://scholar.google.com/scholar?q=A+Theory+of+Universal+Artificial+Intelligence+based+on+Algorithmic+Complexity+%28https%3A%2F%2Farxiv.org%2Fabs%2Fcs%2F0004001%29

7. Universal Intelligence: A Definition of Machine Intelligence (https://arxiv.org/abs/0712.3329) — Shane Legg, Marcus Hutter, 2007

https://scholar.google.com/scholar?q=Universal+Intelligence%3A+A+Definition+of+Machine+Intelligence+%28https%3A%2F%2Farxiv.org%2Fabs%2F0712.3329%29

8. A Monte Carlo AIXI Approximation (https://arxiv.org/abs/0909.0801) — Joel Veness, Kee Siong Ng, Marcus Hutter, William Uther, David Silver, 2009 (later published in JAIR, 2011)

https://scholar.google.com/scholar?q=A+Monte+Carlo+AIXI+Approximation+%28https%3A%2F%2Farxiv.org%2Fabs%2F0909.0801%29

9. One Decade of Universal Artificial Intelligence (https://arxiv.org/abs/1202.6153) — Marcus Hutter, 2012

https://scholar.google.com/scholar?q=One+Decade+of+Universal+Artificial+Intelligence+%28https%3A%2F%2Farxiv.org%2Fabs%2F1202.6153%29

10. Universal Intelligence: A Definition of Machine Intelligence — Shane Legg, Marcus Hutter, 2007

https://scholar.google.com/scholar?q=Universal+Intelligence%3A+A+Definition+of+Machine+Intelligence

11. Levels of AGI for Operationalizing Progress on the Path to AGI — Meredith Ringel Morris, Jascha Sohl-Dickstein, Noah Fiedel, Tris Warkentin, Allan Dafoe, Aleksandra Faust, Clement Farabet, Shane Legg, 2023

https://scholar.google.com/scholar?q=Levels+of+AGI+for+Operationalizing+Progress+on+the+Path+to+AGI

12. AI as Normal Technology — Arvind Narayanan, Sayash Kapoor, 2025

https://scholar.google.com/scholar?q=AI+as+Normal+Technology

13. Preparing for the Intelligence Explosion — William MacAskill, Fin Moorhouse, 2025

https://scholar.google.com/scholar?q=Preparing+for+the+Intelligence+Explosion

14. A Rosetta Stone for AI Benchmarks — Anson Ho, Jean-Stanislas Denain, David Atanasov, Samuel Albanie, Rohin Shah, 2025

https://scholar.google.com/scholar?q=A+Rosetta+Stone+for+AI+Benchmarks

15. Measuring AI Ability to Complete Long Tasks — Thomas Kwa et al., 2025

https://scholar.google.com/scholar?q=Measuring+AI+Ability+to+Complete+Long+Tasks

16. PaperBench: Evaluating AI's Ability to Replicate AI Research — Giulio Starace et al., 2025

https://scholar.google.com/scholar?q=PaperBench%3A+Evaluating+AI%27s+Ability+to+Replicate+AI+Research

17. Inverse Scaling in Test-Time Compute — Aryo P. Gema et al., 2025

https://scholar.google.com/scholar?q=Inverse+Scaling+in+Test-Time+Compute

18. The Art of Scaling Test-Time Compute for Large Language Models — Aradhye Agarwal et al., 2025

https://scholar.google.com/scholar?q=The+Art+of+Scaling+Test-Time+Compute+for+Large+Language+Models

19. Test-Time Scaling Makes Overtraining Compute-Optimal — Nicholas Roberts et al., 2026

https://scholar.google.com/scholar?q=Test-Time+Scaling+Makes+Overtraining+Compute-Optimal

20. When AI Benchmarks Plateau: A Systematic Study of Benchmark Saturation — Mubashara Akhtar et al., 2026

https://scholar.google.com/scholar?q=When+AI+Benchmarks+Plateau%3A+A+Systematic+Study+of+Benchmark+Saturation

21. How Bad is Training on Synthetic Data? A Statistical Analysis of Language Model Collapse — Mohamed El Amine Seddik et al., 2024

https://scholar.google.com/scholar?q=How+Bad+is+Training+on+Synthetic+Data%3F+A+Statistical+Analysis+of+Language+Model+Collapse

22. Is Model Collapse Inevitable? Breaking the Curse of Recursion by Accumulating Real and Synthetic Data — Matthias Gerstgrasser et al., 2024

https://scholar.google.com/scholar?q=Is+Model+Collapse+Inevitable%3F+Breaking+the+Curse+of+Recursion+by+Accumulating+Real+and+Synthetic+Data

23. MLGym: A New Framework and Benchmark for Advancing AI Research Agents — Deepak Nathani et al., 2025

https://scholar.google.com/scholar?q=MLGym%3A+A+New+Framework+and+Benchmark+for+Advancing+AI+Research+Agents

24. MLAgentBench: Evaluating Language Agents on Machine Learning Experimentation — Qian Huang et al., 2023

https://scholar.google.com/scholar?q=MLAgentBench%3A+Evaluating+Language+Agents+on+Machine+Learning+Experimentation

25. AI Post Transformers: Technical AGI Safety and Security Framework — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-03-technical-agi-safety-and-security-framew-f27316.mp3

26. AI Post Transformers: Unified Neural Scaling Laws Across Regimes — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-07-unified-neural-scaling-laws-across-regim-292e2d.mp3

27. AI Post Transformers: TUMIX Multi-Agent Test-Time Scaling with Tools — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-22-tumix-multi-agent-test-time-scaling-with-40671c.mp3

28. AI Post Transformers: Test-time Scaling for Multi-Agent Collaborative Reasoning — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-22-test-time-scaling-for-multi-agent-collab-082570.mp3

Interactive Visualization: From AGI to ASI and Beyond

This episode explores MiniMax Sparse Attention, a long-context transformer design that aims to preserve dense-model quality at million-token scale while sharply reducing the quadratic compute and memory costs of standard attention. It explains how the method combines Grouped Query Attention with blockwise sparse retrieval: a lightweight Index Branch scores past context in blocks, forces a recent local block to stay visible, selects top-k candidate regions, and then lets a Main Branch run exact softmax attention only inside those chosen blocks. The discussion places the paper alongside Longformer, BigBird, Routing Transformers, MInference, and Native Sparse Attention, arguing that its main contribution is a simpler, more GPU-friendly routing scheme that could make sparse attention practical at deployment time. Listeners would find it interesting because it focuses on the real technical tension behind ultra-long-context models: whether this kind of sparse routing can reliably recover rare distant evidence, or whether it mainly wins through recency bias and careful systems engineering.

Sources:

1. MiniMax Sparse Attention — Xunhao Lai, Weiqi Xu, Yufeng Yang, Qiaorui Chen, Yang Xu, Lunbin Zeng, Xiaolong Li, Haohai Sun, Haichao Zhu, Vito Zhang, Pengyu Zhao, 2026

http://arxiv.org/abs/2606.13392

2. Longformer: The Long-Document Transformer — Iz Beltagy, Matthew E. Peters, Arman Cohan, 2020

https://scholar.google.com/scholar?q=Longformer%3A+The+Long-Document+Transformer

3. Big Bird: Transformers for Longer Sequences — Manzil Zaheer, Guru Guruganesh, Avinava Dubey, Joshua Ainslie, Chris Alberti, Amr Ahmed, 2020

https://scholar.google.com/scholar?q=Big+Bird%3A+Transformers+for+Longer+Sequences

4. Efficient Content-Based Sparse Attention with Routing Transformers — Aurko Roy, Mohammad Saffar, Ashish Vaswani, David Grangier, 2020

https://scholar.google.com/scholar?q=Efficient+Content-Based+Sparse+Attention+with+Routing+Transformers

5. Native Sparse Attention: Hardware-Aligned and Natively Trainable Sparse Attention — Jingyang Yuan, Huazuo Gao, Damai Dai, Junyu Luo, Liang Zhao, Wenfeng Liang, Wangding Zeng, 2025

https://scholar.google.com/scholar?q=Native+Sparse+Attention%3A+Hardware-Aligned+and+Natively+Trainable+Sparse+Attention

6. GQA: Training Generalized Multi-Query Transformer Models from Multi-Head Checkpoints — Joshua Ainslie et al., 2025

https://scholar.google.com/scholar?q=GQA%3A+Training+Generalized+Multi-Query+Transformer+Models+from+Multi-Head+Checkpoints

7. Optimizing Mixture of Block Attention — Guangxuan Xiao et al., 2025

https://scholar.google.com/scholar?q=Optimizing+Mixture+of+Block+Attention

8. MInference 1.0: Accelerating Pre-filling for Long-Context LLMs via Dynamic Sparse Attention — Huiqiang Jiang et al., 2024

https://scholar.google.com/scholar?q=MInference+1.0%3A+Accelerating+Pre-filling+for+Long-Context+LLMs+via+Dynamic+Sparse+Attention

9. DuoAttention: Efficient Long-Context LLM Inference with Retrieval and Streaming Heads — Guangxuan Xiao et al., 2024

https://scholar.google.com/scholar?q=DuoAttention%3A+Efficient+Long-Context+LLM+Inference+with+Retrieval+and+Streaming+Heads

10. FlashAttention-3: Fast and Accurate Attention with Asynchrony and Low-precision — Jay Shah, Ganesh Bikshandi, Ying Zhang, Vijay Thakkar, Pradeep Ramani, Tri Dao, 2024

https://scholar.google.com/scholar?q=FlashAttention-3%3A+Fast+and+Accurate+Attention+with+Asynchrony+and+Low-precision

11. FIER: Fine-Grained and Efficient KV Cache Retrieval for Long-context LLM Inference — Dongwei Wang et al., 2025

https://arxiv.org/abs/2508.08256

12. SCBench: A KV Cache-Centric Analysis of Long-Context Methods — Yucheng Li et al., 2024

https://arxiv.org/abs/2412.10319

13. Streaming Video Question-Answering with In-context Video KV-Cache Retrieval — Shangzhe Di et al., 2025

https://arxiv.org/abs/2503.00540

14. Native Hybrid Attention for Efficient Sequence Modeling — Jusen Du et al., 2025

https://arxiv.org/abs/2510.07019

15. Rope to Nope and Back Again: A New Hybrid Attention Strategy — Bowen Yang et al., 2025

https://arxiv.org/abs/2501.18795

16. AI Post Transformers: Optimizing Mixture of Block Attention Through Statistical Theory — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-18-optimizing-mixture-of-block-attention-th-214f91.mp3

17. AI Post Transformers: Deep Kernel Fusion for Transformer Decoding — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-15-deep-kernel-fusion-for-transformer-decod-b1a703.mp3

18. AI Post Transformers: Mooncake for KV Cache-Centric LLM Serving — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-05-mooncake-for-kv-cache-centric-llm-servin-1086d0.mp3

19. AI Post Transformers: How Induction Heads Emerge in Transformers — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-03-how-induction-heads-emerge-in-transforme-a7bfcb.mp3

20. AI Post Transformers: δ-mem and Online Memory for LLMs — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-13-d-mem-and-online-memory-for-llms-6622fa.mp3

21. AI Post Transformers: Ministral 3: Cascade Distillation for Long-Context Multimodal Models — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-15-cascade-distillation-for-long-context-mu-0ebd1a.mp3

Interactive Visualization: MiniMax Sparse Attention at Million-Token Scale

This episode explores the ACE proposal from AMD, Intel, and the x86 Ecosystem Advisory Group, which would add matrix-native AI instructions to x86 CPUs so transformer workloads can run dense linear algebra more efficiently without changing the models themselves. It explains why AVX10 and VNNI fall short for GEMM-heavy inference, introducing outer-product updates, 2-D tile registers, and the reuse of the AMX palette model so operating systems and compilers can handle the new state within familiar x86 mechanisms. The discussion also challenges the proposal’s headline 16x compute-density claim for INT8 and BF16, arguing that real speed depends on full-kernel costs like packing, memory traffic, conversions, tails, and cache behavior. It also examines OCP FP8, MXFP8, MXINT8, and BF16 support as a sign that low-precision AI now depends on tight coordination between ISA design, quantization rules, and kernel implementation, making the proposal interesting both technically and strategically.

Sources:

1. ACE: Matrix-Native AI Extensions for x86

https://x86ecosystem.org/wp-content/uploads/2026/03/ACE-Whitepaper-v1.pdf

2. The AI Compute Extensions (ACE) for x86 — Stuart Biles, Brian Thompto, Michael Estlick, Eric Schwarz, Thomas Fox, Gabriel Loh, Marius Evers, Michael Clark, Alexander Heinecke, Pradeep Dubey, Ido Ouziel, 2026

https://scholar.google.com/scholar?q=The+AI+Compute+Extensions+%28ACE%29+for+x86

3. A matrix math facility for Power ISA(TM) processors — José E. Moreira, Kit Barton, Steven Battle, Peter Bergner, Ramon Bertran and others, 2021

https://scholar.google.com/scholar?q=A+matrix+math+facility+for+Power+ISA%28TM%29+processors

4. Hello SME! Generating Fast Matrix Multiplication Kernels Using the Scalable Matrix Extension — Stefan Remke, Alexander Breuer, 2024

https://scholar.google.com/scholar?q=Hello+SME%21+Generating+Fast+Matrix+Multiplication+Kernels+Using+the+Scalable+Matrix+Extension

5. SparAMX: Accelerating Compressed LLMs Token Generation on AMX-powered CPUs — Ahmed F. AbouElhamayed, Jordan Dotzel, Yash Akhauri, Chi-Chih Chang, Sameh Gobriel, J. Pablo Muñoz, Vui Seng Chua, Nilesh Jain, Mohamed S. Abdelfattah, 2025

https://scholar.google.com/scholar?q=SparAMX%3A+Accelerating+Compressed+LLMs+Token+Generation+on+AMX-powered+CPUs

6. Automating the Last-Mile for High Performance Dense Linear Algebra — Richard Michael Veras, Tze Meng Low, Tyler Michael Smith, Robert A. van de Geijn, Franz Franchetti, 2017

https://scholar.google.com/scholar?q=Automating+the+Last-Mile+for+High+Performance+Dense+Linear+Algebra

7. Microscaling Data Formats for Deep Learning — Bita Darvish Rouhani et al., 2023

https://scholar.google.com/scholar?q=Microscaling+Data+Formats+for+Deep+Learning

8. Recipes for Pre-training LLMs with MXFP8 — Asit Mishra, Dusan Stosic, Simon Layton, 2025

https://scholar.google.com/scholar?q=Recipes+for+Pre-training+LLMs+with+MXFP8

9. Fast Matrix Multiplication via Compiler-only Layered Data Reorganization and Intrinsic Lowering — Braedy Kuzma et al., 2023

https://scholar.google.com/scholar?q=Fast+Matrix+Multiplication+via+Compiler-only+Layered+Data+Reorganization+and+Intrinsic+Lowering

10. THOR: A Non-Speculative Value Dependent Timing Side Channel Attack Exploiting Intel AMX — Farshad Dizani et al., 2025

https://scholar.google.com/scholar?q=THOR%3A+A+Non-Speculative+Value+Dependent+Timing+Side+Channel+Attack+Exploiting+Intel+AMX

11. Compute or Load KV Cache? Why Not Both? (https://arxiv.org/abs/2410.03065) — Shuowei Jin et al., 2024

https://scholar.google.com/scholar?q=Compute+or+Load+KV+Cache%3F+Why+Not+Both%3F+%28https%3A%2F%2Farxiv.org%2Fabs%2F2410.03065%29

12. SOLE: Hardware-Software Co-design of Softmax and LayerNorm for Efficient Transformer Inference (https://arxiv.org/abs/2510.17189) — Wenxun Wang et al., 2025

https://scholar.google.com/scholar?q=SOLE%3A+Hardware-Software+Co-design+of+Softmax+and+LayerNorm+for+Efficient+Transformer+Inference+%28https%3A%2F%2Farxiv.org%2Fabs%2F2510.17189%29

13. Towards Fully FP8 GEMM LLM Training at Scale (https://arxiv.org/abs/2505.20524) — Alejandro Hernandez-Cano et al., 2025

https://scholar.google.com/scholar?q=Towards+Fully+FP8+GEMM+LLM+Training+at+Scale+%28https%3A%2F%2Farxiv.org%2Fabs%2F2505.20524%29

14. Pretraining Large Language Models with NVFP4 (https://arxiv.org/abs/2509.25149) — Felix Abecassis et al. (NVIDIA), 2025

https://scholar.google.com/scholar?q=Pretraining+Large+Language+Models+with+NVFP4+%28https%3A%2F%2Farxiv.org%2Fabs%2F2509.25149%29

15. SageAttention3: Microscaling FP4 Attention for Inference and An Exploration of 8-Bit Training (https://arxiv.org/abs/2505.11594) — Jintao Zhang et al., 2025

https://scholar.google.com/scholar?q=SageAttention3%3A+Microscaling+FP4+Attention+for+Inference+and+An+Exploration+of+8-Bit+Training+%28https%3A%2F%2Farxiv.org%2Fabs%2F2505.11594%29

16. AI Post Transformers: Memory-Bound, Not Bandwidth-Limited Batch-1 LLM Decode — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-02-memory-bound-not-bandwidth-limited-batch-114799.mp3

17. AI Post Transformers: LPU Chip for Low-Latency LLM Inference — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-20-lpu-chip-for-low-latency-llm-inference-be13c3.mp3

18. AI Post Transformers: Deep Kernel Fusion for Transformer Decoding — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-15-deep-kernel-fusion-for-transformer-decod-b1a703.mp3

19. AI Post Transformers: FlatAttention for Tile-Based Accelerator Inference — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-04-flatattention-for-tile-based-accelerator-56e6ca.mp3

Interactive Visualization: ACE: Matrix-Native AI Extensions for x86

This episode explores a 2025 paper on using Dafny as a hidden, verification-aware intermediate language for AI code generation, where a model first produces a formal specification and verified implementation before compiling it into ordinary Python. It examines the paper’s central trust claim: formal verification can prove that the generated code satisfies the hidden spec, but it cannot prove that the hidden spec actually matches the user’s intent, making spec alignment a separate and critical failure point. The discussion uses the paper’s fibfib example and HumanEval results to unpack that distinction, noting that the Dafny-only pipeline trails direct Python generation, while the best reported score comes only after falling back to unverified Python when the verification loop fails to converge. Listeners would find it interesting because it gives a concrete, nuanced look at where AI coding assistants can become more reliable, where the guarantees stop, and why neuro-symbolic workflows may matter most for tightly specified code like algorithms, parsers, and protocol logic.

Sources:

1. Dafny as Verification-Aware Intermediate Language for Code Generation — Yue Chen Li, Stefan Zetzsche, Siva Somayyajula, 2025

http://arxiv.org/abs/2501.06283

2. Dafny: An Automatic Program Verifier for Functional Correctness — K. Rustan M. Leino, 2010

https://scholar.google.com/scholar?q=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness

3. Towards AI-Assisted Synthesis of Verified Dafny Methods — Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, James Noble, 2024

https://scholar.google.com/scholar?q=Towards+AI-Assisted+Synthesis+of+Verified+Dafny+Methods

4. Clover: Closed-Loop Verifiable Code Generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2024

https://scholar.google.com/scholar?q=Clover%3A+Closed-Loop+Verifiable+Code+Generation

5. VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search — David Brandfonbrener, Simon Henniger, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Sabrina Ruixin Hu, Jianang Yang, William E. Byrd, Robert Zinkov, Nada Amin, 2024

https://scholar.google.com/scholar?q=VerMCTS%3A+Synthesizing+Multi-Step+Programs+using+a+Verifier%2C+a+Large+Language+Model%2C+and+Tree+Search

6. Laurel: Generating Dafny Assertions Using Large Language Models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024

https://scholar.google.com/scholar?q=Laurel%3A+Generating+Dafny+Assertions+Using+Large+Language+Models

7. DafnyBench: A Benchmark for Formal Software Verification — Chloe Loughridge et al., 2024

https://scholar.google.com/scholar?q=DafnyBench%3A+A+Benchmark+for+Formal+Software+Verification

8. Evaluating Large Language Models Trained on Code — Mark Chen et al., 2021

https://scholar.google.com/scholar?q=Evaluating+Large+Language+Models+Trained+on+Code

9. Baking for Dafny: A CakeML Backend for Dafny — Daniel Nezamabadi, Magnus Myreen, 2025

https://scholar.google.com/scholar?q=Baking+for+Dafny%3A+A+CakeML+Backend+for+Dafny

10. Intent-aligned Formal Specification Synthesis via Traceable Refinement — Zhe Ye et al., 2026

https://scholar.google.com/scholar?q=Intent-aligned+Formal+Specification+Synthesis+via+Traceable+Refinement

11. Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis — William Murphy et al., 2024

https://scholar.google.com/scholar?q=Combining+LLM+Code+Generation+with+Formal+Specifications+and+Reactive+Program+Synthesis

12. StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback — Shihan Dou et al., 2024

https://scholar.google.com/scholar?q=StepCoder%3A+Improve+Code+Generation+with+Reinforcement+Learning+from+Compiler+Feedback

13. InspectCoder: Dynamic Analysis-Enabled Self Repair through interactive LLM-Debugger Collaboration — Yunkun Wang et al., 2025

https://scholar.google.com/scholar?q=InspectCoder%3A+Dynamic+Analysis-Enabled+Self+Repair+through+interactive+LLM-Debugger+Collaboration

14. FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs — Madhurima Chakraborty et al., 2025

https://scholar.google.com/scholar?q=FormalSpecCpp%3A+A+Dataset+of+C%2B%2B+Formal+Specifications+created+using+LLMs

15. AI Post Transformers: From Natural Language to Verified Dafny Code — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-14-from-natural-language-to-verified-dafny-8abed9.mp3

16. AI Post Transformers: Program Synthesis with Large Language Models — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-20-program-synthesis-with-large-language-mo-b962ec.mp3

17. AI Post Transformers: Generative File Systems: Replacing Code with Formal Specifications — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-18-generative-file-systems-replacing-code-w-414029.mp3

This episode explores whether large language models can help mainstream developers write code that is not just plausible, but formally verified in systems like Dafny, Nagini, and Verus. It explains the core ideas behind machine-checked correctness, including contracts, SMT solvers, loop invariants, and why verification is far stricter than passing tests or matching statistical behavior. The discussion highlights the paper’s main argument that the real bottleneck is not only generating implementations, but also generating the formal scaffolding and annotations that proofs require, especially around loops. Listeners get a clear view of how the authors evaluate LLMs with verifier feedback and extra validation to catch weakened specifications, making the episode interesting for anyone curious about whether AI can close the trust gap in code generation.

Sources:

1. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025

http://arxiv.org/abs/2503.14183

2. Inferring Loop Invariants using Postconditions — Carlo A. Furia, Bertrand Meyer, 2009

https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+using+Postconditions

3. Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking — Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller, 2014

https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+by+Mutation%2C+Dynamic+Analysis%2C+and+Static+Checking

4. LoopInvGen: A Loop Invariant Generator based on Precondition Inference — Saswat Padhi, Rahul Sharma, Todd Millstein, 2017

https://scholar.google.com/scholar?q=LoopInvGen%3A+A+Loop+Invariant+Generator+based+on+Precondition+Inference

5. On Scaling Data-Driven Loop Invariant Inference — Sahil Bhatia, Saswat Padhi, Nagarajan Natarajan, Rahul Sharma, Prateek Jain, 2019

https://scholar.google.com/scholar?q=On+Scaling+Data-Driven+Loop+Invariant+Inference

6. Dafny: An Automatic Program Verifier for Functional Correctness — K. Rustan M. Leino, 2010

https://scholar.google.com/scholar?q=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness

7. Nagini: A Static Verifier for Python — Marco Eilers, Peter Muller, 2018

https://scholar.google.com/scholar?q=Nagini%3A+A+Static+Verifier+for+Python

8. Verus: Verifying Rust Programs using Linear Ghost Types (extended version) — Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel, 2023

https://scholar.google.com/scholar?q=Verus%3A+Verifying+Rust+Programs+using+Linear+Ghost+Types+%28extended+version%29

9. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025

https://scholar.google.com/scholar?q=Can+LLMs+Enable+Verification+in+Mainstream+Programming%3F

10. Clover: Closed-loop verifiable code generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2024

https://scholar.google.com/scholar?q=Clover%3A+Closed-loop+verifiable+code+generation

11. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement — Pranjal Aggarwal, Bryan Parno, Sean Welleck, 2024

https://scholar.google.com/scholar?q=Alphaverus%3A+Bootstrapping+formally+verified+code+generation+through+self-improving+translation+and+treefinement

12. Can large language models transform natural language intent into formal method postconditions? — Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri, 2024

https://scholar.google.com/scholar?q=Can+large+language+models+transform+natural+language+intent+into+formal+method+postconditions%3F

13. Laurel: Generating Dafny assertions using large language models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024

https://scholar.google.com/scholar?q=Laurel%3A+Generating+Dafny+assertions+using+large+language+models

14. Finding Inductive Loop Invariants using Large Language Models — Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma, 2023

https://scholar.google.com/scholar?q=Finding+Inductive+Loop+Invariants+using+Large+Language+Models

15. Towards Formal Verification of LLM-Generated Code from Natural Language Prompts — Aaron Councilman et al., 2025

https://arxiv.org/abs/2507.13290

16. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification — Cheng Wen et al., 2024

https://arxiv.org/abs/2404.00762

17. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models — Lezhi Ma et al., 2024

https://arxiv.org/abs/2401.08807

18. Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? — Cedric Richter and Heike Wehrheim, 2025

https://arxiv.org/abs/2510.12702

19. Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors — Tianchi Li et al., 2026

https://arxiv.org/abs/2605.17914

20. Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers — Varun Bharti et al., 2025

https://arxiv.org/abs/2508.00419

21. LLM For Loop Invariant Generation and Fixing: How Far Are We? — Mostafijur Rahman Akhond et al., 2025

https://arxiv.org/abs/2511.06552

22. AI Post Transformers: From Natural Language to Verified Dafny Code — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-14-from-natural-language-to-verified-dafny-8abed9.mp3

23. AI Post Transformers: Generative File Systems: Replacing Code with Formal Specifications — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-18-generative-file-systems-replacing-code-w-414029.mp3

24. AI Post Transformers: Trajectory Summaries for Long-Horizon Coding Agents — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-24-trajectory-summaries-for-long-horizon-co-0194be.mp3

Interactive Visualization: Can LLMs Enable Mainstream Formal Verification?

This episode explores a 2026 study on turning long natural-language programming problems into Dafny code that can be formally verified, asking whether AI systems can produce code that is not just fluent but provably correct. It explains how Dafny uses preconditions, postconditions, loop invariants, and proof obligations, and why weak specifications can lead to vacuous “verified” programs that still fail to capture the real task. The discussion highlights the paper’s NL2VC-60 benchmark of hand-written verified solutions to UVa-style algorithm problems, along with experiments comparing plain prompting, signature-guided prompting, and self-healing loops that revise code using verifier feedback and additional uDebug testing. Listeners would find it interesting because it gets at the core trust problem in AI coding: whether formal methods can make generated software more reliable, and where the real bottleneck remains the human effort required to write strong specifications.

Sources:

1. From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification — Md Erfan, Md Kamal Hossain Chowdhury, Ahmed Ryan, Md Rayhanur Rahman, 2026

http://arxiv.org/abs/2604.22601

2. Dafny: An Automatic Program Verifier for Functional Correctness — K. Rustan M. Leino, 2010

https://scholar.google.com/scholar?q=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness

3. seL4: Formal Verification of an Operating-System Kernel — Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, et al., 2009

https://scholar.google.com/scholar?q=seL4%3A+Formal+Verification+of+an+Operating-System+Kernel

4. Formal verification of a realistic compiler — Xavier Leroy, 2009

https://scholar.google.com/scholar?q=Formal+verification+of+a+realistic+compiler

5. Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification — Son Ho, Aymeric Fromherz, Jonathan Protzenko, 2021

https://scholar.google.com/scholar?q=Modularity%2C+Code+Specialization%2C+and+Zero-Cost+Abstractions+for+Program+Verification

6. Towards AI-Assisted Synthesis of Verified Dafny Methods — Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, James Noble, 2024

https://scholar.google.com/scholar?q=Towards+AI-Assisted+Synthesis+of+Verified+Dafny+Methods

7. DafnyBench: A Benchmark for Formal Software Verification — Chloe Loughridge et al., 2024

https://scholar.google.com/scholar?q=DafnyBench%3A+A+Benchmark+for+Formal+Software+Verification

8. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025

https://scholar.google.com/scholar?q=Can+LLMs+Enable+Verification+in+Mainstream+Programming%3F

9. Dafny as Verification-Aware Intermediate Language for Code Generation — Yue Chen Li, Stefan Zetzsche, Siva Somayyajula, 2025

https://scholar.google.com/scholar?q=Dafny+as+Verification-Aware+Intermediate+Language+for+Code+Generation

10. ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis — Mantas Baksys et al., 2025

https://scholar.google.com/scholar?q=ATLAS%3A+Automated+Toolkit+for+Large-Scale+Verified+Code+Synthesis

11. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs — Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche, 2026

https://scholar.google.com/scholar?q=DafnyPro%3A+LLM-Assisted+Automated+Verification+for+Dafny+Programs

12. Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving — Sumit Kumar Jha et al., 2023

https://scholar.google.com/scholar?q=Neuro+Symbolic+Reasoning+for+Planning%3A+Counterexample+Guided+Inductive+Synthesis+using+Large+Language+Models+and+Satisfiability+Solving

13. Property-Guided LLM Program Synthesis for Planning — Andre G. Pereira, Augusto B. Correa, Jendrik Seipp, 2026

https://scholar.google.com/scholar?q=Property-Guided+LLM+Program+Synthesis+for+Planning

14. Finding Inductive Loop Invariants using Large Language Models — Adharsh Kamath et al., 2023

https://scholar.google.com/scholar?q=Finding+Inductive+Loop+Invariants+using+Large+Language+Models

15. LLM For Loop Invariant Generation and Fixing: How Far Are We? — Mostafijur Rahman Akhond, Saikat Chakraborty, Gias Uddin, 2025

https://scholar.google.com/scholar?q=LLM+For+Loop+Invariant+Generation+and+Fixing%3A+How+Far+Are+We%3F

16. Type-Constrained Code Generation with Language Models — Niels Mundler et al., 2025

https://scholar.google.com/scholar?q=Type-Constrained+Code+Generation+with+Language+Models

17. Invariant-based Program Repair — Omar I. Al-Bataineh, 2024

https://scholar.google.com/scholar?q=Invariant-based+Program+Repair

18. AI Post Transformers: Program Synthesis with Large Language Models — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-20-program-synthesis-with-large-language-mo-b962ec.mp3

19. AI Post Transformers: SGLang for Faster Structured LLM Programs — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-06-sglang-for-faster-structured-llm-program-c59f1c.mp3

20. AI Post Transformers: SkillsBench for Evaluating Agent Skills — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-14-skillsbench-for-evaluating-agent-skills-58bb1e.mp3

This episode explores the paper Test-Time Training with KV Binding Is Secretly Linear Attention and asks whether KV-binding test-time training is really doing online memorization or instead behaving like learned linear attention with sequence-specific fast weights. It explains how this approach differs from a standard transformer KV cache, situates it within earlier test-time-training work on expressive hidden states, and connects it to the broader push for long-context models that avoid quadratic softmax attention costs. The discussion highlights several findings that weaken the retrieval-style memory story: converged models show a query-key mismatch, replacing queries with keys barely changes aggregate performance, stronger inner-loop optimization does not reliably help, and even switching from descent to ascent can still work. Listeners would find it interesting because the episode reframes a flashy mechanism in simpler algebraic terms, clarifies which equivalence claims are exact versus empirical, and shows how that shift could change how researchers think about memory and efficiency in next-generation sequence models.

Sources:

1. Test-Time Training with KV Binding Is Secretly Linear Attention — Junchen Liu, Sven Elflein, Or Litany, Zan Gojcic, Ruilong Li, 2026

http://arxiv.org/abs/2602.21204

2. Transformers are RNNs: Fast Autoregressive Transformers with Linear Attention — Angelos Katharopoulos, Apoorv Vyas, Nikolaos Pappas, François Fleuret, 2020

https://arxiv.org/abs/2006.16236

3. Linear Transformers Are Secretly Fast Weight Programmers — Imanol Schlag, Kazuki Irie, Jürgen Schmidhuber, 2021

https://arxiv.org/abs/2102.11174

4. Learning to (Learn at Test Time): RNNs with Expressive Hidden States — Yu Sun, Xinhao Li, Karan Dalal, Jiarui Xu, Xinlei Chen, Tatsunori Hashimoto, Carlos Guestrin, et al., 2024

https://arxiv.org/abs/2407.04620

5. Test-Time Training with KV Binding Is Secretly Linear Attention — Junchen Liu, Sven Elflein, Or Litany, Zan Gojcic, Ruilong Li, 2026

https://arxiv.org/abs/2602.21204

6. Titans: Learning to Memorize at Test Time — Ali Behrouz, Peilin Zhong, Vahab Mirrokni, 2024

https://scholar.google.com/scholar?q=Titans%3A+Learning+to+Memorize+at+Test+Time

7. End-to-End Test-Time Training for Long Context — Arnuv Tandon et al., 2025

https://scholar.google.com/scholar?q=End-to-End+Test-Time+Training+for+Long+Context

8. Understanding Factual Recall in Transformers via Associative Memories — Eshaan Nichani, Jason D. Lee, Alberto Bietti, 2024

https://arxiv.org/abs/2412.06538

9. Quantifying Logical Consistency in Transformers via Query-Key Alignment — Eduard Tulchinskii, Anastasia Voznyuk, Laida Kushnareva, Andrei Andriiainen, Irina Piontkovskaya, Evgeny Burnaev, Serguei Barannikov, 2025

https://arxiv.org/abs/2502.17017

10. Dissecting Query-Key Interaction in Vision Transformers — Xu Pan, Aaron Philip, Ziqian Xie, Odelia Schwartz, 2024

https://arxiv.org/abs/2405.14880

11. Improved Test-Time Adaptation for Domain Generalization — Liang Chen, Yong Zhang, Yibing Song, Ying Shan, Lingqiao Liu, 2023

https://arxiv.org/abs/2304.04494

12. AdaShadow: Responsive Test-time Model Adaptation in Non-stationary Mobile Environments — Cheng Fang, Sicong Liu, Zimu Zhou, Bin Guo, Jiaqi Tang, Ke Ma, Zhiwen Yu, 2024

https://arxiv.org/abs/2410.08256

13. Beyond Model Adaptation at Test Time: A Survey — Zehao Xiao, Cees G. M. Snoek, 2024

https://arxiv.org/abs/2411.03687

14. AI Post Transformers: Atlas: Test-Time Memory for Long Contexts — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-11-atlas-test-time-memory-for-long-contexts-1d5545.mp3

15. AI Post Transformers: Parallelizing DeltaNet Linear Transformers over Sequence Length — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-18-parallelizing-deltanet-linear-transforme-2d0377.mp3

16. AI Post Transformers: Gated Linear Attention for Efficient Long Sequences — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-18-gated-linear-attention-for-efficient-lon-c858ab.mp3

17. AI Post Transformers: δ-mem and Online Memory for LLMs — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-13-d-mem-and-online-memory-for-llms-6622fa.mp3

18. AI Post Transformers: Do Transformers Need Three Projections? — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-11-do-transformers-need-three-projections-c227d6.mp3

This episode explores a June 2026 paper on when document-specific LoRA adapters actually help compared with standard retrieval-augmented generation, especially once a model’s KV cache has been aggressively compressed. It walks through the core mechanics of RAG, LoRA, prefill vs. decode costs, parametric retrieval augmentation, and the Compactor method used to rank and retain only part of a document’s cached attention state. The main argument is that LoRA is not a replacement for explicit retrieved text: when most document context is still intact, the adapter adds little, but under severe compression it becomes much more useful, recovering roughly 13 to 21 ROUGE-L points when the document cache is completely removed. Listeners would find it interesting because it turns a vague “LoRA vs. RAG” debate into a concrete systems question about memory budgets, repeated question answering, and the tradeoff between inspectable evidence and lossy parameter-side memory.

Sources:

1. Rethinking LoRA Memory Through the Lens of KV Cache Compression — Chunsheng Zuo, Liaoyaqi Wang, William Jurayj, William Fleshman, Benjamin Van Durme, 2026

http://arxiv.org/abs/2606.05698

2. Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks — Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, et al., 2020

https://scholar.google.com/scholar?q=Retrieval-Augmented+Generation+for+Knowledge-Intensive+NLP+Tasks

3. Parametric Retrieval Augmented Generation — Weihang Su, Yichen Tang, Qingyao Ai, Junxi Yan, et al., 2025

https://scholar.google.com/scholar?q=Parametric+Retrieval+Augmented+Generation

4. Understanding Parametric Knowledge Injection in Retrieval-Augmented Generation — Minghao Tang, Shiyu Ni, Jingtong Wu, Zengxin Han, Keping Bi, 2025

https://scholar.google.com/scholar?q=Understanding+Parametric+Knowledge+Injection+in+Retrieval-Augmented+Generation

5. Rethinking LoRA Memory Through the Lens of KV Cache Compression — Chunsheng Zuo, Liaoyaqi Wang, William Jurayj, William Fleshman, Benjamin Van Durme, 2026

https://scholar.google.com/scholar?q=Rethinking+LoRA+Memory+Through+the+Lens+of+KV+Cache+Compression

6. Training Plug-n-Play Knowledge Modules with Deep Context Distillation — Lucas Caccia et al., 2025

https://scholar.google.com/scholar?q=Training+Plug-n-Play+Knowledge+Modules+with+Deep+Context+Distillation

7. Activated LoRA: Fine-tuned LLMs for Intrinsics — Kristjan Greenewald et al., 2025

https://scholar.google.com/scholar?q=Activated+LoRA%3A+Fine-tuned+LLMs+for+Intrinsics

8. LoRA-Augmented Generation (LAG) for Knowledge-Intensive Language Tasks — William Fleshman and Benjamin Van Durme, 2025

https://scholar.google.com/scholar?q=LoRA-Augmented+Generation+%28LAG%29+for+Knowledge-Intensive+Language+Tasks

9. Doc-to-LoRA: Learning to Instantly Internalize Contexts — Rujikorn Charakorn et al., 2026

https://scholar.google.com/scholar?q=Doc-to-LoRA%3A+Learning+to+Instantly+Internalize+Contexts

10. Decoupling Knowledge and Task Subspaces for Composable Parametric Retrieval Augmented Generation — Weihang Su et al., 2026

https://scholar.google.com/scholar?q=Decoupling+Knowledge+and+Task+Subspaces+for+Composable+Parametric+Retrieval+Augmented+Generation

11. KeDiff: Key Similarity-Based KV Cache Eviction for Long-Context LLM Inference in Resource-Constrained Environments — Junyoung Park et al., 2025

https://scholar.google.com/scholar?q=KeDiff%3A+Key+Similarity-Based+KV+Cache+Eviction+for+Long-Context+LLM+Inference+in+Resource-Constrained+Environments

12. Model Tells You Where to Merge: Adaptive KV Cache Merging for LLMs on Long-Context Tasks — Zheng Wang et al., 2024

https://scholar.google.com/scholar?q=Model+Tells+You+Where+to+Merge%3A+Adaptive+KV+Cache+Merging+for+LLMs+on+Long-Context+Tasks

13. Parametric Retrieval-Augmented Generation using Latent Routing of LoRA Adapters — Zhan Su, Fengran Mo, Jian-yun Nie, 2025

https://scholar.google.com/scholar?q=Parametric+Retrieval-Augmented+Generation+using+Latent+Routing+of+LoRA+Adapters

14. One Token Can Help! Learning Scalable and Pluggable Virtual Tokens for Retrieval-Augmented Large Language Models — Yutao Zhu et al., 2024

https://scholar.google.com/scholar?q=One+Token+Can+Help%21+Learning+Scalable+and+Pluggable+Virtual+Tokens+for+Retrieval-Augmented+Large+Language+Models

15. AI Post Transformers: Doc-to-LoRA: Internalizing Context as LoRA — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-29-doc-to-lora-internalizing-context-as-lor-8dd5ec.mp3

16. AI Post Transformers: KVzip for Query-Agnostic KV Cache Compression — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-29-kvzip-for-query-agnostic-kv-cache-compre-72afe5.mp3

17. AI Post Transformers: Efficient KV Cache Sharing for Multi-LoRA Agents — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-22-efficient-kv-cache-sharing-for-multi-lor-afda05.mp3

18. AI Post Transformers: Lookahead Q-Cache for Consistent KV Eviction — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-03-25-lookahead-q-cache-for-consistent-kv-evic-d97b09.mp3

19. AI Post Transformers: KVzap: Fast, Adaptive, Faithful KV Cache Pruning — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-30-kvzap-fast-adaptive-faithful-kv-cache-pr-dbe515.mp3

20. AI Post Transformers: Explicit Information Transmission for Context Compression — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-05-explicit-information-transmission-for-co-24e3c2.mp3

This episode explores IndexMem, a long-context LLM inference method that tries to cut KV-cache memory by learning which token states to evict while preserving useful information in a fixed-size latent memory. It explains the mechanics behind the KV cache, prefill, and decoding, then frames the real systems problem: for long prompts, memory traffic and bandwidth can become a bigger bottleneck than raw compute. The discussion focuses on two distinct challenges the paper separates clearly: predicting which cached tokens will matter in the future, and avoiding irreversible forgetting after eviction by writing evicted information into a learned summary state. Listeners interested in code agents, multimodal pipelines, and long-context serving will find it useful because it connects transformer theory to practical deployment constraints while questioning whether current evidence really supports the paper’s bigger million-token ambitions.

Sources:

1. IndexMem: Learned KV-Cache Eviction with Latent Memory for Long-Context LLM Inference — Xintong Yang, Hao Gu, Binxing Xu, Lujun Li, Bei Liu, Jiacheng Liu, Qiyuan Zhu, Sirui Han, Yike Guo, 2026

http://arxiv.org/abs/2605.25475

2. Expected Attention: KV Cache Compression by Estimating Attention from Future Queries Distribution — Alessio Devoto, Maximilian Jeblick, Simon Jegou, 2025

https://scholar.google.com/scholar?q=Expected+Attention%3A+KV+Cache+Compression+by+Estimating+Attention+from+Future+Queries+Distribution

3. Lookahead Q-Cache: Achieving More Consistent KV Cache Eviction via Pseudo Query — Yixuan Wang, Shiyu Ji, Yijun Liu, Yuzhuang Xu, Yang Xu, Qingfu Zhu, Wanxiang Che, 2025

https://scholar.google.com/scholar?q=Lookahead+Q-Cache%3A+Achieving+More+Consistent+KV+Cache+Eviction+via+Pseudo+Query

4. Locret: Enhancing Eviction in Long-Context LLM Inference with Trained Retaining Heads on Consumer-Grade Devices — Yuxiang Huang, Binhang Yuan, Xu Han, Chaojun Xiao, Zhiyuan Liu, 2024

https://scholar.google.com/scholar?q=Locret%3A+Enhancing+Eviction+in+Long-Context+LLM+Inference+with+Trained+Retaining+Heads+on+Consumer-Grade+Devices

5. KVReviver: Reversible KV Cache Compression with Sketch-Based Token Reconstruction — Aomufei Yuan, Zhiming Wang, Ruijie Miao, Dayu Wang, Yuxuan Tian, Zihan Wang, Yebo Peng, Yuhan Wu, Bairen Yi, Xin Liu, Tong Yang, 2025

https://scholar.google.com/scholar?q=KVReviver%3A+Reversible+KV+Cache+Compression+with+Sketch-Based+Token+Reconstruction

6. xKV: Cross-Layer SVD for KV-Cache Compression — Chi-Chih Chang, Chien-Yu Lin, Yash Akhauri, Wei-Cheng Lin, Kai-Chiang Wu, Luis Ceze, Mohamed S. Abdelfattah, 2025

https://scholar.google.com/scholar?q=xKV%3A+Cross-Layer+SVD+for+KV-Cache+Compression

7. IndexCache: Accelerating Sparse Attention via Cross-Layer Index Reuse — Yushi Bai, Qian Dong, Ting Jiang, Xin Lv, Zhengxiao Du, Aohan Zeng, Jie Tang, Juanzi Li, 2026

https://scholar.google.com/scholar?q=IndexCache%3A+Accelerating+Sparse+Attention+via+Cross-Layer+Index+Reuse

8. Titans: Learning to Memorize at Test Time — Ali Behrouz, Peilin Zhong, Vahab Mirrokni, 2024

https://scholar.google.com/scholar?q=Titans%3A+Learning+to+Memorize+at+Test+Time

9. FreeKV: Boosting KV Cache Retrieval for Efficient LLM Inference — Guangda Liu et al., 2025

https://arxiv.org/abs/2505.13109

10. Streaming Video Question-Answering with In-context Video KV-Cache Retrieval — Shangzhe Di et al., 2025

https://arxiv.org/abs/2503.00540

11. LLMs Know What to Drop: Self-Attention Guided KV Cache Eviction for Efficient Long-Context Inference — Guangtao Wang et al., 2025

https://arxiv.org/abs/2503.08879

12. Ada-KV: Optimizing KV Cache Eviction by Adaptive Budget Allocation for Efficient LLM Inference — Yuan Feng et al., 2024

https://arxiv.org/abs/2407.11550

13. In-context KV-Cache Eviction for LLMs via Attention-Gate — Zihao Zeng et al., 2024

https://arxiv.org/abs/2410.12876

14. MomentKV: Closing the Directional Gap in KV Cache Eviction for Long-Context Inference — Yu Li et al., 2026

https://arxiv.org/abs/2606.01563

15. ChunkKV: Semantic-Preserving KV Cache Compression for Efficient Long-Context LLM Inference — Xiang Liu et al., 2025

https://arxiv.org/abs/2502.00299

16. MEDA: Dynamic KV Cache Allocation for Efficient Multimodal Long-Context Inference — Zhongwei Wan et al., 2025

https://arxiv.org/abs/2502.17599

17. AI Post Transformers: Adaptive Compression Techniques for Efficient LLM Inference — Hal Turing & Dr. Ada Shannon, 2025

https://podcast.do-not-panic.com/episodes/adaptive-compression-techniques-for-efficient-llm-inference/

18. AI Post Transformers: Explicit Information Transmission for Context Compression — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-05-05-explicit-information-transmission-for-co-24e3c2.mp3

19. AI Post Transformers: TRELLIS and Bounded-Memory Transformer KV Compression — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-02-trellis-and-bounded-memory-transformer-k-81f237.mp3

20. AI Post Transformers: End-to-End Context Compression at Scale — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-06-10-end-to-end-context-compression-at-scale-278c70.mp3

21. AI Post Transformers: 50x KV Cache Compression in Seconds via Attention Matching — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/50x-kv-cache-compression-in-seconds-via-attention-matching/

22. AI Post Transformers: Stochastic KV Routing for Cache Sharing — Hal Turing & Dr. Ada Shannon, 2026

https://podcast.do-not-panic.com/episodes/2026-04-29-stochastic-kv-routing-for-cache-sharing-5fef63.mp3

Interactive Visualization: IndexMem: Learned KV-Cache Eviction for Long-Context LLMs