Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt

• URL: http://arxiv.org/abs/2609.06226v1
• Date: Sat, 05 Sep 2026 18:49:38 GMT
• Title: Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
• Abstract summary: Large language models (LLMs) have recently made substantial progress in formal proof generation.<n> Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds.<n>This paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation.
• Score: 8.739112129971362
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have recently made substantial progress in formal proof generation, yet presenting distinctive challenges in cryptographic area. Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds, which can be provided by a machine-checked framework named EasyCrypt. Although all objects may appear in available context, LLMs still struggle because proof-theoretic dependencies are typically implicit in a linear representation and distributed across multiple programs. So, this paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation. Given the natural-language security description, with formal context and target propositions, the proof objects can be normalized into a typed proof-relation graph. Then a structure-preserving visual compiler transforms the graph into the formula-rich visual proof state that guides a multimodal model in generating the EasyCrypt proof. Also, the Scratchy-eval, a 114-task dataset derived from reliable official EasyCrypt files, has been introduced. It contains 64 security-form proof generations and 50 multiple-choice knowledge tests. After a series of evaluations, covering semantic grounding, relational invariants, and game reductions, classical LLMs like GPT-5.6-Sol and Claude-Opus-5 have gained a clear advantage from Scratchy's structured visual proof states. This contrast suggests that explicit proof structure can make the improvement and multimodal proof-state representation as a promising direction for computer-aided cryptography.

Related papers

• UniProbe: A Learnable Token-Level Hallucination Detector for Large VLMs using Multi-Structural Internal Representations [61.85916280854257]
  Large Vision-Language Models (LVLMs) achieve impressive visual reasoning and dialogue capabilities, yet frequently hallucinate content unsupported by the visual input.<n>We introduce textbfUniProbe, a lightweight, unified, learnable detector that models a frozen LVLM's heterogeneous computational trace from a single forward pass.
  arXiv  Detail & Related papers  (2026-08-11T12:01:59Z)
• Game Hopping in Lean [5.623680633781937]
  We present HOPSCOTCH, a Lean 4 framework for mechanizing sound, game-based cryptographic proofs.<n>Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm.<n>We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction.
  arXiv  Detail & Related papers  (2026-08-06T16:52:16Z)
• CryptanalysisBench: Can LLMs do Cryptanalysis? [76.79639292270497]
  We introduce CryptanalysisBench, 191 tasks across six families of cryptographic primitives.<n>Our benchmark consists of three tiers: (i) primitives with known practical breaks; (ii) primitives with no known practical break, evaluated both at full strength and as scaled-down variants.<n>Five frontier models break 65%-86% of Tier 1 schemes, 6-12 Tier-2 schemes at full strength, and 24-61 across all scaled-down variants.
  arXiv  Detail & Related papers  (2026-07-20T22:09:40Z)
• ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
  ShannonProver is an agentic framework for automating cryptographic proofs.<n>It targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into Prov-level proof obligations.<n>We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies.
  arXiv  Detail & Related papers  (2026-07-03T00:50:51Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields.<n>Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program.<n>This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
  arXiv  Detail & Related papers  (2026-04-07T19:33:54Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  Large Language Models (LLMs) have shown success in code analysis and synthesis. We present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis.
  arXiv  Detail & Related papers  (2023-11-07T05:47:47Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  This document presents the security protocol verifier CryptoVerif. It does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can work automatically, or the user can guide it with manual proof indications.
  arXiv  Detail & Related papers  (2023-10-23T07:53:38Z)
• Towards General Visual-Linguistic Face Forgery Detection [95.73987327101143]
  Deepfakes are realistic face manipulations that can pose serious threats to security, privacy, and trust. Existing methods mostly treat this task as binary classification, which uses digital labels or mask signals to train the detection model. We propose a novel paradigm named Visual-Linguistic Face Forgery Detection(VLFFD), which uses fine-grained sentence-level prompts as the annotation.
  arXiv  Detail & Related papers  (2023-07-31T10:22:33Z)
• Publicly-Verifiable Deletion via Target-Collapsing Functions [81.13800728941818]
  We show that targetcollapsing enables publiclyverifiable deletion (PVD) We build on this framework to obtain a variety of primitives supporting publiclyverifiable deletion from weak cryptographic assumptions.
  arXiv  Detail & Related papers  (2023-03-15T15:00:20Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.