News for hackers. Stuff that matters.

A comment on AI solves IMO problems at silver medal level. Parent comment

Re:AI solves IMO problems at silver medal level by nextos on Thursday July 25, 2024 @05:21PM (#41073538)
These kind of LLMs are also very interesting for software engineering. It's just a matter of replacing Lean with something that is more oriented towards proving software properties.

For example, write a formal specification of a function in Dafny on Liquid Haskell and get the LLM to produce code that is formally guaranteed to be correct. Logic-based + probability-based ML.

All GOFAI ideas are still very useful.

[ Parent | on HN ]
Re:AI solves IMO problems at silver medal level by lucioperca on Friday July 26, 2024 @02:39AM (#41076307)
You can also verify software like compilers in Lean:

https://aws.amazon.com/blogs/opensource/lean-into-verified-s...

[ Parent | on HN ]
Re:AI solves IMO problems at silver medal level by nextos on Friday July 26, 2024 @08:20AM (#41077988)
Sure, but Lean has very little support for software problems compared to Isabelle, Coq or Dafny right now.

Those 3 also have a lot of training data as well. Hoping Lean gets more support as it is very friendly.

As a basic learning resource focused on software engineering, there's [1]. But nothing more advanced I am aware of.

[1] The Hitchhiker's Guide to Logical Verification. https://cs.brown.edu/courses/cs1951x/static_files/main.pdf

[ Parent | on HN ]