Echipele:


Echipa 1 (aprox. 18h00 - 18h30)
Roxana Timon
Oana Rotaru
Robert Bărbulescu

Articol:
Foundational Multi-Modal Program Verifiers
Gladshtein et al.
https://verse-lab.github.io/papers/loom-preprint.pdf
Proiect: SMT-LIB parser


Echipa 2 (aprox. 18h40 - 19h10)
Florin Bălan
Renghiuc Bianca Elena
Iulian Gherghevici (? Gipeto)
Articol:
Olympiad-level formal mathematical reasoning with reinforcement learning
Thomas Hubert et al.

https://www.nature.com/articles/s41586-025-09833-y.epdf?sharing_token=habk-SkP_0eBsYTXxWvQ2NRgN0jAjWel9jnR3ZoTv0MXtQ3_v-YqK7HwXBVXR7rn2eBMeYg_oSXP2y9snSU32mIle25sdI1fnnHqcAUsRnH320m9IAMDwyyAS1y4MUHGJVuUWMd1-P3MJUV1kuWKBPLB4_4by2R5PfiYPaOuuF8%3D
Proiect: QOI


Echipa 3 (aprox. 19h10 - 19h40)
Emma Șleghel
Bogdan Cojocariu
Articol:
Towards Robust Mathematical Reasoning
Luong et al.
https://aclanthology.org/2025.emnlp-main.1794.pdf
Proiect: LIA Solver




Proiect -> până în penultima săptămână
Articol -> până la începutul sesiunii


Metodologia de lucru:

1h40 / 3 = aprox. 30 minute

Fiecare echipă discută cu mine timp de 30 de minute în fiecare laborator.

18h00 Echipa 1 (on-site)

18h40 Echipa 2 (Zoom)

19h15 Echipa 3 (Zoom)



Project 1: Write a LIA solver in Lean

(Cooper's Algorithm + Omega/(Simplex + B&B))

(best) Cooper: https://www2.imm.dtu.dk/courses/02917/Presburger1.pdf

https://www.decision-procedures.org/slides/linear-fourier_motzkin.pdf
The Omega test https://dl.acm.org/doi/pdf/10.1145/125826.125848
Arika Abraham https://ths.rwth-aachen.de/wp-content/uploads/sites/4/teaching/vorlesung_satchecking/ws14_15/06a_fourier_motzkin_handout.pdf
Kroening, Strichman: https://www.decision-procedures.org/slides/linear-omega.pdf
(best) Isil Dillig: https://www.cs.utexas.edu/~isil/cs389L/lecture13-6up.pdf

Linear Integer Arithmetic
Aritmetica Presburger

x + 1 == y && (z > 3 * x || z > 7 * y + 1)

nu am voie: x * y


Pasul 1. Cooper's Algorithm
Elimina cuantificatorii:

exists x.(x > 3 * y && x < 7 * y + 13)     --->     ajung la final intr-o formula fara cuantificatori

QFLIA

Pasul 2. Omega / (Simplex + B&B)

x + 1 == y && (z > 3 * x || z > 7 * y + 1)


x + 1 == y  ==> x + 1 <= y && y <= x + 1
z > 3 * x   ==> 3 * x <= z - 1


Project 2: Write an SMT-LIB Parser in Lean

https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-07-07.pdf

https://github.com/riaqn/smtlean/blob/master/src/smtlib.lean

https://www.philipzucker.com/lean_smt/

Alegere: parser recursiv descendent / bilioteca parser combinator (deja in biblioteca standard)


Pasul 1:

def parse : String -> Option Problem


Pasul 2:

def specification : Problem -> Prop



Project 3: Implement QOI in Lean

https://en.wikipedia.org/wiki/QOI_(image_format)
https://qoiformat.org/
https://qoiformat.org/qoi-specification.pdf

// Simplificare: nu exista canalul alpha.

def encode : Bytes -> Bytes
def decode : Bytes -> Bytes

theorem encode_decode : forall image, decode (encode image) == image

Bucev et al.:
https://repositum.tuwien.at/bitstream/20.500.12708/81370/1/Bucev-2022-Formally%20Verified%20Quite%20OK%20Image%20Format-vor.pdf

Ciobâcă and Gratie:
https://profs.info.uaic.ro/stefan.ciobaca/dafny-qoi-ifm2024.pdf

ADA SPARK:
https://blog.adacore.com/quite-proved-image-format




Scopul prezentării unui articol

=

Audiența să înțeleagă rezultatul principal al articolului, fără să fie nevoită să parcurgă în integralitate articolul respectiv


Article 1 (2025):
Olympiad-level formal mathematical reasoning with reinforcement learning
Thomas Hubert et al.

https://www.nature.com/articles/s41586-025-09833-y.epdf?sharing_token=habk-SkP_0eBsYTXxWvQ2NRgN0jAjWel9jnR3ZoTv0MXtQ3_v-YqK7HwXBVXR7rn2eBMeYg_oSXP2y9snSU32mIle25sdI1fnnHqcAUsRnH320m9IAMDwyyAS1y4MUHGJVuUWMd1-P3MJUV1kuWKBPLB4_4by2R5PfiYPaOuuF8%3D



Article 2 (2025):
Towards Robust Mathematical Reasoning
Luong et al.

https://aclanthology.org/2025.emnlp-main.1794.pdf



Article 3 (2026):
RT, 
Foundational Multi-Modal Program Verifiers
Gladshtein et al.

https://verse-lab.github.io/papers/loom-preprint.pdf