BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Events - ECPv6.17.0//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://live-events-ucsc.pantheonsite.io
X-WR-CALDESC:Events for Events
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20250309T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20251102T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20260308T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20261101T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20270314T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20271107T090000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Los_Angeles:20260810T103000
DTEND;TZID=America/Los_Angeles:20260810T123000
DTSTAMP:20260721T182603Z
CREATED:20260721T182603Z
LAST-MODIFIED:20260721T182603Z
UID:10015110-1786357800-1786365000@live-events-ucsc.pantheonsite.io
SUMMARY:Zhao\, Z. (CSE) - TOWARD VERIFIABLE REASONING IN LLMS
DESCRIPTION:Chain-of-thought (CoT) prompting can improve final-answer performance\, but it does not guarantee that intermediate reasoning steps are faithful\, valid\, or checkable. This proposal studies how formal methods can make natural-language reasoning more reliable by translating CoT rationales into Lean artifacts\, checking the resulting theorem statements and proofs\, and using compiler feedback to diagnose and repair failures. The completed work evaluates direct zero-shot and few-shot auto-formalization pipelines for quantity- and logic-focused reasoning problems\, measuring proof type-check rate\, theorem-statement validity\, assumption faithfulness\, and repair behavior. The ongoing work extends this pipeline with AMR-guided semantic representations and altered-rationale stress tests. The planned work proposes methods of modeling LLM Agent thinking in Lean. Together\, these components separate two questions that are often conflated: whether a model translated the reasoning into the right formal goal\, and whether that goal can be proved once translated. The research goal is to develop an evaluation framework and a tool-supported workflow to improve the reliability\, auditability\, and semantic faithfulness of LLM reasoning. \nEvent Host: Zekun Zhao\, Ph.D. Student\, Computer Science & Engineering \nAdvisor: Jeffrey Flanigan \nZoom: https://ucsc.zoom.us/j/96068207641?pwd=anTpLhBXhIdaIhXKDTB32HlDMA6uIO.1 \nPasscode: 656037
URL:https://live-events-ucsc.pantheonsite.io/event/zhao-z-cse-toward-verifiable-reasoning-in-llms/
LOCATION:Silicon Valley Campus\, 3175 Bowers Avenue\, Santa Clara\, CA\, 95054\, United States
CATEGORIES:Ph.D. Presentations
ATTACH;FMTTYPE=image/jpeg:https://live-events-ucsc.pantheonsite.io/wp-content/uploads/2026/04/ph.d.-presentation-graphic-option2.jpg
GEO:37.3796975;-121.9765484
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Silicon Valley Campus 3175 Bowers Avenue Santa Clara CA 95054 United States;X-APPLE-RADIUS=500;X-TITLE=3175 Bowers Avenue:geo:-121.9765484,37.3796975
END:VEVENT
END:VCALENDAR