Stories with Tag Automated Reasoning

• Show HN: Formalizing Principia Mathematica using Lean

  permalink

  Posted: 2025-04-25 18:49:30

  Verbose tl;dr

  Andrew N. Aguib has launched a project to formalize Alfred North Whitehead and Bertrand Russell's Principia Mathematica within the Lean theorem prover. This ambitious undertaking aims to translate the foundational work of mathematical logic, known for its dense symbolism and intricate proofs, into a computer-verifiable format. The project leverages Lean's powerful type theory and automated proof assistance to rigorously check the Principia's theorems and definitions, offering a modern perspective on this historical text and potentially revealing new insights. The project is ongoing and currently covers a portion of the first volume. The code and progress are available on GitHub.

  This GitHub repository, titled "Formalizing Principia Mathematica using Lean," documents an ambitious project undertaken by Andrew N. Aguib to translate and verify Alfred North Whitehead and Bertrand Russell's monumental work, Principia Mathematica, within the Lean proof assistant. Principia Mathematica, a three-volume work published between 1910 and 1913, represents a landmark attempt to ground mathematics in symbolic logic, aiming to demonstrate that all mathematical truths could be derived from a small set of logical axioms and inference rules. Aguib's project leverages the power of Lean, a modern, interactive theorem prover, to rigorously formalize the definitions, theorems, and proofs presented in Principia. This involves translating the often-opaque symbolic language and intricate arguments of the original text into Lean's precise and computationally verifiable format. The repository contains Lean code corresponding to various sections of Principia, effectively creating a digital, interactive version of the foundational text. This allows for a level of scrutiny and analysis not possible with the original printed work. The formalization process not only helps verify the correctness of the original proofs but also provides a clearer and more accessible representation of the underlying logic. The project is ongoing, with the current state reflecting progress made in formalizing different parts of Principia. The repository serves as a dynamic record of this effort, allowing others to follow, contribute to, and benefit from the ongoing work of translating this historically significant mathematical text into a modern, computationally verifiable form. This endeavor offers valuable insights into the foundations of mathematics, the evolution of logical systems, and the capabilities of modern proof assistants in tackling complex mathematical formalizations. By making Principia Mathematica accessible and verifiable within a powerful computational framework like Lean, the project aims to facilitate a deeper understanding and appreciation of this seminal work in mathematical logic.

  • lean
  • Theorem Prover
  • Principia Mathematica
  • Formalization
  • mathematics
  • Logic
  • Automated Reasoning
  • formal systems
  • Russell
  • Whitehead
  • proof assistant
  • type theory
  • dependent types
  • interactive theorem proving

  Summary of Comments ( 32 )
  https://news.ycombinator.com/item?id=43797256

  Verbose tl;dr

  Hacker News users discussed the impressive feat of formalizing parts of Principia Mathematica in Lean, praising the project for its ambition and clarity. Several commenters highlighted the accessibility of the formalized proofs compared to the original text, making the dense mathematical reasoning easier to follow. Some discussed the potential educational benefits, while others pointed out the limitations of formalization, particularly regarding the philosophical foundations of mathematics addressed in Principia. The project's use of Lean 4 also sparked a brief discussion on the theorem prover itself, with some commenters noting its relative novelty and expressing interest in learning more. A few users referenced similar formalization efforts, emphasizing the growing trend of using proof assistants to verify complex mathematical work.

  The Hacker News post titled "Show HN: Formalizing Principia Mathematica using Lean" (https://news.ycombinator.com/item?id=43797256) has generated a modest number of comments, primarily focusing on the complexities and nuances of formalizing mathematical proofs, particularly within the context of Principia Mathematica.

  One commenter highlights the historical context of Principia, emphasizing its significance as a pre-computer-era attempt to formalize mathematics. They point out the inherent challenges in such an endeavor, particularly the book's verbose and intricate symbolic notation. This comment also touches on the evolution of logical systems and proof assistants, contrasting Principia's methods with more modern approaches.

  Another commenter questions the practical applications of formalizing Principia. They acknowledge the intellectual value of the project but wonder about its relevance to modern mathematics, particularly given the availability of more efficient and powerful proof assistants. This sparks a discussion about the differences between simply verifying existing proofs and actually creating new ones within a formal system.

  A subsequent comment clarifies the distinction between verifying and formalizing a proof. They explain that formalization involves encoding the entire logical structure of a proof within a computer system, allowing for automated checking of each individual step. This is contrasted with mere verification, which might involve a human checking the overall logic of a proof without necessarily breaking down every minute detail.

  Another thread delves into the specifics of Lean, the proof assistant used in this project. Commenters discuss its strengths and weaknesses, comparing it to other systems like Coq and Isabelle. The discussion touches upon the tradeoffs between the accessibility and expressiveness of different proof assistants. One commenter mentions the potential of using Lean for educational purposes, given its relatively user-friendly interface.

  Finally, a comment praises the project for its ambition and potential to contribute to the field of automated theorem proving. They acknowledge the limitations of current technology but express optimism about the future of formal mathematics and the role projects like this can play in advancing the field.

  In summary, the comments on this Hacker News post reflect a nuanced understanding of the challenges and opportunities associated with formalizing mathematical proofs. They range from discussions about the historical significance of Principia Mathematica to the practicalities of using modern proof assistants like Lean. The overall tone is one of cautious optimism, acknowledging the limitations of current technology while recognizing the potential for future advancements.

• Clean, a formal verification DSL for ZK circuits in Lean4

  permalink

  Posted: 2025-03-27 18:33:00

  Verbose tl;dr

  Clean is a new domain-specific language (DSL) built in Lean 4 for formally verifying zero-knowledge circuits. It aims to bridge the gap between circuit development and formal verification by offering a high-level, functional programming style for defining circuits, along with automated proofs of correctness within Lean's powerful theorem prover. Clean compiles to the intermediate representation used by the Circom zk-SNARK toolkit, enabling practical deployment of verified circuits. This approach allows developers to write circuits in a clear, maintainable way, and rigorously prove that these circuits correctly implement the desired logic, enhancing security and trust in zero-knowledge applications. The DSL includes features like higher-order functions and algebraic data types, enabling more expressive and composable circuit design than existing tools.

  The blog post "Clean, a formal verification DSL for ZK circuits in Lean4," introduces Clean, a new domain-specific language (DSL) designed for formally verifying zero-knowledge (ZK) circuits using the Lean4 theorem prover. ZK circuits are computational structures used in cryptography to prove the validity of a statement without revealing the underlying data. Verifying these circuits is crucial for ensuring their correctness and security, but existing methods often lack the rigor of formal verification. Clean aims to address this gap by providing a framework for building and verifying ZK circuits with a high degree of assurance.

  The post emphasizes the difficulty of formally verifying ZK circuits due to their complex nature and the need to reason about both low-level details like bit manipulations and high-level cryptographic concepts. Existing approaches often rely on informal methods or specialized tools limited in their expressive power. Clean, however, leverages the power and expressiveness of Lean4, a dependently-typed programming language and proof assistant, to offer a more robust and versatile solution.

  Clean's DSL embeds within Lean4, allowing developers to define circuits using a syntax similar to functional programming. The DSL provides abstractions for common circuit components, such as arithmetic operations, boolean logic, and cryptographic primitives, enabling concise and readable circuit descriptions. Importantly, these circuit descriptions are not merely specifications but executable code that can be compiled to various ZK proof systems. This facilitates a seamless workflow from circuit design to formal verification and deployment.

  A key aspect of Clean is its integration with Lean4's powerful theorem proving capabilities. Developers can formally specify the desired properties of their circuits using Lean4's logic and then construct proofs to demonstrate that these properties hold. This enables verification of various aspects, including circuit correctness, security properties, and even the soundness of the underlying cryptographic protocols. The dependent typing features of Lean4 play a crucial role in ensuring the consistency and completeness of these proofs.

  The blog post showcases a simple example of verifying a Schnorr signature within Clean, demonstrating how to define the circuit, specify the desired properties, and construct a formal proof of its correctness. While the post acknowledges that Clean is still in its early stages of development, it highlights the potential of the approach for improving the security and reliability of ZK circuits. The authors envision Clean as a valuable tool for researchers and developers working with ZK technology, enabling them to build and deploy formally verified ZK circuits with greater confidence. The ultimate goal is to bridge the gap between the theoretical foundations of ZK cryptography and its practical applications, fostering the development of more secure and trustworthy systems.

  • Formal Verification
  • ZK Circuits
  • zero-knowledge proofs
  • Lean4
  • theorem proving
  • domain specific language
  • DSL
  • Cryptography
  • Security
  • Clean Language
  • program verification
  • Automated Reasoning

  Summary of Comments ( 2 )
  https://news.ycombinator.com/item?id=43496577

  Verbose tl;dr

  Several Hacker News commenters praise Clean's innovative approach to verifying zero-knowledge circuits, appreciating its use of Lean4 for formal proofs and its potential to improve the security and reliability of ZK systems. Some express excitement about Lean4's dependent types and metaprogramming capabilities, and how they might benefit the project. Others raise practical concerns, questioning the performance implications of using a theorem prover for this purpose, and the potential difficulty of debugging generated circuits. One commenter questions the comparison to other frameworks like Noir and Arkworks, requesting clarification on the specific advantages of Clean. Another points out the relative nascency of formal verification in the ZK space, emphasizing the need for further development and exploration. A few users also inquire about the tooling and developer experience, wondering about the availability of IDE support and debugging tools for Clean.

  The Hacker News post titled "Clean, a formal verification DSL for ZK circuits in Lean4" (https://news.ycombinator.com/item?id=43496577) has a moderate number of comments discussing various aspects of the project and its implications.

  Several commenters express enthusiasm for the use of Lean4, highlighting its potential for rigorous formal verification in the zero-knowledge proof space. They see the project as a positive step toward improving the security and reliability of ZK circuits. One commenter specifically praises the choice of Lean4 over other theorem provers, mentioning its speed and the active development community. This sentiment is echoed by another commenter who appreciates the metaprogramming capabilities of Lean4, suggesting it's a good fit for this kind of DSL development.

  There's a discussion around the practicality and usability of formal verification for ZK circuits. One commenter questions the scalability of this approach for larger, real-world circuits, wondering if the proof development overhead becomes too significant. Another commenter points out the inherent complexity of formally verifying cryptographic primitives and protocols, acknowledging the challenge but emphasizing the importance of this work for ensuring security.

  The conversation also touches upon the trade-offs between different formal verification approaches. One commenter contrasts the Lean4-based approach with other methods like Coq, highlighting potential benefits and drawbacks of each. They discuss the potential for integrating with existing tools and frameworks within the ZK ecosystem.

  Some commenters delve into more technical details, discussing the specific features of Lean4 that make it well-suited for this task, such as dependent types and its metaprogramming system. They also discuss the challenges of representing ZK circuits within a formal system and the potential for automated proof generation.

  Finally, there's a thread discussing the broader implications of formal verification in the context of blockchain technology and smart contracts. Commenters acknowledge the growing need for robust security guarantees in these systems and see projects like Clean as important contributions towards achieving this goal. One commenter expresses excitement about the potential for formally verified ZK circuits to enable more complex and secure smart contract applications.

• Translating Natural Language to First-Order Logic for Logical Fallacy Detection

  permalink

  Posted: 2025-03-04 17:36:23

  Verbose tl;dr

  This paper explores using first-order logic (FOL) to detect logical fallacies in natural language arguments. The authors propose a novel approach that translates natural language arguments into FOL representations, leveraging semantic role labeling and a defined set of predicates to capture argument structure. This structured representation allows for the application of automated theorem provers to evaluate the validity of the arguments, thus identifying potential fallacies. The research demonstrates improved performance compared to existing methods, particularly in identifying fallacies related to invalid argument structure, while acknowledging limitations in handling complex linguistic phenomena and the need for further refinement in the translation process. The proposed system provides a promising foundation for automated fallacy detection and contributes to the broader field of argument mining.

  The arXiv preprint "Translating Natural Language to First-Order Logic for Logical Fallacy Detection" by Liu et al. explores a novel approach to identifying logical fallacies within natural language arguments. The authors posit that current methods for fallacy detection, which largely rely on surface-level linguistic features or shallow semantic analysis, are insufficient for capturing the underlying logical structure necessary for robust fallacy identification. They propose instead a method grounded in formal logic, specifically first-order logic (FOL), which allows for a more rigorous and precise representation of argumentative structures.

  The core of their proposed methodology lies in translating natural language arguments into FOL representations. This translation process involves several intricate steps. First, the argumentative text is parsed to identify individual premises and the conclusion. Subsequently, these components are subjected to semantic parsing, transforming them into logical forms expressible within FOL. This necessitates the identification of entities, predicates, and quantifiers present in the natural language, and their subsequent mapping to corresponding elements within the FOL framework. The authors acknowledge the inherent complexity and ambiguity of natural language, which poses a significant challenge for accurate translation. To address this, they employ a combination of existing semantic parsing techniques and introduce novel strategies tailored to the specific requirements of fallacy detection.

  Once the argument is represented in FOL, the authors leverage the power of automated theorem provers to assess the argument's validity. By attempting to prove the conclusion from the premises within the FOL framework, they can determine whether the argument is logically sound. If the conclusion cannot be derived from the premises, this suggests the potential presence of a logical fallacy. However, the mere failure of a proof does not definitively indicate a fallacy; it could simply reflect limitations in the translation process or the theorem prover's capabilities.

  Therefore, the authors introduce a further layer of analysis based on fallacy templates. These templates represent common logical fallacies, such as ad hominem, straw man, or false dilemma, formalized within the FOL framework. By matching the FOL representation of the argument against these pre-defined fallacy templates, the system can identify instances where the argument's structure aligns with a known fallacious pattern. This template-matching approach provides a more targeted and nuanced mechanism for fallacy detection, going beyond the simple binary classification of valid or invalid.

  The paper details experiments conducted on established fallacy datasets, comparing their proposed FOL-based method against existing state-of-the-art techniques. The authors report promising results, demonstrating that their approach achieves improved accuracy in identifying various types of logical fallacies. They further analyze the strengths and limitations of their methodology, acknowledging the ongoing challenges in accurately translating complex natural language arguments into FOL and the need for more comprehensive fallacy templates. The research concludes by emphasizing the potential of FOL-based approaches for advancing the field of automated logical fallacy detection and suggests future research directions, such as incorporating more sophisticated semantic parsing techniques and expanding the library of formalized fallacy templates.

  • natural language processing
  • NLP
  • First-Order Logic
  • FOL
  • Logical Fallacies
  • Fallacy Detection
  • Automated Reasoning
  • Knowledge Representation
  • theorem proving
  • Logic
  • artificial intelligence
  • AI
  • machine learning
  • translation
  • formal methods

  Summary of Comments ( 68 )
  https://news.ycombinator.com/item?id=43257719

  Verbose tl;dr

  Hacker News users discussed the potential and limitations of using first-order logic (FOL) for fallacy detection as described in the linked paper. Some praised the approach for its rigor and potential to improve reasoning in AI, while also acknowledging the inherent difficulty of translating natural language to FOL perfectly. Others questioned the practical applicability, citing the complexity and ambiguity of natural language as major obstacles, and suggesting that statistical/probabilistic methods might be more robust. The difficulty of scoping the domain knowledge necessary for FOL translation was also brought up, with some pointing out the need for extensive, context-specific knowledge bases. Finally, several commenters highlighted the limitations of focusing solely on logical fallacies for detecting flawed reasoning, suggesting that other rhetorical tactics and nuances should also be considered.

  The Hacker News post titled "Translating Natural Language to First-Order Logic for Logical Fallacy Detection" (linking to arXiv paper 2405.02318) has a modest number of comments, sparking a discussion around the practicality and challenges of using formal logic for fallacy detection.

  One commenter expresses skepticism about the real-world applicability of this approach. They argue that logical fallacies in everyday discourse often hinge on implicit premises and contextual nuances that are difficult to capture in formal logic. They suggest that focusing on these implicit elements, which the current approach seems to bypass, is crucial for effective fallacy detection. This commenter also points out the challenge of translating the richness and ambiguity of natural language into the rigid structure of first-order logic, questioning the feasibility of achieving high accuracy in this translation process.

  Another commenter builds on this skepticism by highlighting the issue of ambiguity inherent in natural language. They provide the example of the phrase "most people," which can have different interpretations depending on the context, and how formalizing such a phrase would necessitate making assumptions about the intended quantifier. This emphasizes the difficulty of creating a universally applicable system, as the interpretation of such phrases would need to be tailored to specific domains or contexts.

  A different commenter suggests an alternative perspective, mentioning a different approach to fallacy detection that utilizes large language models (LLMs). They point to a paper where LLMs are used to identify fallacies without explicit formalization. This comment implies that perhaps direct application of statistical methods via LLMs could be a more promising avenue for fallacy detection than attempting the complex task of translating natural language into formal logic.

  Another commenter echoes the concern about the limitations of formal logic in capturing the subtleties of natural language arguments, particularly those involving informal fallacies. They also touch upon the issue of computational complexity associated with logical reasoning, suggesting that practical implementations might face performance bottlenecks.

  Finally, one commenter asks a clarifying question about the specific types of logical fallacies the research addresses, indicating a desire to understand the scope and limitations of the proposed approach. This highlights the importance of clearly defining the target fallacies when evaluating the effectiveness of such systems.

  In summary, the comments largely express reservations about the practicality of the approach outlined in the linked paper, focusing on the difficulties of translating nuanced natural language into formal logic and the potential computational complexities. Alternatives using LLMs are suggested, and the need for careful consideration of the target fallacies is highlighted.

• Compiling C to Safe Rust, Formalized

  permalink

  Posted: 2024-12-20 23:30:03

  Verbose tl;dr

  This paper introduces Crusade, a formally verified translation from a subset of C to safe Rust. Crusade targets a memory-safe dialect of C, excluding features like arbitrary pointer arithmetic and casts. It leverages the Coq proof assistant to formally verify the translation's correctness, ensuring that the generated Rust code behaves identically to the original C, modulo non-determinism inherent in C. This rigorous approach aims to facilitate safe integration of legacy C code into Rust projects without sacrificing confidence in memory safety, a critical aspect of modern systems programming. The translation handles a substantial subset of C, including structs, unions, and functions, and demonstrates its practical applicability by successfully converting real-world C libraries.

  The arXiv preprint "Compiling C to Safe Rust, Formalized" details a novel approach to automatically translating C code into memory-safe Rust code. This process aims to leverage the performance benefits of C while inheriting the robust memory safety guarantees offered by Rust, thereby mitigating the pervasive vulnerability landscape associated with C programming.

  The authors introduce a sophisticated compilation pipeline founded on a formal semantic model. This model rigorously defines the behavior of both the source C code and the target Rust code, enabling a precise and verifiable translation process. The core of this pipeline utilizes a "stacked borrows" model, a memory management strategy adopted by Rust that enforces strict rules regarding shared mutable references and mutable borrows to prevent data races and memory corruption. The translation procedure systematically transforms C pointers into Rust references governed by these stacked borrows rules, ensuring that the resulting Rust code adheres to the same memory safety principles inherent in Rust's design.

  A key challenge addressed by the paper is the handling of C's flexible pointer arithmetic and unrestricted memory access patterns. The authors introduce a concept of "ghost state" within the formal model. This ghost state tracks the provenance and validity of pointers throughout the C code, allowing the compiler to reason about pointer relationships and enforce memory safety during translation. This information is then leveraged to generate corresponding safe Rust constructs, such as safe references and bounds checks, that mirror the intended behavior of the original C code while respecting Rust's stricter memory model.

  The paper demonstrates the effectiveness of their approach through a formalization within the Coq proof assistant. This formalization rigorously verifies the soundness of the translation process, proving that the generated Rust code preserves the semantics of the original C code while guaranteeing memory safety. This rigorous verification provides strong evidence for the correctness and reliability of the proposed compilation technique.

  Furthermore, the authors outline how their approach accommodates various C language features, including function pointers, structures, and unions. They describe how these features are mapped to corresponding safe Rust equivalents, thereby expanding the scope of the translation process to cover a wider range of C code.

  While the paper primarily focuses on the formal foundations and theoretical aspects of the C-to-Rust translation, it also lays the groundwork for future development of a practical compiler toolchain based on these principles. Such a toolchain could offer a valuable pathway for migrating existing C codebases to a safer environment while minimizing manual rewriting effort and preserving performance characteristics. The formal verification aspect provides a high degree of confidence in the safety of the translated code, a crucial consideration for security-critical applications.

  • C
  • Rust
  • Compilers
  • Formal Verification
  • Safety
  • Programming Languages
  • Code Translation
  • Transpilation
  • Automated Reasoning
  • formal methods
  • software engineering
  • Software Security
  • static analysis
  • Memory Safety
  • Type Safety
  • Correctness
  • Semantics
  • Crux
  • CakeML

  Summary of Comments ( 157 )
  https://news.ycombinator.com/item?id=42476192

  Verbose tl;dr

  HN commenters discuss the challenges and nuances of formally verifying the C to Rust transpiler, Cracked. Some express skepticism about the practicality of fully verifying such a complex tool, citing the potential for errors in the formal proofs themselves and the inherent difficulty of capturing all undefined C behavior. Others question the performance impact of the generated Rust code. However, many commend the project's ambition and see it as a significant step towards safer systems programming. The discussion also touches upon the trade-offs between a fully verified transpiler and a more pragmatic approach focusing on common C patterns, with some suggesting that prioritizing practical safety improvements could be more beneficial in the short term. There's also interest in the project's handling of concurrency and the potential for integrating Cracked with existing Rust tooling.

  The Hacker News post titled "Compiling C to Safe Rust, Formalized" (https://news.ycombinator.com/item?id=42476192) has generated a moderate amount of discussion, with several commenters exploring different aspects of the C to Rust transpilation process and its implications.

  One of the most prominent threads revolves around the practical benefits and challenges of such a conversion. A commenter points out the potential for improved safety and maintainability by leveraging Rust's ownership and borrowing system, but also acknowledges the difficulty in translating C's undefined behavior into a Rust equivalent. This leads to a discussion about the trade-offs between preserving the original C code's semantics and enforcing Rust's stricter safety guarantees. The difficulty of handling C's reliance on pointer arithmetic and manual memory management is highlighted as a major hurdle.

  Another key area of discussion centers around the performance implications of the transpilation. Commenters speculate about the potential for performance improvements due to Rust's closer-to-the-metal nature and its ability to optimize memory access. However, others raise concerns about the overhead introduced by Rust's safety checks and the potential for performance regressions if the translation isn't carefully optimized. The question of whether the generated Rust code would be idiomatic and performant is also raised.

  The topic of formal verification and its role in ensuring the correctness of the translation is also touched upon. Commenters express interest in the formalization aspect, recognizing its potential to guarantee that the translated Rust code behaves equivalently to the original C code. However, some skepticism is voiced about the practicality of formally verifying complex C codebases and the potential for subtle bugs to slip through even with formal methods.

  Finally, several commenters discuss alternative approaches to improving the safety and security of C code, such as using static analysis tools or employing safer subsets of C. The transpilation approach is compared to these alternatives, with varying opinions on its merits and drawbacks. The overall sentiment seems to be one of cautious optimism, with many acknowledging the potential of C to Rust transpilation but also recognizing the significant challenges involved.