Adapting large foundation segmentation models such as SAM2 to video object segmentation (VOS), especially for long sequences, is often limited by the high training cost of full fine-tuning. We present Memory-Aware Fine-tuning (MFT), a parameter-efficient adaptation strategy that freezes the image encoder and selectively updates only memory-related modules responsible for temporal reasoning (memory attention, mask decoder, and memory encoder). To improve robustness on extended sequences, we further introduce a lightweight Memory Compression (MC) network that periodically condenses short-term memory embeddings into a compact long-term representation, keeping the memory bank bounded while preserving historical context. Extensive experiments demonstrate that MFT achieves state-of-the-art results on long-sequence benchmarks while maintaining efficient resource utilization, offering an accessible approach for fine-tuning SAM2 on resource-constrained hardware.

General-purpose probabilistic proof systems operate on programs expressed as systems of arithmetic constraints-an unfriendly representation. There are two broad approaches in the literature to turning friendlier, high-level programs into constraints suitable for proof systems: direct translation and CPU emulation. Direct translators compile a program into highly optimized constraints; unfortunately, this process requires expressing all possible paths through the program, which results in compile times that scale with the program's runtime rather than its size. In addition, the prover must pay the cost of every possible program path, even those untaken by a given input. In contrast, CPU emulators don't compile programs to constraints; instead, they “execute” those programs, expressed as CPU instructions, on a CPU emulator that is itself expressed as constraints. As a result, this approach can't perform powerful, program-specific optimizations, and may require thousands of constraints where direct translation could use a clever handful. Worse, CPU emulators inherit an impractically expensive program state representation from the CPUs they emulate. This paper presents a compiler and proof system, CoBBL, that combines the benefits of CPU emulation and direct translation: it takes advantage of program-specific optimizations, but doesn't pay for an unnecessary state representation or unexecuted computation. CoBBL outperforms CirC, a state-of-the-art direct translator, by 1-30× on compile time and 26–350 ×on prover time, and outperforms Jolt, a state-of-the-art CPU emulator, on prover time by 1.1-1.8× on Jolt-friendly benchmarks, and up to 100× on other benchmarks.

There has been intense interest over the last decade in implementations of probabilistic proofs (IPs, SNARKs, PCPs, and so on): protocols in which an untrusted party proves to a verifier that a given computation was executed properly, possibly in zero knowledge. Nevertheless, implementations still do not scale beyond small computations. A central source of overhead is the front-end: translating from the abstract computation to a set of equivalent arithmetic constraints. This paper introduces a general-purpose framework, called Distiller, in which a user translates to constraints not the original computation but an abstracted specification of it. Distiller is the first in this area to perform such transformations in a way that is provably safe. Furthermore, by taking the idea of "encode a check in the constraints" to its literal logical extreme, Distiller exposes many new opportunities for constraint reduction, resulting in cost reductions for benchmark computations of 1.3–50×, and in some cases, better asymptotics.