Spotlight on Ido Pinto’s poster at ICLM 2026 

A few days ago, Ido Pinto from The Hebrew University of Jerusalem presented his poster and discussed his paper – co-authored with Yizhak Elboher , Andrew Wu, Nina Narodytska, and Guy Katz – titled “𝗡𝗼𝘁 𝗔𝗹𝗹 𝗜𝗻𝘃𝗮𝗿𝗶𝗮𝗻𝘁𝘀 𝗔𝗿𝗲 𝗘𝗾𝘂𝗮𝗹: 𝗖𝘂𝗿𝗮𝘁𝗶𝗻𝗴 𝗧𝗿𝗮𝗶𝗻𝗶𝗻𝗴 𝗗𝗮𝘁𝗮 𝘁𝗼 𝗔𝗰𝗰𝗲𝗹𝗲𝗿𝗮𝘁𝗲 𝗣𝗿𝗼𝗴𝗿𝗮𝗺 𝗩𝗲𝗿𝗶𝗳𝗶𝗰𝗮𝘁𝗶𝗼𝗻 𝘄𝗶𝘁𝗵 𝗦𝗟𝗠𝘀” at CML2026 (Forty-Third International Conference on Machine Learning) in South Korea.

𝗛𝗲𝗿𝗲’𝘀 𝗮 𝗾𝘂𝗶𝗰𝗸 𝘀𝘂𝗺𝗺𝗮𝗿𝘆 𝗼𝗳 𝘁𝗵𝗲𝗶𝗿 𝘄𝗼𝗿𝗸

Program verification mathematically guarantees that software behaves correctly, which is essential for safety-critical systems where a single bug can be catastrophic. It often depends on loop invariants, properties that hold on every iteration of a loop, and discovering them automatically has been a bottleneck for decades.
We introduce WONDA, a data curation pipeline for loop invariant generation that turns raw, verbose invariants from symbolic verifiers into compact, high-quality training data, formally verifying every candidate so it remains provably correct and useful.
Fine-tuning small models on this curated data yields consistent gains across the Qwen3, Llama-3.1, and Mistral families.
Most strikingly, a 4B model outperforms an 80B, and a 14B matches GPT-5.2 on end-to-end verification time.
This shows that careful data curation lets small models compete with much larger ones, a practical step toward efficient LLM-assisted verification.