Use theorem provers to ensure the correctness of your LLM's reasoning

https://github.com/DebarghaG/proofofthought

#HackerNews #theoremprovers #LLM #correctness #reasoning #AIresearch #proofsofthought

Reenvío información sobre cursos intensivos de #Computación en la #UBA

> Escuela de Ciencias Informáticas
> 28 de julio al 1 de agosto

> Ya está confirmado el Programa completo de cursos. Cada curso tiene una duración de 15 horas reloj en total (3 horas por día, de lunes a viernes). La inscripción a cursos se abrirá el 9 de junio y se cerrará el 4 de julio para estudiantes de #Exactas-UBA y el 18 de julio para público general.

> TURNO MAÑANA: 9 A 12
> M1: Análisis Probabilístico de Algoritmos
> M2: The Evolution of Blockchain Technologies
> M3: Modelos generativos de imágenes basados en redes profundas

> TURNO TARDE: 13:30 A 16:30
> T1: Interactive theorem provers: theory and practice
> T2: Introducción a la computación cuántica
> T3: Procesamiento de imágenes con aplicación a la biomedicina

> TURNO NOCHE: 18 a 21
> N1: Introduction to Column Generation and VRPSolver
> N2: De la planificación no determinista a la síntesis y planificación generalizada
> N3: AI for Immersive Technologies: Enhancing Virtual and Augmented Realities

> Se otorgará certificado de asistencia concurriendo al 80% de las clases. El certificado de aprobación estará sujeto a una evaluación final cuya modalidad es elegida por cada profesor y se informa al comienzo de cada curso.

> Gracias al apoyo de nuestros auspiciantes, la ECI ofrece Becas de ayuda económica para estudiantes de universidad nacionales y de países limítrofes, que residan a más de 100 kms de la Ciudad de Buenos Aires. Estas becas son fundamentales para financiar los gastos de traslado para estudiantes que deseen asistir a los cursos que dicta la Escuela. La convocatoria estará abierta desde el 19 de mayo al 2 de junio.

> La información sobre cursos, inscripción, becas y otras actividades se actualizará, a medida que esté disponible, en el sitio web: http://www.dc.uba.ar/eci

#ComputaciónUBA #CienciasInformáticas #CienciasDeLaComputación #CABA #Argentina #BuenosAires #AMBA #AnálisisProbabilístico #Blockchain #ModelosGenerativos #TheoremProvers #ComputaciónCuántica #ProcesamientoDeImágenes #biomedicina #ColumnGeneration #PlanificaciónNoDeterminista #PlanificaciónGeneralizada
#ImmersiveTechnologies

I'm trying to use Z3 to solve a logic puzzle, mostly as a chance to learn more about Z3. I'm stuck on a couple of things out of the gate:

How do people usually interact with Z3 in practice? Manually writing smtlib doesn't seem like it would scale. Do people use the Z3 bindings to Python, Java, etc. or are people using libraries to generate smtlib syntax which then gets fed in?

I'm looking at the TypeScript bindings. There's a "high level" set of bindings which seems incomplete (no support for datatype declarations, for example) and a "low level" set of bindings that seems more featureful. I get the vibe that the high level bindings aren't getting a lot of usage or maintenance. Can anyone confirm or give background here? Is TS simply the wrong language to use, or am I still likely to be writing Z3 in a modern-ish way by using the low level bindings?

#z3 #smt #smtlib #TheoremProvers #TheoremProving

Extended abstract by Sára Juhošová at TyDe '24: How Novices Perceive Interactive Theorem Provers

"we conducted an online survey among bachelor students, asking them to list the obstacles they encountered while learning Agda. [...]These observations point to one prominent point of improvement: providing a more accessible and sturdy infrastructure for ITP programmers."

https://icfp24.sigplan.org/details/tyde-2024-papers/1/How-Novices-Perceive-Interactive-Theorem-Provers-Extended-Abstract-

#agda #theoremprovers #usability #tyde

My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!

Who? anyone who uses or has used an interactive theorem prover for whatever purpose

What? 90 - 120 minute interviews (possibly including a small think-aloud programming session)

When? interviews will be scheduled starting September 2024

Where? online (participants from anywhere are welcome)

We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.

Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy

#Agda #Coq #Lean #Isabelle #Usability #TheoremProvers

"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
- Jacob Lurie

https://www.youtube.com/watch?v=eNgUQlpc1m0

#theoremprovers #coq #agda #lean #mathematics #hott

There are some (seemingly obvious) real-world applications of interactive #TheoremProvers like #lean that honestly have the power to change the world, we just have a broken social system that wont properly invest in them. For example, I imagine that carefully crafted curricular mathematics teaching languages ala #HTDP for K-12 (with perhaps a scratch-like interface for the younger kids) created in lean would be a game-changer for mathematics education.

I was lucky enough to be sent to a decent public school for #autistic and #ADHD kids growing up, because I had consistently done terribly at math in school because I couldn't sit still, keep my mouth closed, and was constantly in ISAP, but I always scored in the top percentage of standardized tests. There I got to do mathematics self-study, with a teacher to help when needed, and that was truly liberating, and I graduated early with an almost 4.0 grade point average, and went on to do an (unfinished) philosophy doctorate, much of which involved category theory. I feel like if kids had an environment to independently explore #mathematics, one that grows with them, many kids that are bad at it now would succeed.